Fix deprecation warnings and modernize build

.github/workflows/coq-action.yml

@@ -16,23 +16,23 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        image:
-          - "coqorg/coq:dev"
-          - "coqorg/coq:8.20"
+        coq_version:
+          - "dev"
+          - "latest"
       fail-fast: false
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v6
         with:
           submodules: true
       - uses: coq-community/docker-coq-action@v1
         with:
-          custom_image: ${{ matrix.image }}
+          coq_version: ${{ matrix.coq_version }}
           before_install:
           install:
           after_install:
           before_script: |
             startGroup "Workaround permission issue"
-              sudo chown -R coq:coq .
+              sudo chown -R 1000:1000 .
             endGroup
           script: |
             startGroup "Build project"

.gitignore

@@ -22,5 +22,5 @@
 *.v.d
 *.glob
 .coqdeps.d
-_CoqProject
+_RocqProject
 .lia.cache

Makefile

@@ -4,13 +4,13 @@ TEST_VFILES := $(shell find 'src' -name "*Tests.v")
 PROJ_VFILES := $(shell find 'src' -name "*.v")
 VFILES := $(filter-out $(TEST_VFILES),$(PROJ_VFILES))
 
-COQARGS :=
+COQARGS := -w +deprecated-since-8.8,+deprecated-since-8.17,+deprecated-since-8.20,+deprecated-since-9.0,-deprecated-transitive-library-file-since-9.0
 
 all: coq extract
 coq: $(VFILES:.v=.vo)
 test: $(TEST_VFILES:.v=.vo) $(VFILES:.v=.vo)
 
-_CoqProject: libname $(wildcard vendor/*)
+_RocqProject: libname $(wildcard vendor/*)
 	@echo "-R src $$(cat libname)" > $@
 	@for libdir in $(wildcard vendor/*); do \
 	libname=$$(cat $$libdir/libname); \
@@ -20,20 +20,20 @@ _CoqProject: libname $(wildcard vendor/*)
 	fi; \
 	echo "-R $$libdir/src $$(cat $$libdir/libname)" >> $@; \
 	done
-	@echo "_CoqProject:"
+	@echo "_RocqProject:"
 	@cat $@
 
-.coqdeps.d: $(ALL_VFILES) _CoqProject
+.coqdeps.d: $(ALL_VFILES) _RocqProject
 	@echo "COQDEP $@"
-	@coqdep -f _CoqProject $(ALL_VFILES) > $@
+	@rocq dep -f _RocqProject $(ALL_VFILES) > $@
 
 ifneq ($(MAKECMDGOALS), clean)
 -include .coqdeps.d
 endif
 
-%.vo: %.v _CoqProject
+%.vo: %.v _RocqProject
 	@echo "COQC $<"
-	@coqc $(COQARGS) $(shell cat '_CoqProject') $< -o $@
+	@rocq compile $(COQARGS) $(shell cat '_RocqProject') $< -o $@
 
 extract: logging-client/extract/ComposedRefinement.hs
 
@@ -46,7 +46,7 @@ clean:
 	@find $(SRC_DIRS) -name ".*.aux" -exec rm {} \;
 	@echo "CLEAN extraction"
 	@rm -rf logging-client/extract/*.hs
-	rm -f _CoqProject .coqdeps.d
+	rm -f _RocqProject .coqdeps.d
 
 .PHONY: all coq test clean extract
 .DELETE_ON_ERROR:

logging-client/Extract.v

@@ -1,18 +1,16 @@
-Cd "logging-client/extract/".
-
-From Coq Require Extraction.
-Require Import ExtrHaskellNatInteger.
-Require Import ExtrHaskellBasic.
+From Stdlib Require Extraction.
+From Stdlib Require Import ExtrHaskellNatInteger.
+From Stdlib Require Import ExtrHaskellBasic.
 
 From RecoveryRefinement Require Import Examples.Logging.Impl.
 From RecoveryRefinement Require Import Examples.Logging.ComposedRefinement.
 
 Extraction Language Haskell.
 
+Set Extraction Output Directory "logging-client/extract".
+
 Extract Constant Impl.LogHdr_fmt => "logHdrFmt".
 Extract Constant Impl.Descriptor_fmt => "descriptorFmt".
 
 Import LoggingTwoDiskRefinement.
 Separate Extraction compile init recover.
-
-Cd "../../".

src/Examples/Logging/LogEncoding.v

@@ -1,4 +1,4 @@
-Require Import Arith.
+From Stdlib Require Import Arith.
 Require Import Disk.
 
 Set Implicit Arguments.

src/Examples/Logging/LogicalLog.v

@@ -158,7 +158,7 @@ Proof.
   intros ps ls a v s Hphy Hlog Hcommit_false pf.
   pose proof (logd_log_bounds Hlog).
   constructor; simpl; eauto.
-  - rewrite app_length; simpl.
+  - rewrite length_app; simpl.
     rewrite (logd_loglen ltac:(eassumption)); auto.
   - intros.
     pose proof (logd_log_contents Hlog (i:=i)).
@@ -223,7 +223,7 @@ Proof.
   intros ps ls s Hphy Hlog Hcommit_false hdr desc log_values Hcommit.
   exists (firstn hdr.(log_length) (zip desc log_values)).
   constructor; eauto.
-  - rewrite firstn_length.
+  - rewrite length_firstn.
     rewrite zip_length1; autorewrite with length; auto.
     rewrite Nat.min_l; auto.
     apply hdr.(log_length_ok).

src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v

@@ -796,7 +796,7 @@ Module ReplicatedDisk.
         simplify; finish.
         destruct r; step.
         lia.
-      * split; [intuition; eauto; try lia|].
+      * split; [intuition auto; eauto; try lia|].
         simplify; finish.
         destruct r.
         ** spec_intros. simpl in H3. destruct H3.

src/Examples/StatDb/Impl.v

@@ -1,5 +1,5 @@
-From Coq Require Import List.
-From Coq Require Import Arith.
+From Stdlib Require Import List.
+From Stdlib Require Import Arith.
 
 From RecoveryRefinement Require Export Lib.
 

src/Helpers/Disk.v

@@ -1,4 +1,4 @@
-Require Extraction.
+From Stdlib Require Extraction.
 From Classes Require Import Classes.
 From Array Require Export Array.
 

src/Helpers/Maybe.v

@@ -1,7 +1,7 @@
-Require Import Arith.
-Require Import Bool.
-Require Import List.
-Require Import EquivDec.
+From Stdlib Require Import Arith.
+From Stdlib Require Import Bool.
+From Stdlib Require Import List.
+From Stdlib Require Import EquivDec.
 
 Set Implicit Arguments.
 (** * [maybe_holds] predicate.

src/Helpers/RelationAlgebra.v

@@ -1,5 +1,5 @@
-Require Import Setoid.
-Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import Morphisms.
 
 Require Import Tactical.Propositional.
 Require Import Tactical.Misc.

src/Lib.v

@@ -1,7 +1,7 @@
-From Coq Require Export List.
-From Coq Require Export Lia.
-From Coq Require Export Compare_dec.
-From Coq Require Export Arith.
+From Stdlib Require Export List.
+From Stdlib Require Export Lia.
+From Stdlib Require Export Compare_dec.
+From Stdlib Require Export Arith.
 
 From Classes Require Export Classes.
 Require Export Helpers.RelationAlgebra.

src/Spec/Proc.v

@@ -1,5 +1,5 @@
 Require Import Helpers.RelationAlgebra.
-Require Import List.
+From Stdlib Require Import List.
 
 Global Set Implicit Arguments.
 Global Generalizable Variables T R Op State.

src/Spec/ProcTheorems.v

@@ -1,5 +1,5 @@
-Require Import Setoid.
-Require Import Morphisms.
+From Stdlib Require Import Setoid.
+From Stdlib Require Import Morphisms.
 Require Import Proc.
 From Classes Require Import Classes.
 Require Import Helpers.RelationAlgebra.