From f14ddfcad8bfe1a55d277aeffeea6a1dce441b19 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 1 Apr 2026 07:25:49 -0500 Subject: [PATCH 1/3] Use _RocqProject --- .gitignore | 2 +- Makefile | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.gitignore b/.gitignore index 7ce477f4..db9d492b 100644 --- a/.gitignore +++ b/.gitignore @@ -22,5 +22,5 @@ *.v.d *.glob .coqdeps.d -_CoqProject +_RocqProject .lia.cache diff --git a/Makefile b/Makefile index 4ab675c7..42eefa04 100644 --- a/Makefile +++ b/Makefile @@ -10,7 +10,7 @@ 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) > $@ + @coqdep -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 $@ + @coqc $(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: From 227d7a553fee4e214b8089e2460dd052dd5a05aa Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 1 Apr 2026 07:34:31 -0500 Subject: [PATCH 2/3] Modernize CI workflow --- .github/workflows/coq-action.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index f1439896..f28cc3c2 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -16,17 +16,17 @@ 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: From 463725dfc3a257d0d1fc6e11e83c4f063269b11c Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 1 Apr 2026 07:58:57 -0500 Subject: [PATCH 3/3] Fix all deprecation warnings and modernize build - Replace From Coq with From Stdlib across all source files - Add From Stdlib prefix to bare Require of Stdlib modules - Replace deprecated app_length/firstn_length with length_app/length_firstn - Replace deprecated intuition (auto with *) with intuition auto - Replace deprecated Cd command with Set Extraction Output Directory - Switch from coqc/coqdep to rocq compile/rocq dep - Add deprecation warning-as-error flags to COQARGS - Update submodules (coq-classes, coq-tactical, coq-array) with same fixes - Update CI: coq_version with dev/latest, UID 1000 permissions Co-Authored-By: Claude Opus 4.6 (1M context) --- .github/workflows/coq-action.yml | 2 +- Makefile | 6 +++--- logging-client/Extract.v | 12 +++++------- src/Examples/Logging/LogEncoding.v | 2 +- src/Examples/Logging/LogicalLog.v | 4 ++-- src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v | 2 +- src/Examples/StatDb/Impl.v | 4 ++-- src/Helpers/Disk.v | 2 +- src/Helpers/Maybe.v | 8 ++++---- src/Helpers/RelationAlgebra.v | 4 ++-- src/Lib.v | 8 ++++---- src/Spec/Proc.v | 2 +- src/Spec/ProcTheorems.v | 4 ++-- vendor/array | 2 +- vendor/classes | 2 +- vendor/tactical | 2 +- 16 files changed, 32 insertions(+), 34 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index f28cc3c2..58f35359 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -32,7 +32,7 @@ jobs: after_install: before_script: | startGroup "Workaround permission issue" - sudo chown -R coq:coq . + sudo chown -R 1000:1000 . endGroup script: | startGroup "Build project" diff --git a/Makefile b/Makefile index 42eefa04..4df3ad62 100644 --- a/Makefile +++ b/Makefile @@ -4,7 +4,7 @@ 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) @@ -25,7 +25,7 @@ _RocqProject: libname $(wildcard vendor/*) .coqdeps.d: $(ALL_VFILES) _RocqProject @echo "COQDEP $@" - @coqdep -f _RocqProject $(ALL_VFILES) > $@ + @rocq dep -f _RocqProject $(ALL_VFILES) > $@ ifneq ($(MAKECMDGOALS), clean) -include .coqdeps.d @@ -33,7 +33,7 @@ endif %.vo: %.v _RocqProject @echo "COQC $<" - @coqc $(COQARGS) $(shell cat '_RocqProject') $< -o $@ + @rocq compile $(COQARGS) $(shell cat '_RocqProject') $< -o $@ extract: logging-client/extract/ComposedRefinement.hs diff --git a/logging-client/Extract.v b/logging-client/Extract.v index 00bcb53a..f86b2f89 100644 --- a/logging-client/Extract.v +++ b/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 "../../". diff --git a/src/Examples/Logging/LogEncoding.v b/src/Examples/Logging/LogEncoding.v index aced0f03..2cad9800 100644 --- a/src/Examples/Logging/LogEncoding.v +++ b/src/Examples/Logging/LogEncoding.v @@ -1,4 +1,4 @@ -Require Import Arith. +From Stdlib Require Import Arith. Require Import Disk. Set Implicit Arguments. diff --git a/src/Examples/Logging/LogicalLog.v b/src/Examples/Logging/LogicalLog.v index 45775bc4..2db56652 100644 --- a/src/Examples/Logging/LogicalLog.v +++ b/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). diff --git a/src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v b/src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v index b2a932bd..a33d7162 100644 --- a/src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v +++ b/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. diff --git a/src/Examples/StatDb/Impl.v b/src/Examples/StatDb/Impl.v index 7cef0155..07390cc3 100644 --- a/src/Examples/StatDb/Impl.v +++ b/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. diff --git a/src/Helpers/Disk.v b/src/Helpers/Disk.v index 09bf8899..12609231 100644 --- a/src/Helpers/Disk.v +++ b/src/Helpers/Disk.v @@ -1,4 +1,4 @@ -Require Extraction. +From Stdlib Require Extraction. From Classes Require Import Classes. From Array Require Export Array. diff --git a/src/Helpers/Maybe.v b/src/Helpers/Maybe.v index 2bd79a91..447e0052 100644 --- a/src/Helpers/Maybe.v +++ b/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. diff --git a/src/Helpers/RelationAlgebra.v b/src/Helpers/RelationAlgebra.v index 49df11cb..992d6724 100644 --- a/src/Helpers/RelationAlgebra.v +++ b/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. diff --git a/src/Lib.v b/src/Lib.v index 2accf583..083cf014 100644 --- a/src/Lib.v +++ b/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. diff --git a/src/Spec/Proc.v b/src/Spec/Proc.v index 6c515c54..fae0a21d 100644 --- a/src/Spec/Proc.v +++ b/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. diff --git a/src/Spec/ProcTheorems.v b/src/Spec/ProcTheorems.v index 607ee6ad..bc3673a2 100644 --- a/src/Spec/ProcTheorems.v +++ b/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. diff --git a/vendor/array b/vendor/array index 951c6d79..ae626632 160000 --- a/vendor/array +++ b/vendor/array @@ -1 +1 @@ -Subproject commit 951c6d792b96369a6c626c6e40e99ef30f42f7e9 +Subproject commit ae626632601c347a5471ac2cdab45e8de45dd5fd diff --git a/vendor/classes b/vendor/classes index e74411c6..c4086f8c 160000 --- a/vendor/classes +++ b/vendor/classes @@ -1 +1 @@ -Subproject commit e74411c6c3efc9122915d69be52e4fcd0bbdf2c3 +Subproject commit c4086f8ca76a1508faf9742bcd36f689330fadbd diff --git a/vendor/tactical b/vendor/tactical index 544ef403..3c96e91c 160000 --- a/vendor/tactical +++ b/vendor/tactical @@ -1 +1 @@ -Subproject commit 544ef4033ac9467876e8dc77ce2063a48cdbf97a +Subproject commit 3c96e91cd9a7dde2296e25f32b46e1444c078379