adapting coq-htt to rocq-9.2/mathcomp-2.6.0

Makefile

@@ -1,4 +1,19 @@
-# -*- Makefile -*-
+# KNOWNTARGETS will not be passed along to RocqMakefile
+KNOWNTARGETS := RocqMakefile
+# KNOWNFILES will not get implicit targets from the final rule, and so depending on them won’t invoke the submake
+# Warning: These files get declared as PHONY, so any targets depending on them always get rebuilt
+KNOWNFILES := Makefile _RocqProject
 
-# --------------------------------------------------------------------
-include Makefile.common
+.DEFAULT_GOAL := invoke-rocqmakefile
+
+RocqMakefile: Makefile _RocqProject
+	$(ROCQBIN)rocq makefile -f _RocqProject -o RocqMakefile
+
+invoke-rocqmakefile: RocqMakefile
+	$(MAKE) --no-print-directory -f RocqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
+
+.PHONY: invoke-rocqmakefile $(KNOWNFILES)
+
+# This should be the last rule, to handle any targets not declared above
+%: invoke-rocqmakefile
+	@true

Makefile.common

@@ -6,12 +6,12 @@
 # pre-makefile::, this-clean:: and __always__:: may be extended      #
 # Additionally, the following variables may be customized:           #
 SUBDIRS?=
-COQBIN?=$(dir $(shell which coqtop))
-COQMAKEFILE?=$(COQBIN)coq_makefile
-COQDEP?=$(COQBIN)coqdep
-COQPROJECT?=_CoqProject
-COQMAKEOPTIONS?=
-COQMAKEFILEOPTIONS?=
+ROCQBIN?=$(dir $(shell which rocq))
+ROCQMAKEFILE?=$(ROCQBIN)rocq_makefile
+ROCQDEP?=$(ROCQBIN)rocq dep
+ROCQPROJECT?=_RocqProject
+ROCQMAKEOPTIONS?=
+ROCQMAKEFILEOPTIONS?=
 V?=
 VERBOSE?=V
 ######################################################################
@@ -22,28 +22,28 @@ VERBOSE?=V
 
 H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
-COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
-BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
+ROCQMAKE = $(MAKE) -f Makefile.rocq $(ROCQMAKEOPTIONS)
+BRANCH_rocq:= $(shell $(ROCQBIN)rocq top -v | head -1 | grep -E '(trunk|master)' \
 	      | wc -l | sed 's/ *//g')
 
-# coq version:
-ifneq "$(BRANCH_coq)" "0"
-COQVVV:= dev
+# rocq version:
+ifneq "$(BRANCH_rocq)" "0"
+ROCQVVV:= dev
 else
-COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1)
+ROCQVVV:=$(shell $(ROCQBIN)rocq top --print-version | cut -d" " -f1)
 endif
 
-COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
-COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
+ROCQV:= $(shell echo $(ROCQVVV) | cut -d"." -f1)
+ROCQVV:= $(shell echo $(ROCQVVV) | cut -d"." -f1-2)
 
 # all: ---------------------------------------------------------------
 all: config build
 
-# Makefile.coq: ------------------------------------------------------
+# Makefile.rocq: ------------------------------------------------------
 .PHONY: pre-makefile
 
-Makefile.coq: pre-makefile $(COQPROJECT) Makefile
-	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
+Makefile.rocq: pre-makefile $(ROCQPROJECT) Makefile
+	$(ROCQMAKEFILE) $(ROCQMAKEFILEOPTIONS) -f $(ROCQPROJECT) -o Makefile.rocq
 
 # Global config, build, clean and distclean --------------------------
 config: sub-config this-config
@@ -59,27 +59,27 @@ distclean: sub-distclean this-distclean
 
 this-config:: __always__
 
-this-build:: this-config Makefile.coq
-	+$(COQMAKE)
+this-build:: this-config Makefile.rocq
+	+$(ROCQMAKE)
 
 this-distclean:: this-clean
-	rm -f Makefile.coq Makefile.coq.conf Makefile.coq
+	rm -f Makefile.rocq Makefile.rocq.conf Makefile.rocq
 
 this-clean:: __always__
-	@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
+	@if [ -f Makefile.rocq ]; then $(ROCQMAKE) cleanall; fi
 
 # Install target -----------------------------------------------------
 .PHONY: install
 
-install: __always__ Makefile.coq
-	$(COQMAKE) install
-# counting lines of Coq code -----------------------------------------
+install: __always__ Makefile.rocq
+	$(ROCQMAKE) install
+# counting lines of Rocq code -----------------------------------------
 .PHONY: count
 
-COQFILES = $(shell grep '.v$$' $(COQPROJECT))
+ROCQFILES = $(shell grep '.v$$' $(ROCQPROJECT))
 
 count:
-	@coqwc $(COQFILES) | tail -1 | \
+	@rocq wc $(ROCQFILES) | tail -1 | \
 	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
 # Additionally cleaning backup (*~) files ----------------------------
 this-distclean::
@@ -95,5 +95,5 @@ sub-%: __always__
 endif
 
 # Make of individual .vo ---------------------------------------------
-%.vo: __always__ Makefile.coq
-	+$(COQMAKE) $@
+%.vo: __always__ Makefile.rocq
+	+$(ROCQMAKE) $@

coq-htt-core.opam

@@ -34,13 +34,14 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-C" "htt" "-j%{jobs}%"]
 install: [make "-C" "htt" "install"]
 depends: [
-  "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
-  "coq-mathcomp-algebra" 
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "dune" {>= "3.23"}
+  "rocq-core" { (>= "9.2" & < "9.3~") | (= "dev") }
+  "rocq-stdlib"
+  "rocq-mathcomp-ssreflect" { (>= "2.6.0" & < "2.7~") | (= "dev") }
+  "rocq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "rocq-mathcomp-algebra" 
+  "rocq-mathcomp-fingroup" 
+  "coq-fcsl-pcm" { (>= "2.3.0" & < "2.4~") | (= "dev") }
 ]
 
 tags: [

coq-htt.opam

@@ -31,12 +31,14 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
-  "dune" {>= "3.6"}
-  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
-  "coq-mathcomp-algebra" 
-  "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "dune" {>= "3.23"}
+  "rocq-core" { (>= "9.2" & < "9.3~") | (= "dev") }
+  "rocq-stdlib"
+  "rocq-mathcomp-ssreflect" { (>= "2.6.0" & < "2.7~") | (= "dev") }
+  "rocq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "rocq-mathcomp-algebra" 
+  "rocq-mathcomp-fingroup" 
+  "coq-fcsl-pcm" { (>= "2.3.0" & < "2.4~") | (= "dev") }
   "coq-htt-core" {= version}
 ]
 

examples/array.v

@@ -63,7 +63,7 @@ End ArraySig.
 Module Array : ArraySig.
 Section Array.
 Context {I : finType} {T : Type}.
-Notation array := {array I -> T}.
+Abbreviation array := {array I -> T}.
 
 (* array is specified by finite function *)
 Definition shape (a : array) (f : {ffun I -> T}) : Pred heap :=

examples/bubblesort.v

@@ -22,9 +22,6 @@ Import Order.NatOrder Order.TTheory.
 Local Open Scope order_scope.
 Local Open Scope nat_scope.
 
-(* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
-Set SsrOldRewriteGoalsOrder.  
-
 (* Brief mathematics of (bubble) array sorting: *)
 (* Theory of permutations built out of (adjacent-element) swaps acting on *)
 (* finite functions from bounded nats to ordered values. *)
@@ -128,7 +125,7 @@ Lemma codom1_ax_rcons2 (f : {ffun 'I_n.+1 -> A}) (a : itv_bound nat) (i : 'I_n)
         rcons (rcons (&:(fgraph f) (Interval a (BLeft (i : nat)))) 
               (f (Wo i))) (f (So i)).
 Proof.
-move=>H; rewrite slice_xR; last first.
+move=>H; rewrite slice_xR.
 - by apply: ltW; case: a H=>[[] ax|ab] //; rewrite !bnd_simp ltEnat /= =>/ltnW.
 by rewrite onth_codom1S /= slice_oSR codom1_ax_rcons.
 Qed.
@@ -194,7 +191,7 @@ Proof.
 move=>Hx0 Hx1.
 suff E: {in &:(enum 'I_n.+1) i, f =1 pffun (swnx x) f}.
 - by rewrite !fgraph_codom /= !codomE /= -2!slice_map /=; move/eq_in_map: E.
-move=>/= y; rewrite slice_uniq_memE /=; last by exact: enum_uniq.
+move=>/= y; rewrite slice_uniq_memE /=; first by exact: enum_uniq.
 case: i Hx0 Hx1=>i j Hx0 Hx1 /=.
 case/and3P=>_; rewrite /swnx size_enum_ord index_enum_ord =>Hy1 Hy2.
 rewrite ffunE; case: tpermP=>// Ey; move: Hy1 Hy2; rewrite {y}Ey /=.
@@ -282,7 +279,7 @@ Proof.
 move=>H; move: (perm_swnx f i).
 set f' : {ffun 'I_n.+1 -> A} := pffun (swnx i) f.
 rewrite {1}(slice_uxou (fgraph f) k.+1) {1}(slice_uxou (fgraph f') k.+1).
-by rewrite swnx_oa /=; [rewrite perm_cat2r | rewrite ltnS].
+by rewrite swnx_oa /=; [rewrite ltnS|rewrite perm_cat2r].
 Qed.
 End SwapNextEq.
 
@@ -728,13 +725,13 @@ apply: [stepE f]=>//= sw m [p][Hm Hsw]; case: decP=>H.
   - rewrite Sbo_eq.
     case: sw Hsw=>/=; case=>Ep Hf; rewrite {p}Ep ?pffunE1 in Hm *.
     (* swap happened before the call *)
-    - rewrite So_eq swnx_oa; last by rewrite ltnS; apply: ltnW.
+    - rewrite So_eq swnx_oa; first by rewrite ltnS; apply: ltnW.
       rewrite swnx_Skk /=; split=>//.
       - rewrite (@allrel_in_l _ _ _ _ &:(codom f) `]-oo, k.+1]) //.
         by apply/perm_mem; rewrite perm_sym; apply: perm_swnx_ux.
       - by rewrite ltnS leqnn.
-      rewrite allrel1r slice_oSR (slice_split (x:=ls) _ true); 
-        last by rewrite in_itv.
+      rewrite allrel1r slice_oSR (slice_split (x:=ls) _ true).
+      - by rewrite in_itv.
       rewrite /= all_cat; apply/andP; split.
       - rewrite swnx_ao //; move: Hai.
         by rewrite codom1_ax_rcons // allrel_rconsr; case/andP.
@@ -777,13 +774,13 @@ step=>Vm; exists p; case: sw Hsw=>/=; case=>Ep Hf.
     move: Hsi; rewrite codom1_ax_rcons // sorted_rconsE //=. 
     case/andP => Halsi _.
     move: Hils; rewrite leq_eqVlt; case/orP=>[/eqP <-|Hlsi] //.
-    rewrite (slice_split (x:=ls) _ true); last by rewrite in_itv.
+    rewrite (slice_split (x:=ls) _ true); first by rewrite in_itv.
     by rewrite /= all_cat Hals.
   rewrite Ep swnx_xu_cons /= (path_sortedE (@otrans A)) Hsk andbT.
   by move: Hak; rewrite codom1_ax_rcons2 // !allrel_rconsl -!andbA; case/and3P.
 (* swap didn't happen on last iteration *)
 rewrite {p}Ep pffunE1 /= in Hm *.
-rewrite (slice_split (x:=i) (i:=`[ls:nat, +oo[) _ false); last first. 
+rewrite (slice_split (x:=i) (i:=`[ls:nat, +oo[) _ false).
 - by rewrite in_itv /= andbT.
 split=>//=.
 - rewrite allrel_catr Hai /= -slice_oSL codom1_xu_cons allrel_consr.
@@ -860,7 +857,7 @@ Qed.
 Next Obligation.
 move=>a [f][] h /= E.
 apply: [gE f]=>//=.
-rewrite (@itv_overL _ _ _ +oo) /=; first by split=>//; exact: allrel0r.
+rewrite (@itv_overL _ _ _ +oo) /=; last by split=>//; exact: allrel0r.
 by rewrite leEnat addn1 size_codom /= card_ord.
 Qed.