Fix deprecations for Rocq 9 (#826)

* Fix deprecations for Rocq 9

* Update CI

* Use user-contrib [opam] for InteractionTrees, paco, ext-lib; adjust CI; update bundled CompCert

* Put InteractionTree back as submodule

* Tweak CI

* closes #836
closes #839
closes #840

* Bring 32-bit tests up to date

* Brought FCF submodule up to date

* Improved a makefile dependency

Author: andrew-appel

.github/workflows/coq-action.yml

@@ -21,19 +21,12 @@ jobs:
         # except for the "make_target" field and make_target related excludes
         coq_version:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
-          - '8.19'
-          - '8.20'
           - 'dev'
         bit_size:
           - 32
           - 64
         make_target:
           - vst
-        exclude:   
-          - coq_version: 8.19
-            bit_size: 32
-          - coq_version: dev
-            bit_size: 32
     steps:
       - uses: actions/checkout@v4
         with:
@@ -53,6 +46,7 @@ jobs:
               opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13.1' || 'coq-compcert.3.13.1' }}
               # Required by test2
               opam install -y coq-ext-lib
+              opam install -y coq-paco
             endGroup
           # See https://github.com/coq-community/docker-coq-action/tree/v1#permissions
           before_script: |
@@ -88,8 +82,6 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.19'
-          - '8.20'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -102,10 +94,6 @@ jobs:
           - 32
           - 64
         exclude:
-          - coq_version: 8.19
-            bit_size: 32
-          - coq_version: dev
-            bit_size: 32
           - bit_size: 64
             make_target: test3
           - bit_size: 32

InteractionTrees

@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 or-else 8.20.1
+COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 or-else 8.20.1 or-else 9.0.0 orelse 9.1.0 or-else 9.2+alpha
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)
@@ -303,6 +303,7 @@ CGFLAGS =  -DCOMPCERT -short-idents
 
 # ##### Interaction Trees Flags #####
 
+# as of 1 July 2025, coq-itree package seems not compatible with rocq 9.2+alpha, so still using submodule
 ifneq ($(wildcard InteractionTrees/theories),)
 EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
 endif
@@ -315,9 +316,10 @@ endif#
 
 # ##### PaCo (Parameterized Coinduction) Flags #####
 
-ifneq ($(wildcard paco/src),)
-EXTFLAGS:=$(EXTFLAGS) -Q paco/src Paco
-endif
+# the following commented out, because we get from opam instead of submodules
+# ifneq ($(wildcard paco/src),)
+# EXTFLAGS:=$(EXTFLAGS) -Q paco/src Paco
+# endif
 
 # ##### SSReflect Flags #####
 
@@ -327,7 +329,10 @@ endif
 
 # ##### Flag summary #####
 
-COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../paco/src Paco -Q ../coq-ext-lib/theories ExtLib -Q ../fcf/src/fcf FCF
+COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../fcf/src/fcf FCF
+
+# old version with paco, coq-ext-lib; we now obtain these from opam environment instead of submodules
+# COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../paco/src Paco -Q ../coq-ext-lib/theories ExtLib -Q ../fcf/src/fcf FCF
 
 
 DEPFLAGS:=$(COQFLAGS)
@@ -829,7 +834,7 @@ VST.config:
 
 # Note: doc files are installed into the coq destination folder.
 # This is not ideal but otherwise it gets tricky to handle variants
-install: VST.config
+install: VST.config vst
 	install -d "$(INSTALLDIR)"
 	for d in $(sort $(dir $(INSTALL_FILES) $(EXTRA_INSTALL_FILES))); do install -d "$(INSTALLDIR)/$$d"; done
 	for f in $(INSTALL_FILES); do install -m 0644 $$f "$(INSTALLDIR)/$$(dirname $$f)"; done
@@ -923,15 +928,16 @@ endif
 # ifneq ($(wildcard coq-ext-lib/theories),)
 # 	$(COQDEP) -Q coq-ext-lib/theories ExtLib coq-ext-lib/theories >>.depend
 # endif
+
 ifneq ($(wildcard InteractionTrees/theories),)
-#	$(COQDEP) -Q coq-ext-lib/theories ExtLib -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
-	$(COQDEP) -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
+	$(COQDEP) -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
 endif
+# the following commented out, because we get from opam instead of submodules
+# ifneq ($(wildcard paco/src),)
+# 	$(COQDEP) -Q paco/src Paco paco/src/*.v >>.depend
+# endif
 ifneq ($(wildcard fcf/src/FCF),)
 	$(COQDEP) -Q fcf/src/FCF FCF fcf/src/FCF/*.v >>.depend
-endif
-ifneq ($(wildcard paco/src),)
-	$(COQDEP) -Q paco/src Paco paco/src/*.v >>.depend
 endif
 	wc .depend
 

Makefile

@@ -134,7 +134,7 @@ ifdef CLIGHTGEN
 VERSION1= $(lastword $(shell $(CLIGHTGEN) --version))
 VERSION2= $(subst version=,,$(shell grep version $(COMPCERT_SRC_DIR)/VERSION))
 ifneq ($(VERSION1),$(VERSION2))
-$(warning clightgen version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2))
+$(warning $(CLIGHTGEN) version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2))
 endif
 endif
 

Makefile.bundled

@@ -37,7 +37,7 @@ Qed.
 Lemma repeat_op_table_nat_length: forall {T: Type} (i: nat) (x: T) (f: T -> T),
   length (repeat_op_table_nat i x f) = i.
 Proof.
-  intros. induction i. reflexivity. simpl. rewrite app_length. simpl.
+  intros. induction i. reflexivity. simpl. rewrite length_app. simpl.
   rewrite IHi. lia.
 Qed.
 

aes/list_utils.v

@@ -1,6 +1,6 @@
 (* SC atomics without importing Iris *)
 
-Require Import Ensembles.
+From Stdlib Require Import Ensembles.
 Require Import VST.veric.rmaps.
 Require Import VST.veric.compcert_rmaps.
 Require Import VST.concurrency.ghosts.

atomics/SC_atomics_base.v

@@ -1098,7 +1098,7 @@ Proof.
       rewrite Z2Nat.inj_add, repeat_plus by omega; simpl.
       rewrite !combine_app, map_app, sepcon_app; simpl.
       unfold atomic_entry, atomic_loc_hist; entailer!.
-      { rewrite combine_length, repeat_length, Zlength_correct, Nat2Z.id, Nat.min_l; auto.
+      { rewrite length_combine, repeat_length, Zlength_correct, Nat2Z.id, Nat.min_l; auto.
         apply Nat2Z.inj_le; rewrite <- !Zlength_correct; omega. }
       { apply Nat2Z.inj; rewrite <- !Zlength_correct; omega. }
   - Intros entries ghosts.

atomics/verif_hashtable1.v

@@ -6,7 +6,7 @@ SHAREDIR=$(PREFIX)/share
 COQDEVDIR=$(PREFIX)/lib/compcert/coq
 OCAML_NATIVE_COMP=true
 OCAML_OPT_COMP=true
-MENHIR_DIR=/Users/appel/.opam/coq8.19/lib/menhirLib
+MENHIR_DIR=/Users/appel/.opam/CP.2024.10.1~8.20~2025.01/lib/menhirLib
 COMPFLAGS=-bin-annot
 ABI=apple
 ARCH=aarch64
@@ -31,4 +31,4 @@ MODEL=default
 SYSTEM=macos
 RESPONSEFILE=gnu
 LIBRARY_FLOCQ=external
-LIBRARY_MENHIRLIB=local
+LIBRARY_MENHIRLIB=external

compcert/Makefile.config

@@ -1,4 +1,4 @@
-version=3.15
+version=3.16
 buildnr=
 tag=
 branch=

compcert/VERSION

@@ -361,7 +361,7 @@ Variable e: env.
 Variable le: temp_env.
 Variable m: mem.
 
-(** [eval_expr ge e m a v] defines the evaluation of expression [a]
+(** [eval_expr ge e le m a v] defines the evaluation of expression [a]
   in r-value position.  [v] is the value of the expression.
   [e] is the current environment and [m] is the current memory state. *)