Support for Rocq/Coq 9.0

.github/workflows/latest.yml

@@ -16,18 +16,18 @@ jobs:
       target: ${{ matrix.target }}
       os: linux
       jobs: 4
-      opamroot: /home/coq/.opam
+      opamroot: /home/rocq/.opam
       configopts: -ignore-coq-version
     container:
-      image: coqorg/coq:latest-ocaml-4.14-flambda
+      image: rocq/rocq-prover:latest
       options: --user root
     steps:
       - name: Checkout
         uses: actions/checkout@v4
         with:
           submodules: true
       - name: OPAM dependencies
-        run: tools/runner.sh opam_install menhir
+        run: tools/runner.sh opam_install coq menhir
       - name: Configure
         run: tools/runner.sh configure
       - name: Build

.github/workflows/oldest.yml

@@ -19,7 +19,7 @@ jobs:
       opamroot: /home/coq/.opam
       configopts: -ignore-coq-version
     container:
-      image: coqorg/coq:8.13
+      image: coqorg/coq:8.15
       options: --user root
     steps:
       - name: Checkout

Makefile

@@ -61,29 +61,35 @@ endif
 # deprecated-since-8.20
 #    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".
 
 COQCOPTS ?= \
   -w -unused-pattern-matching-variable \
   -w -deprecated-since-8.19 \
-  -w -deprecated-since-8.20
+  -w -deprecated-since-8.20 \
+  -w -deprecated-from-Coq
 
 cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
 MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
 
 # Flocq and Menhirlib run into other renaming issues.
 # These warnings can only be addressed upstream.
 
-flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
-MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition
+flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
+MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
 
 # For the extraction phase, we silence other warnings:
 # change-dir-deprecated:
 #    warning introduced in 8.20, no alternative before 8.20
 # extraction-default-directory:
 #    warning introduced in 8.20, no alternative before 8.20
+# deprecated-from-Coq:
+#    see above
 COQEXTRACTOPTS ?= \
   -w -change-dir-deprecated \
-  -w -extraction-default-directory
+  -w -extraction-default-directory \
+  -w -deprecated-from-Coq
 
 ifneq ($(INSTALL_COQDEV),true)
 # Disable costly generation of .cmx files, which are not used locally

Makefile.extr

@@ -72,6 +72,7 @@ EXTRWARNINGS=$(WARNINGS) \
   -w -ambiguous-name \
   -w -open-shadow-identifier \
   -w -open-shadow-label-constructor \
+  -w -unreachable-case \
   -w -unused-module \
   -w -unused-functor-parameter
 

aarch64/Archi.v

@@ -16,8 +16,8 @@
 
 (** Architecture-dependent parameters for AArch64 *)
 
+From Coq Require Import ZArith List.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := true.
 

aarch64/Asmgen.v

@@ -12,8 +12,8 @@
 
 (** Translation from Mach to AArch64. *)
 
-Require Import Recdef Coqlib Zwf Zbits.
-Require Import Errors AST Integers Floats Op.
+From Coq Require Import Recdef Zwf.
+Require Import Zbits Coqlib Errors AST Integers Floats Op.
 Require Import Locations Mach Asm.
 Require SelectOp.
 

aarch64/Asmgenproof1.v

@@ -12,8 +12,9 @@
 
 (** Correctness proof for AArch64 code generation: auxiliary results. *)
 
-Require Import Recdef Coqlib Zwf Zbits.
-Require Import Maps Errors AST Integers Floats Values Memory Globalenvs.
+From Coq Require Import Recdef Zwf.
+Require Import Zbits Coqlib Maps Errors.
+Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Mach Asm Conventions.
 Require Import Asmgen.
 Require Import Asmgenproof0.

aarch64/Builtins1.v

@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 
 Inductive platform_builtin : Type := .

aarch64/CombineOpproof.v

@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib.
 Require Import AST Integers Values Memory.
 Require Import Op Registers RTL.

aarch64/Machregs.v

@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Decidableplus Maps.
 Require Import AST Op.
 

arm/Archi.v

@@ -17,8 +17,8 @@
 
 (** Architecture-dependent parameters for ARM *)
 
+From Coq Require Import ZArith List.
 From Flocq Require Import Binary Bits.
-Require Import ZArith List.
 
 Definition ptr64 := false.
 

arm/Builtins1.v

@@ -16,8 +16,8 @@
 
 (** Platform-specific built-in functions *)
 
-Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+From Coq Require Import String.
+Require Import Coqlib AST Integers Floats Values.
 Require Import Builtins0.
 
 Inductive platform_builtin : Type := .

arm/CombineOpproof.v

@@ -13,15 +13,9 @@
 (** Recognition of combined operations, addressing modes and conditions
   during the [CSE] phase. *)
 
-Require Import FunInd.
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
+From Coq Require Import FunInd.
+Require Import Coqlib AST Integers Values Memory.
+Require Import Op Registers RTL.
 Require Import CSEdomain.
 Require Import CombineOp.
 

arm/Machregs.v

@@ -10,12 +10,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import String.
-Require Import Coqlib.
-Require Import Decidableplus.
-Require Import Maps.
-Require Import AST.
-Require Import Op.
+From Coq Require Import String.
+Require Import Coqlib Decidableplus Maps.
+Require Import AST Op.
 
 (** ** Machine registers *)
 

arm/SelectLongproof.v

@@ -12,7 +12,8 @@
 
 (** Instruction selection for 64-bit integer operations *)
 
-Require Import String Coqlib Maps Integers Floats Errors.
+From Coq Require Import String.
+Require Import Coqlib Maps Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.

backend/Allocation.v

@@ -12,7 +12,8 @@
 
 (** Register allocation by external oracle and a posteriori validation. *)
 
-Require Import FSets FSetAVLplus.
+From Coq Require Import FSets.
+Require Import FSetAVLplus.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Lattice Kildall Memdata.
 Require Archi.

backend/Allocproof.v

@@ -13,8 +13,7 @@
 (** Correctness proof for the [Allocation] pass (validated translation from
   RTL to LTL). *)
 
-Require Import FunInd.
-Require Import FSets.
+From Coq Require Import FunInd FSets.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Linking Lattice Kildall.
 Require Import Values Memory Globalenvs Events Smallstep.

backend/Bounds.v

@@ -12,7 +12,7 @@
 
 (** Computation of resource bounds for Linear code. *)
 
-Require Import FSets FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Ordered.
 Require Intv.
 Require Import AST.

backend/CleanupLabels.v

@@ -20,7 +20,7 @@
   better-looking, the present pass removes labels that cannot be
   branched to. *)
 
-Require Import FSets FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Ordered.
 Require Import Linear.
 

backend/CleanupLabelsproof.v

@@ -12,7 +12,7 @@
 
 (** Correctness proof for clean-up of labels *)
 
-Require Import FSets.
+From Coq Require Import FSets.
 Require Import Coqlib Ordered Integers.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.

backend/Deadcodeproof.v

@@ -12,7 +12,7 @@
 
 (** Elimination of unneeded computations over RTL: correctness proof. *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
 Require Import AST Linking.
 Require Import Values Memory Builtins Globalenvs Events Smallstep.

backend/Inliningaux.mli

@@ -0,0 +1,19 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Inlining heuristics *)
+
+type inlining_info
+
+val inlining_analysis: RTL.program -> inlining_info
+
+val should_inline: inlining_info -> AST.ident -> RTL.coq_function -> bool

backend/Linearize.v

@@ -12,7 +12,7 @@
 
 (** Linearization of the control-flow graph: translation from LTL to Linear *)
 
-Require Import FSets FSetAVL.
+From Coq Require Import FSets FSetAVL.
 Require Import Coqlib Maps Ordered Errors Lattice Kildall.
 Require Import AST Op Locations LTL Linear.
 

backend/Linearizeproof.v

@@ -12,7 +12,7 @@
 
 (** Correctness proof for code linearization *)
 
-Require Import FSets.
+From Coq Require Import FSets.
 Require Import Coqlib Maps Ordered Errors Lattice Kildall Integers.
 Require Import AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.

backend/Locations.v

@@ -13,12 +13,9 @@
 (** Locations are a refinement of RTL pseudo-registers, used to reflect
   the results of register allocation (file [Allocation]). *)
 
-Require Import OrderedType.
-Require Import Coqlib.
-Require Import Maps.
-Require Import Ordered.
-Require Import AST.
-Require Import Values.
+From Coq Require Import OrderedType.
+Require Import Coqlib Maps Ordered.
+Require Import AST Values.
 Require Export Machregs.
 
 (** * Representation of locations *)

backend/RTLgenproof.v

@@ -12,7 +12,8 @@
 
 (** Correctness proof for RTL generation. *)
 
-Require Import Wellfounded Coqlib Maps AST Linking.
+From Coq Require Import Wellfounded.
+Require Import Coqlib Maps AST Linking.
 Require Import Integers Values Memory Events Smallstep Globalenvs.
 Require Import Switch Registers Cminor Op CminorSel RTL.
 Require Import RTLgen RTLgenspec.

backend/Registers.v

@@ -17,12 +17,9 @@
   intermediate language.  We also define finite sets and finite maps
   over pseudo-registers. *)
 
-Require Import Coqlib.
-Require Import AST.
-Require Import Maps.
-Require Import Ordered.
-Require FSetAVL.
-Require Import Values.
+From Coq Require FSetAVL.
+Require Import Coqlib Maps Ordered.
+Require Import AST Values.
 
 Definition reg: Type := positive.
 

backend/SelectDivproof.v

@@ -12,7 +12,8 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import Zquot Coqlib Zbits.
+From Coq Require Import Zquot.
+Require Import Coqlib Zbits.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.

backend/Selection.v

@@ -22,7 +22,7 @@
   Instruction selection proceeds by bottom-up rewriting over expressions.
   The source language is Cminor and the target language is CminorSel. *)
 
-Require String.
+From Coq Require String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Globalenvs Builtins Switch.
 Require Cminor.

backend/Selectionproof.v

@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps.
 Require Import AST Linking Errors Integers.
 Require Import Values Memory Builtins Events Globalenvs Smallstep.

backend/SplitLong.vp

@@ -12,7 +12,7 @@
 
 (** Instruction selection for 64-bit integer operations *)
 
-Require String.
+From Coq Require String.
 Require Import Coqlib.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.

backend/SplitLongproof.v

@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Maps.
 Require Import AST Errors Integers Floats.
 Require Import Values Memory Globalenvs Builtins Events Cminor Op CminorSel.

backend/Tunneling.v

@@ -12,7 +12,7 @@
 
 (** Branch tunneling (optimization of branches to branches). *)
 
-Require Import FunInd.
+From Coq Require Import FunInd.
 Require Import Coqlib Maps UnionFind.
 Require Import AST.
 Require Import LTL.