Install platform version of compcert 3.7 via opam in travis CI

.travis.yml

@@ -35,6 +35,7 @@ env:
 #  - COMPILER="default"
   - COQ_VERSION="8.11.0"
   - NEXT_VERSION="8.11.0"
+  - COMPCERT_VERSION="3.7~platform-flocq"
 
 branches:
   only:
@@ -61,10 +62,12 @@ install:
 - opam config var root
 - opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev || true
 - opam repo add coq-released https://coq.inria.fr/opam/released
+- opam repo add prerelease file://$(pwd)/opam-prerelease
 - opam update
 - opam show coq
 - travis_wait 15 opam install -j ${NJOBS} -y coq=${COQ_VERSION} ${EXTRA_OPAM}
 - opam install -j ${NJOBS} -y coq=${COQ_VERSION} coq-ext-lib coq-flocq
+- travis_wait 30 opam install -j ${NJOBS} -y coq-COMPCERT=${COMPCERT_VERSION}
 - opam list
 - file `which coqc`
 

opam-prerelease/packages/coq-compcert/coq-compcert.3.7/opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+authors: "Xavier Leroy <[email protected]>"
+maintainer: "Jacques-Henri Jourdan <[email protected]>"
+homepage: "http://compcert.inria.fr/"
+dev-repo: "git+https://github.com/AbsInt/CompCert.git"
+bug-reports: "https://github.com/AbsInt/CompCert/issues"
+license: "INRIA Non-Commercial License Agreement"
+build: [
+  ["./configure" "ia32-linux" {os = "linux"}
+  "ia32-macosx" {os = "macos"}
+  "ia32-cygwin" {os = "cygwin"}
+  "-bindir" "%{bin}%"
+  "-libdir" "%{lib}%/compcert"
+  "-install-coqdev"
+  "-clightgen"
+  "-coqdevdir" "%{lib}%/coq/user-contrib/compcert"
+  "-ignore-coq-version"]
+  [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
+]
+install: [
+  [make "install"]
+  ["install" "-m" "0644" "VERSION" "%{lib}%/coq/user-contrib/compcert/"]
+]
+depends: [
+  "coq" {>= "8.7.0" & < "8.12"}
+  "menhir" {>= "20190626" & < "20200123"}
+  "ocaml" {>= "4.05.0"}
+]
+synopsis: "The CompCert C compiler"
+tags: [
+  "category:CS/Semantics and Compilation/Compilation"
+  "category:CS/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "keyword:compiler"
+  "logpath:compcert"
+  "date:2020-03-21"
+]
+url {
+  src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz"
+  checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0"
+}

opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch

@@ -0,0 +1,36 @@
+diff --git a/Makefile b/Makefile
+index af069e3f..c924283b 100644
+--- a/Makefile
++++ b/Makefile
+@@ -205,18 +205,19 @@ compcert.ini: Makefile.config
+          echo "prepro=$(CPREPRO)"; \
+          echo "linker=$(CLINKER)"; \
+          echo "asm=$(CASM)"; \
+-	 echo "prepro_options=$(CPREPRO_OPTIONS)";\
+-	 echo "asm_options=$(CASM_OPTIONS)";\
+-	 echo "linker_options=$(CLINKER_OPTIONS)";\
++         echo "prepro_options=$(CPREPRO_OPTIONS)";\
++         echo "asm_options=$(CASM_OPTIONS)";\
++         echo "linker_options=$(CLINKER_OPTIONS)";\
+          echo "arch=$(ARCH)"; \
+          echo "model=$(MODEL)"; \
+          echo "abi=$(ABI)"; \
+          echo "endianness=$(ENDIANNESS)"; \
++         echo "bitsize=$(BITSIZE)"; \
+          echo "system=$(SYSTEM)"; \
+          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
+          echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \
+          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
+-	 echo "response_file_style=$(RESPONSEFILE)";) \
++         echo "response_file_style=$(RESPONSEFILE)";) \
+         > compcert.ini
+
+ driver/Version.ml: VERSION
+@@ -253,6 +254,7 @@ ifeq ($(INSTALL_COQDEV),true)
+           install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
+ 	done
+ 	install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
++	install -m 0644 ./compcert.ini $(DESTDIR)$(COQDEVDIR)
+ 	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
+ endif
+

opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch

@@ -0,0 +1,104 @@
+diff --git a/aarch64/Archi.v b/aarch64/Archi.v
+index aef4ab77..c99569c0 100644
+--- a/aarch64/Archi.v
++++ b/aarch64/Archi.v
+@@ -13,7 +13,7 @@
+ (** Architecture-dependent parameters for AArch64 *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := true.
+diff --git a/arm/Archi.v b/arm/Archi.v
+index 16d6c71d..9b4cc96a 100644
+--- a/arm/Archi.v
++++ b/arm/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for ARM *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := false.
+diff --git a/lib/Floats.v b/lib/Floats.v
+index 13350dd0..ea9e220d 100644
+--- a/lib/Floats.v
++++ b/lib/Floats.v
+@@ -17,7 +17,7 @@
+ (** Formalization of floating-point numbers, using the Flocq library. *)
+
+ Require Import Coqlib Zbits Integers.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits Core.
+ Require Import IEEE754_extra.
+ Require Import Program.
+diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
+index c23149be..d546c7d3 100644
+--- a/lib/IEEE754_extra.v
++++ b/lib/IEEE754_extra.v
+@@ -20,7 +20,7 @@
+ Require Import Psatz.
+ Require Import Bool.
+ Require Import Eqdep_dec.
+-(*From Flocq *)
++From Flocq
+ Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd.
+
+ Local Open Scope Z_scope.
+diff --git a/powerpc/Archi.v b/powerpc/Archi.v
+index 10f38391..5ada45f4 100644
+--- a/powerpc/Archi.v
++++ b/powerpc/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for PowerPC *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := false.
+diff --git a/riscV/Archi.v b/riscV/Archi.v
+index 61d129d0..4a929aac 100644
+--- a/riscV/Archi.v
++++ b/riscV/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for RISC-V *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Parameter ptr64 : bool.
+diff --git a/x86_32/Archi.v b/x86_32/Archi.v
+index e9d05c14..b5e4b638 100644
+--- a/x86_32/Archi.v
++++ b/x86_32/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for x86 in 32-bit mode *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := false.
+diff --git a/x86_64/Archi.v b/x86_64/Archi.v
+index 959d8dc1..59502b4a 100644
+--- a/x86_64/Archi.v
++++ b/x86_64/Archi.v
+@@ -17,7 +17,7 @@
+ (** Architecture-dependent parameters for x86 in 64-bit mode *)
+
+ Require Import ZArith List.
+-(*From Flocq*)
++From Flocq
+ Require Import Binary Bits.
+
+ Definition ptr64 := true.

opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam

@@ -0,0 +1,48 @@
+opam-version: "2.0"
+authors: "Xavier Leroy <[email protected]>"
+maintainer: "Jacques-Henri Jourdan <[email protected]>"
+homepage: "http://compcert.inria.fr/"
+dev-repo: "git+https://github.com/AbsInt/CompCert.git"
+bug-reports: "https://github.com/AbsInt/CompCert/issues"
+license: "INRIA Non-Commercial License Agreement"
+version: "3.7"
+build: [
+  ["./configure" "ia32-linux" {os = "linux"}
+  "ia32-macosx" {os = "macos"}
+  "ia32-cygwin" {os = "cygwin"}
+  "-bindir" "%{bin}%"
+  "-libdir" "%{lib}%/compcert"
+  "-install-coqdev"
+  "-clightgen"
+  "-coqdevdir" "%{lib}%/coq/user-contrib/compcert"
+  "-ignore-coq-version"]
+  [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
+]
+patches: ["platform-flocq.patch" "copy_ini_to_coqlib.patch"]
+extra-files: [
+  ["platform-flocq.patch" "sha256=36371f28651ac2310b96ea4e3fc6bf2a0c48074e088da46de6cc45458b8b4d82"]
+  ["copy_ini_to_coqlib.patch" "sha256=f461f47a464e6f34eab0160f02b94ff00fa742a647df79e1de09f101800e3bb2"]
+]
+install: [
+  [make "install"]
+  ["install" "-m" "0644" "VERSION" "%{lib}%/coq/user-contrib/compcert/"]
+]
+depends: [
+  "coq" {>= "8.7.0" & < "8.12"}
+  "coq-flocq" {>= "3.2.1"}
+  "menhir" {>= "20190626" & < "20200123"}
+  "ocaml" {>= "4.05.0"}
+]
+synopsis: "The CompCert C compiler (using the platform supplied version of Flocq)"
+tags: [
+  "category:CS/Semantics and Compilation/Compilation"
+  "category:CS/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "keyword:compiler"
+  "logpath:compcert"
+  "date:2020-03-21"
+]
+url {
+  src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz"
+  checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0"
+}