diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 9080ee8c..03189517 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -9,5 +9,5 @@ jobs: with: github_access_token: ${{ secrets.GITHUB_TOKEN }} - run: nix build - - run: nix build ./.#catt-coq-plugin - - run: nix flake check --all-systems \ No newline at end of file + - run: nix build ./.#catt-rocq-plugin + - run: nix flake check --all-systems diff --git a/README.md b/README.md index 45f370e4..ef1c3e2f 100644 --- a/README.md +++ b/README.md @@ -17,9 +17,9 @@ Make sure `opam` is installed, clone the project and move to the directory where ``` opam install ./catt.opam ``` -The Coq plugin can be installed with the following command +The Rocq plugin can be installed with the following command ``` -opam install ./coq-catt-plugin.opam +opam install ./rocq-catt-plugin.opam ``` ### Building from source with dune and opam @@ -31,15 +31,15 @@ opam install --deps-only ./catt.opam dune build catt.install ``` -To build the Coq plugin, run the following commands: +To build the Rocq plugin, run the following commands: ``` -opam install --deps-only ./coq-catt-plugin.opam -dune build coq-catt-plugin.install +opam install --deps-only ./rocq-catt-plugin.opam +dune build rocq-catt-plugin.install ``` ### Using nix -This repository contains a `flake.nix` file that defines the packages `catt` and `coq-catt-plugin`, as well as `catt-mode`, an editing mode for catt in emacs. +This repository contains a `flake.nix` file that defines the packages `catt` and `rocq-catt-plugin`, as well as `catt-mode`, an editing mode for catt in emacs. ## Syntax There are two keywords to define a new operation: @@ -281,16 +281,16 @@ Calling `catt --no-builtin [FILE]` will deactivate the use of the built-in ident Calling `catt --keep-going [FILE]` will make it so that `catt` will report errors but will keep running on the file and exit with a success even if the file does not typecheck properly. This is not the default behaviour, as in a typical use case, later definitions depend on earlier ones, so if a defined coherence or term is invalid, all further coherences and terms depending on it also fail. This option is useful for scripting and testing. -## Coq plugin -`catt` also provide a plugin for the proof assistant `coq` (packaged separately, called `coq-catt-plugin`), that allows one to export any defined term in `catt` into a function computing higher identity witnesses in `coq`. Once the plugin is installed, write the following to load it at the head of a `coq` file: +## Rocq plugin +`catt` also provide a plugin for the proof assistant `rocq` (packaged separately, called `rocq-catt-plugin`), that allows one to export any defined term in `catt` into a function computing higher identity witnesses in `rocq`. Once the plugin is installed, write the following to load it at the head of a `rocq` file: ``` From Catt Require Import Loader. ``` -You can then use the `Catt` command in `coq` as follows: +You can then use the `Catt` command in `rocq` as follows: ``` Catt [NAMES] FROM FILE [PATH]. ``` -where `[NAMES]` is a list of names of `catt` terms and `[PATH]` is a file containing the definition of those `catt` terms. Upon evaluation of this line, `coq` will call `catt` on the given file and export the listed terms into `coq` terms, whose names will be given as `catt_[NAME]`. For instance, one can write the following: +where `[NAMES]` is a list of names of `catt` terms and `[PATH]` is a file containing the definition of those `catt` terms. Upon evaluation of this line, `rocq` will call `catt` on the given file and export the listed terms into `rocq` terms, whose names will be given as `catt_[NAME]`. For instance, one can write the following: ``` Catt "whiskr" From File "../example/file.catt". diff --git a/catt.opam b/catt.opam index a406153e..9495e059 100644 --- a/catt.opam +++ b/catt.opam @@ -16,7 +16,7 @@ homepage: "https://github.com/thibautbenjamin/catt" bug-reports: "https://github.com/thibautbenjamin/catt/issues" depends: [ "ocaml" {>= "4.14" & < "5.0"} - "dune" {>= "3.16" & >= "3.10"} + "dune" {>= "3.20" & >= "3.10"} "menhir" {>= "20240715"} "base" {>= "0.17.0"} "odoc" {with-doc} @@ -36,3 +36,4 @@ build: [ ] ] dev-repo: "git+https://github.com/thibautbenjamin/catt.git" +x-maintenance-intent: ["(latest)"] diff --git a/coq-catt-plugin.opam b/coq-catt-plugin.opam index 38508172..900828bc 100644 --- a/coq-catt-plugin.opam +++ b/coq-catt-plugin.opam @@ -1,8 +1,8 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -synopsis: "A Coq plugin for the catt proof-assistant" +synopsis: "A Rocq plugin for the catt proof-assistant" description: - "A Coq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types" + "A Rocq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types" maintainer: [ "Thibaut Benjamin " "Chiara Sarti " @@ -16,9 +16,9 @@ tags: ["higher-categories" "dependent-type-theory"] homepage: "https://github.com/thibautbenjamin/catt" bug-reports: "https://github.com/thibautbenjamin/catt/issues" depends: [ - "dune" {>= "3.16"} + "dune" {>= "3.20"} "catt" - "coq" {>= "8.20"} + "coq" {>= "9.0"} "odoc" {with-doc} ] build: [ @@ -36,3 +36,4 @@ build: [ ] ] dev-repo: "git+https://github.com/thibautbenjamin/catt.git" +x-maintenance-intent: ["(latest)"] diff --git a/dune-project b/dune-project index 58dfd9df..6415509f 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 3.16) +(lang dune 3.20) (name catt) (generate_opam_files true) @@ -10,7 +10,7 @@ (license MIT) (using menhir 2.0) (cram enable) -(using coq 0.9) +(using coq 0.10) (package (name catt) @@ -26,11 +26,11 @@ (package (name coq-catt-plugin) - (synopsis "A Coq plugin for the catt proof-assistant") - (description "A Coq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types") + (synopsis "A Rocq plugin for the catt proof-assistant") + (description "A Rocq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types") (depends catt - (coq (>= 8.20))) + (coq (>= 9.0))) (tags (higher-categories dependent-type-theory))) diff --git a/flake.lock b/flake.lock index bd12035c..2cb5b01a 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1726560853, - "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -20,11 +20,11 @@ }, "nix-filter": { "locked": { - "lastModified": 1730207686, - "narHash": "sha256-SCHiL+1f7q9TAnxpasriP6fMarWE5H43t25F5/9e28I=", + "lastModified": 1757882181, + "narHash": "sha256-+cCxYIh2UNalTz364p+QYmWHs0P+6wDhiWR4jDIKQIU=", "owner": "numtide", "repo": "nix-filter", - "rev": "776e68c1d014c3adde193a18db9d738458cd2ba4", + "rev": "59c44d1909c72441144b93cf0f054be7fe764de5", "type": "github" }, "original": { @@ -35,11 +35,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1731139594, - "narHash": "sha256-IigrKK3vYRpUu+HEjPL/phrfh7Ox881er1UEsZvw9Q4=", + "lastModified": 1759036355, + "narHash": "sha256-0m27AKv6ka+q270dw48KflE0LwQYrO7Fm4/2//KCVWg=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "76612b17c0ce71689921ca12d9ffdc9c23ce40b2", + "rev": "e9f00bd893984bc8ce46c895c3bf7cac95331127", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index c4fa8c9c..ea9203d7 100644 --- a/flake.nix +++ b/flake.nix @@ -7,8 +7,16 @@ nix-filter.url = "github:numtide/nix-filter"; }; - outputs = { self, nixpkgs, flake-utils, nix-filter, ... }: - flake-utils.lib.eachDefaultSystem (system: + outputs = + { + self, + nixpkgs, + flake-utils, + nix-filter, + ... + }: + flake-utils.lib.eachDefaultSystem ( + system: let pkgs = (import nixpkgs { inherit system; }); ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14; @@ -33,12 +41,12 @@ ]; }; - coq-plugin = nix-filter.lib { + rocq-plugin = nix-filter.lib { root = ./.; include = [ ".ocamlformat" "dune-project" - (nix-filter.lib.inDirectory "coq_plugin") + (nix-filter.lib.inDirectory "rocq_plugin") (nix-filter.lib.inDirectory "test.t") ]; }; @@ -52,8 +60,8 @@ (nix-filter.lib.inDirectory "lib") (nix-filter.lib.inDirectory "test.t") (nix-filter.lib.inDirectory "web") - (nix-filter.lib.inDirectory "coq_plugin/src/") - "coq_plugin/theories/dune" + (nix-filter.lib.inDirectory "rocq_plugin/src/") + "rocq_plugin/theories/dune" ]; }; @@ -65,7 +73,8 @@ elisp = ./share/site-lisp; }; - in { + in + { packages = { default = self.packages.${system}.catt; @@ -85,7 +94,10 @@ description = "A proof assistant for weak omega-categories"; homepage = "https://www.github.com/thibautbenjamin/catt"; license = nixpkgs.lib.licenses.mit; - maintainers = [ "Thibaut Benjamin" "Chiara Sarti" ]; + maintainers = [ + "Thibaut Benjamin" + "Chiara Sarti" + ]; mainProgram = "catt"; }; }; @@ -107,30 +119,39 @@ ]; meta = { - description = - "Browser embedded version of the catt proof-assistant"; + description = "Browser embedded version of the catt proof-assistant"; homepage = "https://www.github.com/thibautbenjamin/catt"; license = nixpkgs.lib.licenses.mit; - maintainers = [ "Thibaut Benjamin" "Chiara Sarti" ]; + maintainers = [ + "Thibaut Benjamin" + "Chiara Sarti" + ]; }; }; - catt-coq-plugin = pkgs.coqPackages.mkCoqDerivation { + catt-rocq-plugin = pkgs.coqPackages.mkCoqDerivation { pname = "catt-plugin"; version = "1.0"; - src = sources.coq-plugin; + src = sources.rocq-plugin; nativeBuildInputs = [ ]; - buildInputs = - [ self.packages.${system}.catt pkgs.dune_3 pkgs.opam pkgs.coq ]; + buildInputs = [ + self.packages.${system}.catt + pkgs.dune_3 + pkgs.opam + pkgs.rocq-core + ]; mlPlugin = true; useDune = true; meta = { - description = "Coq plugin for the catt proof-assistant"; + description = "Rocq plugin for the catt proof-assistant"; homepage = "https://www.github.com/thibautbenjamin/catt"; license = nixpkgs.lib.licenses.mit; - maintainers = [ "Thibaut Benjamin" "Chiara Sarti" ]; + maintainers = [ + "Thibaut Benjamin" + "Chiara Sarti" + ]; }; }; @@ -148,30 +169,36 @@ }; }; - formatter = pkgs.nixfmt-classic; + formatter = pkgs.nixfmt; checks = { - lint-nix = pkgs.runCommand "check-flake-format" { - nativeBuildInputs = [ pkgs.nixfmt-classic ]; - } '' - echo "checking nix formatting" - nixfmt --check ${sources.nix} - touch $out - ''; - - dune-fmt = pkgs.runCommand "check-ocaml-fmt" { - nativeBuildInputs = [ - ocamlPackages.dune_3 - ocamlPackages.ocaml - ocamlPackages.ocamlformat - ]; - } '' - echo "checking dune and ocaml formatting for catt" - dune fmt \ - --display=short \ - --root=$(pwd) - touch $out - ''; + lint-nix = + pkgs.runCommand "check-flake-format" + { + nativeBuildInputs = [ pkgs.nixfmt ]; + } + '' + echo "checking nix formatting" + nixfmt --check ${sources.nix} + touch $out + ''; + + dune-fmt = + pkgs.runCommand "check-ocaml-fmt" + { + nativeBuildInputs = [ + ocamlPackages.dune_3 + ocamlPackages.ocaml + ocamlPackages.ocamlformat + ]; + } + '' + echo "checking dune and ocaml formatting for catt" + dune fmt \ + --display=short \ + --root=$(pwd) + touch $out + ''; default = self.packages.${system}.catt.overrideAttrs (oldAttrs: { name = "check-${oldAttrs.name}"; @@ -181,7 +208,11 @@ }; devShells.default = pkgs.mkShell { - packages = (with pkgs; [ nixfmt-classic fswatch ]) + packages = + (with pkgs; [ + nixfmt + fswatch + ]) ++ (with ocamlPackages; [ odoc ocaml-lsp @@ -197,10 +228,11 @@ inputsFrom = [ self.packages.${system}.catt self.packages.${system}.catt-web - self.packages.${system}.catt-coq-plugin + self.packages.${system}.catt-rocq-plugin ]; }; devShells.web = self.packages.${system}.catt-web; - }); + } + ); } diff --git a/coq_plugin/_CoqProject b/rocq_plugin/_CoqProject similarity index 57% rename from coq_plugin/_CoqProject rename to rocq_plugin/_CoqProject index 137187bb..e0fe55f6 100644 --- a/coq_plugin/_CoqProject +++ b/rocq_plugin/_CoqProject @@ -1,3 +1,3 @@ -generate-meta-for-package catt --R ../_build/default/coq_plugin/theories/ Catt +-R ../_build/default/rocq_plugin/theories/ Catt -I ../_build/install/default/lib/ diff --git a/coq_plugin/src/coq_plugin.mlpack b/rocq_plugin/src/coq_plugin.mlpack similarity index 100% rename from coq_plugin/src/coq_plugin.mlpack rename to rocq_plugin/src/coq_plugin.mlpack diff --git a/coq_plugin/src/dune b/rocq_plugin/src/dune similarity index 100% rename from coq_plugin/src/dune rename to rocq_plugin/src/dune diff --git a/coq_plugin/src/export.ml b/rocq_plugin/src/export.ml similarity index 93% rename from coq_plugin/src/export.ml rename to rocq_plugin/src/export.ml index d1ed6efc..a390aa50 100644 --- a/coq_plugin/src/export.ml +++ b/rocq_plugin/src/export.ml @@ -12,14 +12,6 @@ let run_catt_on_file f = | Ok f -> Command.exec ~loop_fn:Prover.loop f | Error () -> () -let rec catt_var_to_coq_name v = - match v with - | Var.Db i -> "catt_db_" ^ string_of_int i - | Var.Name s -> "catt_name_" ^ s - | Var.New i -> "catt_new_" ^ string_of_int i - | Var.Plus v -> catt_var_to_coq_name v ^ "_plus" - | Var.Bridge v -> catt_var_to_coq_name v ^ "_bridge" - let counter = ref 0 let anon () = @@ -27,11 +19,11 @@ let anon () = Printf.sprintf "anonymous_term_%d" !counter let c_Q env sigma = - let gr = Coqlib.lib_ref "core.eq.type" in + let gr = Rocqlib.lib_ref "core.eq.type" in Evd.fresh_global env sigma gr let c_R env sigma = - let gr = Coqlib.lib_ref "core.eq.refl" in + let gr = Rocqlib.lib_ref "core.eq.refl" in Evd.fresh_global env sigma gr let rec find_db ctx x = @@ -62,7 +54,7 @@ end = struct let retrieve_lambda value sigma = let build_econstr name = - let gr = Coqlib.lib_ref ("catt_" ^ name) in + let gr = Rocqlib.lib_ref ("catt_" ^ name) in let env = Global.env () in let sigma, econstr = Evd.fresh_global env sigma gr in (env, sigma, econstr) @@ -74,12 +66,12 @@ end = struct let body = Evarutil.nf_evar sigma body in let info = Declare.Info.make () in let cinfo = - Declare.CInfo.make ~name:Id.(of_string ("catt_" ^ name)) ~typ:None () + Declare.CInfo.make ~name:(Id.of_string ("catt_" ^ name)) ~typ:None () in let gr = Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma in - Coqlib.register_ref ("catt_" ^ name) gr; + Rocqlib.register_ref Local ("catt_" ^ name) gr; let env = Global.env () in let sigma, econstr = Evd.fresh_global env sigma gr in let _ = Hashtbl.add tbl value name in @@ -138,16 +130,12 @@ end = struct (* translate a catt context into a coq lambda abstraction *) let rec ctx_to_lambda env sigma obj_type eq_type refl ctx inner_tm = match ctx with - | [] -> - ( sigma, - EConstr.mkLambda - (nameR (Names.Id.of_string "catt_Obj"), obj_type, inner_tm) ) + | [] -> (sigma, EConstr.mkLambda (anonR, obj_type, inner_tm)) | (x, (ty, _)) :: ctx -> let env, sigma, ty = ty_to_econstr env sigma obj_type eq_type refl ctx ty in - let id_lambda = Names.Id.of_string (catt_var_to_coq_name x) in - let lambda = EConstr.mkLambda (nameR id_lambda, ty, inner_tm) in + let lambda = EConstr.mkLambda (anonR, ty, inner_tm) in ctx_to_lambda env sigma obj_type eq_type refl ctx lambda (* translate a catt type into a coq type *) diff --git a/coq_plugin/src/export.mli b/rocq_plugin/src/export.mli similarity index 100% rename from coq_plugin/src/export.mli rename to rocq_plugin/src/export.mli diff --git a/coq_plugin/src/g_catt.mlg b/rocq_plugin/src/g_catt.mlg similarity index 97% rename from coq_plugin/src/g_catt.mlg rename to rocq_plugin/src/g_catt.mlg index 9c751581..c98e3374 100644 --- a/coq_plugin/src/g_catt.mlg +++ b/rocq_plugin/src/g_catt.mlg @@ -6,4 +6,4 @@ open Stdarg VERNAC COMMAND EXTEND Catt CLASSIFIED AS QUERY | [ "Catt" ne_string_list(tms) "From" "File" string(file) ] -> { Export.catt_tm file tms } -END \ No newline at end of file +END diff --git a/coq_plugin/theories/Loader.v b/rocq_plugin/theories/Loader.v similarity index 100% rename from coq_plugin/theories/Loader.v rename to rocq_plugin/theories/Loader.v diff --git a/coq_plugin/theories/Test.v b/rocq_plugin/theories/Test.v similarity index 100% rename from coq_plugin/theories/Test.v rename to rocq_plugin/theories/Test.v diff --git a/coq_plugin/theories/dune b/rocq_plugin/theories/dune similarity index 100% rename from coq_plugin/theories/dune rename to rocq_plugin/theories/dune diff --git a/web/web.ml b/web/web.ml index 321ba0b3..3851d8a3 100644 --- a/web/web.ml +++ b/web/web.ml @@ -4,7 +4,7 @@ module Dom = Js_of_ocaml.Dom module Sys_js = Js_of_ocaml.Sys_js module Html = Js_of_ocaml.Dom_html module Js = Js_of_ocaml.Js -module Firebug = Js_of_ocaml.Firebug +module Console = Js_of_ocaml.Console let doc = Html.document @@ -19,7 +19,7 @@ let button ~id txt action = b##.id := Js.string id; b -let _debug s = Firebug.console##debug (Js.string s) +let _debug s = Console.console##debug (Js.string s) let run_action s = try