Merge pull request #547 from AbsInt/coq-9.0

Support for Rocq/Coq 9.0

Author: xavierleroy

.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.