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

Open
xavierleroy wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Full support for Rocq 9.2 #587

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
4e26d4b
Build system: call `rocq` if available, instead of `coqc`, etc
xavierleroy Jun 11, 2026
73e0bce
GHA CI: update `latest` action to Rocq 9.2.0
xavierleroy Jun 11, 2026
d46a7c3
Explicit declaration of proof hints databases using `Create Hintdb`
xavierleroy Jun 13, 2026
186b6d4
Rewrite `Proof (term)` as `Proof. exact (term). Qed.`
xavierleroy Jun 13, 2026
9c2cd93
Put postfix notations at level 1
xavierleroy Jun 13, 2026
62e0d5d
Avoid `try (rewrite H; auto)` when `H` may not be an equality
xavierleroy Jun 14, 2026
99937c5
Memory.v: use more portable lemmas from ZArith
xavierleroy Jun 14, 2026
11f5f2f
Makefile: update warning options for Rocq 9.2
xavierleroy Jun 14, 2026
a29b3d5
MenhirLib/Interpreter.v: reintroduce `Declare Scope` and re-enable wa…
xavierleroy Jun 14, 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
23 changes: 14 additions & 9 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ COQCOPTS ?= \
-w -deprecated-since-8.20 \
-w -deprecated-from-Coq

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

# Flocq and Menhirlib run into other renaming issues.
Expand Down Expand Up @@ -113,11 +113,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,13 +316,13 @@ latexdoc:

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

%.v: %.vp tools/ndfun
@rm -f $*.v
@echo "Preprocessing $*.vp"
@echo " Preprocessing $*.vp"
@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
@chmod a-w $*.v

Expand Down Expand Up @@ -369,7 +374,7 @@ cparser/Parser.v: cparser/Parser.vy
depend: $(GENERATED) depend1

depend1: $(FILES)
@echo "Analyzing Coq dependencies"
@echo " Analyzing Coq dependencies"
@$(COQDEP) $^ > .depend

install:
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
8 changes: 4 additions & 4 deletions backend/Debugvarproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -296,25 +296,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: 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: 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_preserved:
forall f tf,
Expand Down
8 changes: 4 additions & 4 deletions backend/Inliningproof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,23 +36,23 @@ 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: fundef),
Genv.find_funct ge v = Some f ->
exists cu f', Genv.find_funct tge v = Some f' /\ transf_fundef (funenv_program cu) f = OK f' /\ 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: fundef),
Genv.find_funct_ptr ge b = Some f ->
exists cu f', Genv.find_funct_ptr tge b = Some f' /\ transf_fundef (funenv_program cu) f = OK f' /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).
Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.

Lemma sig_function_translated:
forall cu f f', transf_fundef (funenv_program cu) f = OK f' -> funsig f' = funsig f.
Expand Down
Loading