From 622dbde0326c15b6acde35015913ee25660c05be Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Wed, 22 Apr 2020 15:56:19 +0200 Subject: [PATCH] Install platform version of compcert 3.7 via opam in travis CI --- .travis.yml | 3 + .../coq-compcert/coq-compcert.3.7/opam | 41 +++++++ .../files/copy_ini_to_coqlib.patch | 36 ++++++ .../files/platform-flocq.patch | 104 ++++++++++++++++++ .../coq-compcert.3.7~platform-flocq/opam | 48 ++++++++ 5 files changed, 232 insertions(+) create mode 100644 opam-prerelease/packages/coq-compcert/coq-compcert.3.7/opam create mode 100644 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch create mode 100644 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch create mode 100644 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam diff --git a/.travis.yml b/.travis.yml index f90564d64b..bbeee96cc7 100644 --- a/.travis.yml +++ b/.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 +- opam install -j ${NJOBS} -y coq-COMPCERT=${COMPCERT_VERSION} - opam list - file `which coqc` diff --git a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7/opam b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7/opam new file mode 100644 index 0000000000..c77b51f439 --- /dev/null +++ b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7/opam @@ -0,0 +1,41 @@ +opam-version: "2.0" +authors: "Xavier Leroy " +maintainer: "Jacques-Henri Jourdan " +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" +} diff --git a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch new file mode 100644 index 0000000000..60d5107b44 --- /dev/null +++ b/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 + diff --git a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch new file mode 100644 index 0000000000..10fd7ea471 --- /dev/null +++ b/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. diff --git a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam new file mode 100644 index 0000000000..954a57cd4e --- /dev/null +++ b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam @@ -0,0 +1,48 @@ +opam-version: "2.0" +authors: "Xavier Leroy " +maintainer: "Jacques-Henri Jourdan " +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" +}