Skip to content

Full support for Rocq 9.2 #587

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
xavierleroy merged 10 commits into from
Jul 21, 2026
Merged

Full support for Rocq 9.2 #587

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
0ccfd43
Build system: call `rocq` if available, instead of `coqc`, etc
xavierleroy Jun 11, 2026
f5a45f0
GHA CI: update `latest` action to Rocq 9.2.0
xavierleroy Jun 11, 2026
f59ceb0
Explicit declaration of proof hints databases using `Create Hintdb`
xavierleroy Jun 13, 2026
4710ec0
Rewrite `Proof (term)` as `Proof. exact (term). Qed.`
xavierleroy Jun 13, 2026
33244f8
Put postfix notations at level 1
xavierleroy Jun 13, 2026
e1e0d42
Avoid `try (rewrite H; auto)` when `H` may not be an equality
xavierleroy Jun 14, 2026
b7e9f97
Memory.v: use more portable lemmas from ZArith
xavierleroy Jun 14, 2026
0697626
Makefile: update warning options for Rocq 9.2
xavierleroy Jun 14, 2026
73af265
MenhirLib/Interpreter.v: reintroduce `Declare Scope` and re-enable wa…
xavierleroy Jun 14, 2026
844b397
Notations `#1` and `#2` (for `fst` and `snd`) moved to Coqlib
xavierleroy Jul 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/workflows/latest.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,15 +19,15 @@ jobs:
opamroot: /home/rocq/.opam
configopts: -ignore-coq-version
container:
image: rocq/rocq-prover:9.1.1
image: rocq/rocq-prover:9.2.0
options: --user root
steps:
- name: Checkout
uses: actions/checkout@v6
with:
submodules: true
- name: OPAM dependencies
run: tools/runner.sh opam_install coq menhir
run: tools/runner.sh opam_install rocq-prover menhir
- name: Configure
run: tools/runner.sh configure
- name: Build
Expand Down
61 changes: 43 additions & 18 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,33 +51,53 @@ endif
# unused-pattern-matching-variable:
# warning introduced in 8.13
# the code rewrite that avoids the warning is not desirable
# undeclared-scope:
# warning introduced in 8.12, addressed in the main CompCert files
# triggered by MenhirLib, to be solved upstream
# deprecated-instance-without-locality:
# warning introduced in 8.14
# triggered by Menhir-generated files, to be solved upstream in Menhir
# deprecated-since-8.19
# deprecated-since-8.20
# deprecated-reference-since-9.0
# deprecated-reference-since-9.1
# renamings performed in Coq's standard library;
# using the new names would break compatibility with earlier Coq versions.
# deprecated-from-Coq
# Rocq wants "From Stdlib Require" while Coq wants "From Coq Require".

# register-all
# Rocq 9.2 warns on inductive datatypes that recurse through list or prod
# notation-for-abbreviation
# The warning and the `Abbreviation` keyword needed to fix it
# were both introduced in Rocq 9.2.
# implicit-create-rewrite-hint-db
# The warning and the `Create Rewrite Hintdb` command needed to fix it
# were both introduced in Rocq 9.2.
# deprecated-end-tac
# Warning introduced in Rocq 9.2, should go away in later Rocq versions
COQCOPTS ?= \
-w -unused-pattern-matching-variable \
-w -deprecated-since-8.19 \
-w -deprecated-since-8.20 \
-w -deprecated-from-Coq
-w -deprecated-reference-since-9.0 \
-w -deprecated-reference-since-9.1 \
-w -deprecated-from-Coq \
-w -register-all \
-w -notation-for-abbreviation \
-w -implicit-create-rewrite-hint-db \
-w -deprecated-end-tac

cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
# deprecated-instance-without-locality:
# warning introduced in 8.14

@SkySkimmer SkySkimmer Jul 28, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

and removed in 8.18, with the default locality changing

# triggered by Menhir-generated files, to be solved upstream in Menhir
# deprecated-exact-proof:
# warning introduced in 9.2
# triggered by Menhir-generated files, to be solved upstream in Menhir

cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality -w -deprecated-exact-proof

# Flocq and Menhirlib run into other renaming issues.
# These warnings can only be addressed upstream.

flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
flocq/%.vo MenhirLib/%.vo: COQCOPTS+=\
-w -deprecated-syntactic-definition \
-w -deprecated-since-9.0 \
-w -deprecated-since-9.1 \
-w -deprecated-since-9.2

# For the extraction phase, we silence other warnings:
# change-dir-deprecated:
Expand Down Expand Up @@ -113,11 +133,16 @@ ifneq (,$(PROFILING))
endif
PROFILE_ZIP ?= true

COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) $(COQEXTRACTOPTS) -batch -load-vernac-source
COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
ifeq ($(USE_ROCQ),true)
COQCOMMAND="$(COQBIN)rocq" $(2)
else
COQCOMMAND="$(COQBIN)$(1)"
endif

COQC=$(call COQCOMMAND,coqc,compile) -q $(COQINCLUDES) $(COQCOPTS)
COQDEP=$(call COQCOMMAND,coqdep,dep) $(COQINCLUDES)
COQEXEC=$(call COQCOMMAND,coqtop,repl) $(COQINCLUDES) $(COQEXTRACTOPTS) -batch -load-vernac-source
COQCHK=$(call COQCOMMAND,coqchk,check) $(COQINCLUDES)
COQ2HTML=coq2html
MENHIR=menhir
CP=cp
Expand Down Expand Up @@ -311,7 +336,7 @@ latexdoc:

%.vo: %.v
@rm -f doc/$(*F).glob
@echo "COQC $*.v"
@echo "CROCQ $*.v"
@$(COQC) $*.v
@$(PROFILE_ZIP)

Expand Down
4 changes: 2 additions & 2 deletions MenhirLib/Interpreter.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,8 +82,8 @@ CoInductive buffer : Type :=
Buf_cons { buf_head : token; buf_tail : buffer }.

(* Note: Coq 8.12.0 wants a Declare Scope command,
but this breaks compatibility with Coq < 8.10.
Declare Scope buffer_scope. *)
but this breaks compatibility with Coq < 8.10. *)
Declare Scope buffer_scope.
Delimit Scope buffer_scope with buf.
Bind Scope buffer_scope with buffer.

Expand Down
6 changes: 3 additions & 3 deletions aarch64/Asmgenproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,18 +37,18 @@ Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).
Proof. exact (Genv.find_symbol_match TRANSF). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
Proof. exact (Genv.senv_match TRANSF). Qed.

Lemma functions_translated:
forall b f,
Genv.find_funct_ptr ge b = Some f ->
exists tf,
Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSF).
Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.

Lemma functions_transl:
forall fb f tf,
Expand Down
6 changes: 3 additions & 3 deletions arm/Asmgenproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,18 +39,18 @@ Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).
Proof. exact (Genv.find_symbol_match TRANSF). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
Proof. exact (Genv.senv_match TRANSF). Qed.

Lemma functions_translated:
forall b f,
Genv.find_funct_ptr ge b = Some f ->
exists tf,
Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSF).
Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.

Lemma functions_transl:
forall fb f tf,
Expand Down
12 changes: 6 additions & 6 deletions backend/Allocation.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -407,11 +407,11 @@ Module OrderedEquation <: OrderedType.
(OrderedLoc.lt (eloc x) (eloc y) \/ (eloc x = eloc y /\
OrderedEqKind.lt (ekind x) (ekind y)))).
Lemma eq_refl : forall x : t, eq x x.
Proof (@eq_refl t).
Proof. exact (@eq_refl t). Qed.
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@eq_sym t).
Proof. exact (@eq_sym t). Qed.
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@eq_trans t).
Proof. exact (@eq_trans t). Qed.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
unfold lt; intros.
Expand Down Expand Up @@ -469,11 +469,11 @@ Module OrderedEquation' <: OrderedType.
(Plt (ereg x) (ereg y) \/ (ereg x = ereg y /\
OrderedEqKind.lt (ekind x) (ekind y)))).
Lemma eq_refl : forall x : t, eq x x.
Proof (@eq_refl t).
Proof. exact (@eq_refl t). Qed.
Lemma eq_sym : forall x y : t, eq x y -> eq y x.
Proof (@eq_sym t).
Proof. exact (@eq_sym t). Qed.
Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Proof (@eq_trans t).
Proof. exact (@eq_trans t). Qed.
Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof.
unfold lt; intros.
Expand Down
8 changes: 4 additions & 4 deletions backend/Allocproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1790,25 +1790,25 @@ Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).
Proof. exact (Genv.find_symbol_match TRANSF). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
Proof. exact (Genv.senv_match TRANSF). Qed.

Lemma functions_translated:
forall (v: val) (f: RTL.fundef),
Genv.find_funct ge v = Some f ->
exists tf,
Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_transf_partial TRANSF).
Proof. exact (Genv.find_funct_transf_partial TRANSF). Qed.

Lemma function_ptr_translated:
forall (b: block) (f: RTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists tf,
Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSF).
Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.

Lemma sig_function_translated:
forall f tf,
Expand Down
2 changes: 2 additions & 0 deletions backend/Asmgenproof0.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ Require Import Conventions.

(** * Processor registers and register states *)

Create HintDb asmgen.
Global Hint Extern 2 (_ <> _) => congruence: asmgen.

Lemma ireg_of_eq:
Expand Down Expand Up @@ -746,6 +747,7 @@ Qed.
Definition nolabel (i: instruction) :=
match i with Plabel _ => False | _ => True end.

Create HintDb labels.
Global Hint Extern 1 (nolabel _) => exact I : labels.

Lemma tail_nolabel_cons:
Expand Down
1 change: 1 addition & 0 deletions backend/CSEdomain.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,7 @@ Record wf_numbering (n: numbering) : Prop := {
In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v
}.

Create HintDb cse.
Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.

(** Satisfiability of numberings. A numbering holds in a concrete
Expand Down
8 changes: 4 additions & 4 deletions backend/CSEproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1079,27 +1079,27 @@ Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).
Proof. exact (Genv.find_symbol_match TRANSF). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
Proof. exact (Genv.senv_match TRANSF). Qed.

Lemma functions_translated:
forall (v: val) (f: RTL.fundef),
Genv.find_funct ge v = Some f ->
exists cu tf, Genv.find_funct tge v = Some tf
/\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf
/\ linkorder cu prog.
Proof (Genv.find_funct_match TRANSF).
Proof. exact (Genv.find_funct_match TRANSF). Qed.

Lemma funct_ptr_translated:
forall (b: block) (f: RTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists cu tf, Genv.find_funct_ptr tge b = Some tf
/\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf
/\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).
Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.

Lemma sig_preserved:
forall dm rm f tf, transf_fundef dm rm f = OK tf -> funsig tf = funsig f.
Expand Down
8 changes: 4 additions & 4 deletions backend/CleanupLabelsproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,23 +40,23 @@ Let tge := Genv.globalenv tprog.
Lemma symbols_preserved:
forall id,
Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf TRANSL).
Proof. exact (Genv.find_symbol_transf TRANSL). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_transf TRANSL).
Proof. exact (Genv.senv_transf TRANSL). Qed.

Lemma functions_translated:
forall v f,
Genv.find_funct ge v = Some f ->
Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL).
Proof. exact (Genv.find_funct_transf TRANSL). Qed.

Lemma function_ptr_translated:
forall v f,
Genv.find_funct_ptr ge v = Some f ->
Genv.find_funct_ptr tge v = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL).
Proof. exact (Genv.find_funct_ptr_transf TRANSL). Qed.

Lemma sig_function_translated:
forall f,
Expand Down
4 changes: 2 additions & 2 deletions backend/Cminor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1152,7 +1152,7 @@ Lemma eval_funcall_steps:
is_call_cont k ->
star step ge (Callstate fd args k m)
t (Returnstate res k m').
Proof (proj1 eval_funcall_exec_stmt_steps).
Proof. exact (proj1 eval_funcall_exec_stmt_steps). Qed.

Lemma exec_stmt_steps:
forall f sp e m s t e' m' out,
Expand All @@ -1161,7 +1161,7 @@ Lemma exec_stmt_steps:
exists S,
star step ge (State f s k sp e m) t S
/\ outcome_state_match sp e' m' f k out S.
Proof (proj2 eval_funcall_exec_stmt_steps).
Proof. exact (proj2 eval_funcall_exec_stmt_steps). Qed.

Lemma evalinf_funcall_forever:
forall m fd args T k,
Expand Down
1 change: 1 addition & 0 deletions backend/CminorSel.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -459,6 +459,7 @@ Inductive final_state: state -> int -> Prop :=
Definition semantics (p: program) :=
Semantics step (initial_state p) final_state (Genv.globalenv p).

Create HintDb evalexpr.
Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.

(** * Lifting of let-bound variables *)
Expand Down
4 changes: 2 additions & 2 deletions backend/Constpropproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,11 @@ Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSL).
Proof. exact (Genv.find_symbol_match TRANSL). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSL).
Proof. exact (Genv.senv_match TRANSL). Qed.

Lemma functions_translated:
forall (v: val) (f: fundef),
Expand Down
8 changes: 4 additions & 4 deletions backend/Deadcodeproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -413,25 +413,25 @@ Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).
Proof. exact (Genv.find_symbol_match TRANSF). Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).
Proof. exact (Genv.senv_match TRANSF). Qed.

Lemma functions_translated:
forall (v: val) (f: RTL.fundef),
Genv.find_funct ge v = Some f ->
exists cu tf,
Genv.find_funct tge v = Some tf /\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_match TRANSF).
Proof. exact (Genv.find_funct_match TRANSF). Qed.

Lemma function_ptr_translated:
forall (b: block) (f: RTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists cu tf,
Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).
Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.

Lemma sig_function_translated:
forall dm rm f tf,
Expand Down
Loading
Loading