Merge pull request #632 from mattam82/rocq-renaming

Rocq-renaming

.github/workflows/build.yml

@@ -23,39 +23,20 @@ jobs:
         coq_version: 
           - 'dev'
         ocaml_version:
-          - '4.09-flambda'
-        target: [ local, hott, dune ]
+          - '4.14.2-flambda'
+        target: [ dune ] # hott, disabled for now
       fail-fast: false
 
     steps:
 
       - name: Checkout code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
         with:
           fetch-depth: 1
 
       - name: Docker-Coq-Action
         uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-equations.opam'
+          opam_file: 'rocq-equations.opam'
           coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
-          before_script: |
-            startGroup "Workaround permission issue"
-              sudo chown -R coq:coq .  # <--
-              ocamlfind list
-            endGroup
-          script: |
-            startGroup "Build project"
-              opam exec -- ./configure.sh --enable-${{matrix.target}}
-              opam exec -- make -j 2 ci-${{matrix.target}}
-            endGroup
-          uninstall: |
-            startGroup "Clean project"
-              make clean
-            endGroup
-
-      - name: Revert permissions
-        # to avoid a warning at cleanup time
-        if: ${{ always() }}
-        run: sudo chown -R 1001:116 .  # <--

.gitignore

@@ -4,11 +4,11 @@
 *.vo
 *.vok
 *.vos
-/Makefile.coq
-/Makefile.coq.conf
+/Makefile.rocq
+/Makefile.rocq.conf
 /Makefile.hott
 /Makefile.hott.conf
-src/META.coq-equations
+src/META.rocq-equations
 *.bak
 *.cm*
 *.o
@@ -51,7 +51,6 @@ docs/_site
 .merlin
 _build
 *.install
-/test-suite/*.agdai
 /custom-HoTT/
 /examples/Makefile
 /examples/Makefile.conf

Makefile

@@ -2,12 +2,12 @@
 
 .PHONY: all default makefiles clean-makefiles
 
-all: Makefile.coq
-	$(MAKE) -f Makefile.coq
+all: Makefile.rocq
+	$(MAKE) -f Makefile.rocq
 	test -f Makefile.hott && $(MAKE) -f Makefile.hott || true
 
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
+install: Makefile.rocq
+	$(MAKE) -f Makefile.rocq install
 	test -f Makefile.hott && $(MAKE) -f Makefile.hott install || true
 
 makefiles: test-suite/Makefile examples/Makefile
@@ -16,10 +16,10 @@ clean-makefiles:
 	rm -f test-suite/Makefile examples/Makefile
 
 test-suite/Makefile: test-suite/_CoqProject
-	cd test-suite && coq_makefile -f _CoqProject -o Makefile
+	cd test-suite && rocq makefile -f _CoqProject -o Makefile
 
 examples/Makefile: examples/_CoqProject
-	cd examples && coq_makefile -f _CoqProject -o Makefile
+	cd examples && rocq makefile -f _CoqProject -o Makefile
 
 pre-all:: makefiles
 
@@ -43,7 +43,7 @@ examples: examples/Makefile all
 .PHONY: examples
 
 clean: clean-makefiles makefiles
-	$(MAKE) -f Makefile.coq clean
+	$(MAKE) -f Makefile.rocq clean
 	test -f Makefile.hott && make -f Makefile.hott clean || true
 	$(MAKE) clean-examples clean-test-suite
 
@@ -52,20 +52,20 @@ siteexamples: examples/*.glob
 
 doc: html
 	mkdir -p html/api && ocamldoc -html -d html/api \
-		`ocamlfind query -r coq-core.lib coq-core.kernel coq-core.tactics coq-core.proofs \
-			coq-core.toplevel coq-core.ltac coq-core.plugins.extraction -i-format` \
+		`ocamlfind query -r rocq-runtime.lib rocq-runtime.kernel rocq-runtime.tactics rocq-runtime.proofs \
+			rocq-runtime.toplevel rocq-runtime.ltac rocq-runtime.plugins.extraction -i-format` \
 	  -I src src/*.ml
 
 toplevel: src/equations_plugin.cma bytefiles
 	"$(OCAMLFIND)" ocamlc -linkpkg -linkall -g $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-		-package coq-core.toplevel,coq-core.plugins.extraction \
+		-package rocq-runtime.toplevel,rocq-runtime.plugins.extraction \
 	  $< $(COQLIB)/toplevel/coqtop_bin.ml -o coqtop_equations
 
 dune:-
 	dune build
 
 ci-dune:
-	opam install -j 2 -y coq-hott.dev
+	# opam install -j 2 -y coq-hott.dev
 	dune build
 
 ci-hott:
@@ -75,10 +75,10 @@ ci-hott:
 	$(MAKE) -f Makefile.hott uninstall
 
 ci-local:
-	$(MAKE) -f Makefile.coq all 
+	$(MAKE) -f Makefile.rocq all 
 	$(MAKE) test-suite examples
-	$(MAKE) -f Makefile.coq install
-	$(MAKE) -f Makefile.coq uninstall
+	$(MAKE) -f Makefile.rocq install
+	$(MAKE) -f Makefile.rocq uninstall
 
 ci: ci-local
 

Makefile.hott.local

@@ -1,2 +1,2 @@
-CAMLPKGS+=-package coq-core.plugins.extraction,coq-core.plugins.cc
+CAMLPKGS+=-package rocq-runtime.plugins.extraction,rocq-runtime.plugins.cc
 ci: all test-suite examples

Makefile.rocq.local

@@ -0,0 +1,2 @@
+CAMLPKGS+=-package rocq-runtime.plugins.extraction,rocq-runtime.plugins.cc
+ci: all test-suite examples

README.md

@@ -105,11 +105,11 @@ if you didn't do it yet:
 
 and run:
 
-    opam install coq-equations
+    opam install rocq-equations
 
 To get the beta versions of Coq, activate the repository:
 
-    opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
+    opam repo add rocq-runtime-dev https://coq.inria.fr/opam/core-dev
 
 To get the development version of Equations, activate the repository:
 
@@ -144,7 +144,7 @@ in your own directory. E.g. on Ubuntu, you would prefix the command with
 
 ## HoTT Variant
 
-The HoTT variant of Equations works with the coq-hott library for Coq 8.13 and up. When using `opam`, simply install first the `coq-hott` library and `coq-equations` will install its HoTT variant. From source, first 
+The HoTT variant of Equations works with the coq-hott library for Coq 8.13 and up. When using `opam`, simply install first the `coq-hott` library and `rocq-equations` will install its HoTT variant. From source, first 
 install `coq-hott` and then use:
 
     ./configure.sh --enable-hott

_CoqProject

@@ -1,4 +1,4 @@
-src/META.coq-equations.in
+src/META.rocq-equations.in
 -I src
 -I test-suite
 -Q src Equations

configure.sh

@@ -1,16 +1,16 @@
 #!/usr/bin/env bash
 
-rm -f Makefile.coq Makefile.hott
+rm -f Makefile.rocq Makefile.hott
 
 if [ "$1" == "--enable-hott" ]
 then
-    if command -v coqtop >/dev/null 2>&1
-    then coq_makefile -f _HoTTProject -o Makefile.hott
-    else echo "Error: coqtop not found in path"
+    if command -v rocq >/dev/null 2>&1
+    then rocq makefile -f _HoTTProject -o Makefile.hott
+    else echo "Error: rocq not found in path"
     fi
 fi
 
-if command -v coqtop >/dev/null 2>&1
-then coq_makefile -f _CoqProject -o Makefile.coq
-else echo "Error: coqtop not found in path"
+if command -v rocq >/dev/null 2>&1
+then rocq makefile -f _CoqProject -o Makefile.rocq
+else echo "Error: rocq not found in path"
 fi

doc/equations.tex

@@ -64,11 +64,11 @@ \section*{Installation}
 
 Equations is available through the
 \texttt{opam}\footnote{\url{http://opam.ocaml.org}} package manager as
-package \texttt{coq-equations}. To install it on an already existing
+package \texttt{rocq-equations}. To install it on an already existing
 \texttt{opam} installation with the \Coq repository, simply input the
 command:
 \begin{verbatim}
-# opam install coq-equations
+# opam install rocq-equations
 \end{verbatim}
 
 If you want to use it with the \href{https://github.com/HoTT/HoTT}{HoTT library for Coq}, simply install the 

doc/equations_intro.v

@@ -12,11 +12,11 @@
    session by importing the [Equations] module.  *)
 
 From Stdlib Require Import Arith Lia Program.
-From Equations Require Import Equations.
+From Equations.Prop Require Import Equations.
 
 (* begin hide *)
 Check @eq.
-Require Import Bvector.
+From Stdlib Require Import Bvector.
 
 (* Derive DependentElimination for nat bool option sum Datatypes.prod list *)
 (* end hide *)

doc/manual.tex

@@ -376,7 +376,7 @@ \section{Changes}
   \begin{itemize}
   \item \textbf{Incompatible change} Support for the Coq-HoTT library, out of the box. This required a slight reorganization 
     of the directories. To use this, simply install the \texttt{opam} \texttt{coq-hott} package before 
-    \texttt{coq-equations} and \[\texttt{From Equations.HoTT Require Import All}\]
+    \texttt{rocq-equations} and \[\texttt{From Equations.HoTT Require Import All}\]
     Now \[\texttt{Require Import Equations.Equations}\] no longer works, 
     use \texttt{Require Import Equations.Prop.Equations} (absolute path, future-proof) or 
     \texttt{From Equations Require Import Equations} (relative path) to use the 

dune-project

@@ -1,5 +1,38 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.13)
+(using coq 0.8)
+(name rocq-equations)
+(source (github mattam82/Coq-Equations))
+(license LGPL-2.1-only)
+(authors "Matthieu Sozeau <[email protected]>"  "Cyprien Mangin <[email protected]>")
+(maintainers "Matthieu Sozeau <[email protected]>")
+(homepage "https://mattam82.github.io/Coq-Equations")
 
-(name coq-equations)
+(package 
+ (name rocq-equations)
+ (synopsis "A function definition package for Rocq")
+ (description "Equations is a function definition plugin for Rocq, that allows the \
+  definition of functions by dependent pattern-matching and well-founded, \
+  mutual or nested structural recursion and compiles them into core \
+  terms. It automatically derives the clauses equations, the graph of the \
+  function and its associated elimination principle.")
+ (tags ("keyword:dependent pattern-matching"
+  "keyword:functional elimination"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:Equations"))
+ (depends
+   (ocaml (>= 4.10.0))
+   (rocq-prover (>= "9.0~"))
+   (ppx_optcomp :build)
+   (ocaml-lsp-server :with-dev-setup)))
 
+(package
+ (name rocq-equations-examples)
+ (synopsis "Examples")
+ (description "Do not install")
+ (depends rocq-equations))
+
+(package
+ (name rocq-equations-tests)
+ (synopsis "Technical package to run tests")
+ (description "Do not install")
+ (depends rocq-equations))

examples/AlmostFull.v

@@ -1,16 +1,20 @@
-From Equations Require Import Equations.
+From Equations.Prop Require Import Equations.
+
 Require Import Examples.Fin.
-Require Import Relations Utf8.
-Require Import Relations Wellfounded.
-Require Import Setoid RelationClasses Morphisms.
-Require Import Lia.
-Require Import Bool.
-Require Import List Arith String.
+From Stdlib Require Import Relations Utf8.
+From Stdlib Require Import Relations Wellfounded.
+From Stdlib Require Import Setoid RelationClasses Morphisms.
+From Stdlib Require Import Lia.
+From Stdlib Require Import Bool.
+From Stdlib Require Import List Arith String.
 From Stdlib Require Import FunctionalExtensionality.
 
 Set Equations Transparent.
 Set Keyed Unification.
 Set Asymmetric Patterns.
+Local Set Firstorder Solver auto with arith core datatypes.
+
+Ltac intuition_solver ::= auto with *.
 
 Section Equality.
   Class Eq (A : Type) :=
@@ -448,7 +452,7 @@ Section OplusUnary.
 
 End OplusUnary.
 
-Set Firstorder Solver auto.
+Local Set Firstorder Solver auto.
 
 (* Lemma oplus_unary_sec_intersection {X} (p q : WFT X) *)
 (*       (C : X -> X -> Prop) (A B : X -> Prop) : *)
@@ -609,7 +613,7 @@ Ltac destruct_pairs := repeat
   | [ x : _ /\ _ |- _ ] => destruct x
 end.
 
-Require Import ssreflect.
+From Stdlib Require Import ssreflect.
 
 Section SCT.
 
@@ -1352,7 +1356,7 @@ Print Assumptions size_change_wf.
 Print Assumptions size_change_termination.
 
 Definition R := product_rel Nat.le Nat.le.
-Require Import Lia.
+From Stdlib Require Import Lia.
 
 Derive Signature for clos_trans_1n.
 
@@ -1390,7 +1394,7 @@ Definition gnlex : (nat * nat) -> nat.
   red. simpl. red. compute. simpl. intuition lia. red. simpl. compute. intuition lia.
 Defined.
 
-Require Import ExtrOcamlBasic.
+From Stdlib Require Import ExtrOcamlBasic.
 (* Extraction gnlex.
 Print Assumptions gnlex. *)