From 28f27d0a352d28bc6f1873768f3776fed468a003 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 20 Apr 2020 14:49:31 +0200 Subject: [PATCH 1/4] Added latest CompCert version (3.7) and platform Flocq variant of CompCert --- .../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 ++++++++ 4 files changed, 229 insertions(+) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7/opam create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam diff --git a/released/packages/coq-compcert/coq-compcert.3.7/opam b/released/packages/coq-compcert/coq-compcert.3.7/opam new file mode 100644 index 000000000..c77b51f43 --- /dev/null +++ b/released/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/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch b/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch new file mode 100644 index 000000000..60d5107b4 --- /dev/null +++ b/released/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/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch b/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch new file mode 100644 index 000000000..10fd7ea47 --- /dev/null +++ b/released/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/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam b/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam new file mode 100644 index 000000000..954a57cd4 --- /dev/null +++ b/released/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" +} From 84b46199f7866609739236b7e23424c0d914e49e Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 1 May 2020 12:04:38 +0200 Subject: [PATCH 2/4] Adjusted to compcert makefile changes --- .../coq-compcert/coq-compcert.3.7/opam | 1 - ....config-file-along-the-Coq-developme.patch | 81 +++++++++++++++++++ ...003-Use-Coq-platform-supplied-Flocq.patch} | 19 +++++ .../opam | 14 ++-- .../files/copy_ini_to_coqlib.patch | 36 --------- 5 files changed, 108 insertions(+), 43 deletions(-) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch rename released/packages/coq-compcert/{coq-compcert.3.7~platform-flocq/files/platform-flocq.patch => coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch} (82%) rename released/packages/coq-compcert/{coq-compcert.3.7~platform-flocq => coq-compcert.3.7~coq-platform}/opam (71%) delete mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch diff --git a/released/packages/coq-compcert/coq-compcert.3.7/opam b/released/packages/coq-compcert/coq-compcert.3.7/opam index c77b51f43..f58109163 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7/opam @@ -19,7 +19,6 @@ build: [ ] install: [ [make "install"] - ["install" "-m" "0644" "VERSION" "%{lib}%/coq/user-contrib/compcert/"] ] depends: [ "coq" {>= "8.7.0" & < "8.12"} diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch new file mode 100644 index 000000000..63df61d08 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch @@ -0,0 +1,81 @@ +From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Wed, 29 Apr 2020 15:40:13 +0200 +Subject: [PATCH 1/3] Install "compcert.config" file along the Coq development + +The file contains various parameters about the target processor and ABI, +useful for VST and possibly other users of CompCert as a Coq library. + +It is in "var=val" syntax so that it can be included directly from +a Makefile or a shell script. +--- + .gitignore | 1 + + Makefile | 19 ++++++++++++++++++- + 2 files changed, 19 insertions(+), 1 deletion(-) + +diff --git a/.gitignore b/.gitignore +index 6c10e1c3..b75ea5e7 100644 +--- a/.gitignore ++++ b/.gitignore +@@ -31,6 +31,7 @@ + /.depend + /.depend.extr + /compcert.ini ++/compcert.config + /x86/ConstpropOp.v + /x86/SelectOp.v + /x86/SelectLong.v +diff --git a/Makefile b/Makefile +index aed0da28..df5fb03f 100644 +--- a/Makefile ++++ b/Makefile +@@ -147,6 +147,9 @@ endif + ifeq ($(CLIGHTGEN),true) + $(MAKE) clightgen + endif ++ifeq ($(INSTALL_COQDEV),true) ++ $(MAKE) compcert.config ++endif + + proof: $(FILES:.v=.vo) + +@@ -224,6 +227,19 @@ compcert.ini: Makefile.config + echo "response_file_style=$(RESPONSEFILE)";) \ + > compcert.ini + ++compcert.config: Makefile.config ++ (echo "# CompCert configuration parameters"; \ ++ echo "COMPCERT_ARCH=$(ARCH)"; \ ++ echo "COMPCERT_MODEL=$(MODEL)"; \ ++ echo "COMPCERT_ABI=$(ABI)"; \ ++ echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \ ++ echo "COMPCERT_BITSIZE=$(BITSIZE)"; \ ++ echo "COMPCERT_SYSTEM=$(SYSTEM)"; \ ++ echo "COMPCERT_VERSION=$(BUILDVERSION)"; \ ++ echo "COMPCERT_BUILDNR=$(BUILDNR)"; \ ++ echo "COMPCERT_TAG=$(TAG)" \ ++ ) > compcert.config ++ + driver/Version.ml: VERSION + (echo 'let version = "$(BUILDVERSION)"'; \ + echo 'let buildnr = "$(BUILDNR)"'; \ +@@ -258,6 +274,7 @@ ifeq ($(INSTALL_COQDEV),true) + install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \ + done + install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR) ++ install -m 0644 ./compcert.config $(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 + +@@ -267,7 +284,7 @@ clean: + rm -f $(patsubst %, %/.*.aux, $(DIRS)) + rm -rf doc/html doc/*.glob + rm -f driver/Version.ml +- rm -f compcert.ini ++ rm -f compcert.ini compcert.config + rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr + rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o + rm -f $(GENERATED) .depend +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch similarity index 82% rename from released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch rename to released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch index 10fd7ea47..1adbba4b5 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch @@ -1,3 +1,19 @@ +From e47591667fea0cc22ccd0ba407d8c1463005686b Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Thu, 30 Apr 2020 16:25:19 +0200 +Subject: [PATCH 3/3] Use Coq platform supplied Flocq + +--- + aarch64/Archi.v | 2 +- + arm/Archi.v | 2 +- + lib/Floats.v | 2 +- + lib/IEEE754_extra.v | 2 +- + powerpc/Archi.v | 2 +- + riscV/Archi.v | 2 +- + x86_32/Archi.v | 2 +- + x86_64/Archi.v | 2 +- + 8 files changed, 8 insertions(+), 8 deletions(-) + diff --git a/aarch64/Archi.v b/aarch64/Archi.v index aef4ab77..c99569c0 100644 --- a/aarch64/Archi.v @@ -102,3 +118,6 @@ index 959d8dc1..59502b4a 100644 Require Import Binary Bits. Definition ptr64 := true. +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam similarity index 71% rename from released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam rename to released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam index 954a57cd4..bc1de523c 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam @@ -18,14 +18,16 @@ build: [ "-ignore-coq-version"] [make "-j%{jobs}%" {ocaml:version >= "4.06"}] ] -patches: ["platform-flocq.patch" "copy_ini_to_coqlib.patch"] +patches: [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "0003-Use-Coq-platform-supplied-Flocq.patch" +] extra-files: [ - ["platform-flocq.patch" "sha256=36371f28651ac2310b96ea4e3fc6bf2a0c48074e088da46de6cc45458b8b4d82"] - ["copy_ini_to_coqlib.patch" "sha256=f461f47a464e6f34eab0160f02b94ff00fa742a647df79e1de09f101800e3bb2"] + ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=f9354b4b52f2956842d395b8d26afe91530e7262db539439cd6b0d0f2e756f48"] + ["0003-Use-Coq-platform-supplied-Flocq.patch" "sha256=13ad400aa972dacb925376c2168b4b9be28f372b4ba42be35fbeae47c9a6773c"] ] install: [ [make "install"] - ["install" "-m" "0644" "VERSION" "%{lib}%/coq/user-contrib/compcert/"] ] depends: [ "coq" {>= "8.7.0" & < "8.12"} @@ -33,14 +35,14 @@ depends: [ "menhir" {>= "20190626" & < "20200123"} "ocaml" {>= "4.05.0"} ] -synopsis: "The CompCert C compiler (using the platform supplied version of Flocq)" +synopsis: "The CompCert C compiler (using coq-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" + "date:2020-04-29" ] url { src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz" diff --git a/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch b/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch deleted file mode 100644 index 60d5107b4..000000000 --- a/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch +++ /dev/null @@ -1,36 +0,0 @@ -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 - From 15cdaf3d08433f967ebd07ccbf1eadb27b015b67 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Fri, 1 May 2020 12:05:25 +0200 Subject: [PATCH 3/4] Added open source only variant (as a tilde version) --- ....config-file-along-the-Coq-developme.patch | 81 ++++++++++++ ...-Added-open-source-build-to-makefile.patch | 106 +++++++++++++++ ...0003-Use-Coq-platform-supplied-Flocq.patch | 123 ++++++++++++++++++ .../opam | 53 ++++++++ 4 files changed, 363 insertions(+) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch new file mode 100644 index 000000000..63df61d08 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch @@ -0,0 +1,81 @@ +From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Wed, 29 Apr 2020 15:40:13 +0200 +Subject: [PATCH 1/3] Install "compcert.config" file along the Coq development + +The file contains various parameters about the target processor and ABI, +useful for VST and possibly other users of CompCert as a Coq library. + +It is in "var=val" syntax so that it can be included directly from +a Makefile or a shell script. +--- + .gitignore | 1 + + Makefile | 19 ++++++++++++++++++- + 2 files changed, 19 insertions(+), 1 deletion(-) + +diff --git a/.gitignore b/.gitignore +index 6c10e1c3..b75ea5e7 100644 +--- a/.gitignore ++++ b/.gitignore +@@ -31,6 +31,7 @@ + /.depend + /.depend.extr + /compcert.ini ++/compcert.config + /x86/ConstpropOp.v + /x86/SelectOp.v + /x86/SelectLong.v +diff --git a/Makefile b/Makefile +index aed0da28..df5fb03f 100644 +--- a/Makefile ++++ b/Makefile +@@ -147,6 +147,9 @@ endif + ifeq ($(CLIGHTGEN),true) + $(MAKE) clightgen + endif ++ifeq ($(INSTALL_COQDEV),true) ++ $(MAKE) compcert.config ++endif + + proof: $(FILES:.v=.vo) + +@@ -224,6 +227,19 @@ compcert.ini: Makefile.config + echo "response_file_style=$(RESPONSEFILE)";) \ + > compcert.ini + ++compcert.config: Makefile.config ++ (echo "# CompCert configuration parameters"; \ ++ echo "COMPCERT_ARCH=$(ARCH)"; \ ++ echo "COMPCERT_MODEL=$(MODEL)"; \ ++ echo "COMPCERT_ABI=$(ABI)"; \ ++ echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \ ++ echo "COMPCERT_BITSIZE=$(BITSIZE)"; \ ++ echo "COMPCERT_SYSTEM=$(SYSTEM)"; \ ++ echo "COMPCERT_VERSION=$(BUILDVERSION)"; \ ++ echo "COMPCERT_BUILDNR=$(BUILDNR)"; \ ++ echo "COMPCERT_TAG=$(TAG)" \ ++ ) > compcert.config ++ + driver/Version.ml: VERSION + (echo 'let version = "$(BUILDVERSION)"'; \ + echo 'let buildnr = "$(BUILDNR)"'; \ +@@ -258,6 +274,7 @@ ifeq ($(INSTALL_COQDEV),true) + install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \ + done + install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR) ++ install -m 0644 ./compcert.config $(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 + +@@ -267,7 +284,7 @@ clean: + rm -f $(patsubst %, %/.*.aux, $(DIRS)) + rm -rf doc/html doc/*.glob + rm -f driver/Version.ml +- rm -f compcert.ini ++ rm -f compcert.ini compcert.config + rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr + rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o + rm -f $(GENERATED) .depend +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch new file mode 100644 index 000000000..6c30f3edc --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch @@ -0,0 +1,106 @@ +From d585a348abe669b57854de2dbaec68ea06e8848a Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Thu, 30 Apr 2020 13:50:08 +0200 +Subject: [PATCH 2/3] Added open source build to makefile + +--- + Makefile | 36 +++++++++++++++++++++++++++++++++--- + 1 file changed, 33 insertions(+), 3 deletions(-) + +diff --git a/Makefile b/Makefile +index df5fb03f..48770ebd 100644 +--- a/Makefile ++++ b/Makefile +@@ -57,10 +57,14 @@ FLOCQ=\ + Relative.v Sterbenz.v Round_odd.v Double_rounding.v \ + Binary.v Bits.v + ++# Architecture files (in respective architecture folder) ++ ++ARCHFILES=Archi.v ++ + # General-purpose libraries (in lib/) + + VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ +- Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ ++ Iteration.v Zbits.v Integers.v IEEE754_extra.v Floats.v \ + Parmov.v UnionFind.v Wfsimpl.v \ + Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v + +@@ -101,6 +105,8 @@ BACKEND=\ + Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ + Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v + ++BACKEND_OPEN_SOURCE=Cminor.v ++ + # C front-end modules (in cfrontend/) + + CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ +@@ -110,6 +116,8 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ + Cshmgen.v Cshmgenproof.v \ + Csharpminor.v Cminorgen.v Cminorgenproof.v + ++CFRONTEND_OPEN_SOURCE=Clight.v ClightBigstep.v Cop.v Csem.v Cstrategy.v Csyntax.v Ctypes.v Ctyping.v ++ + # Parser + + PARSER=Cabs.v Parser.v +@@ -126,9 +134,17 @@ DRIVER=Compopts.v Compiler.v Complements.v + + # All source files + +-FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ ++FILES=$(ARCHFILES) $(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ + $(MENHIRLIB) $(PARSER) + ++# All open source source files (in the order given in LICENSE) ++ ++# ATTENTION: this also includes ./x86/Builtins1.vo - which is not open source but many files depend on it ++ ++FILES_OPEN_SOURCE=$(VLIB) $(COMMON) $(CFRONTEND_OPEN_SOURCE) $(BACKEND_OPEN_SOURCE) $(PARSER) Clightdefs.v $(ARCHFILES) ++ ++# These files have non open dependencies: extractionMachdep.v, extraction.v ++ + # Generated source files + + GENERATED=\ +@@ -153,6 +169,8 @@ endif + + proof: $(FILES:.v=.vo) + ++proof_open_source: $(FILES_OPEN_SOURCE:.v=.vo) compcert.config ++ + # Turn off some warnings for compiling Flocq + flocq/%.vo: COQCOPTS+=-w -compatibility-notation + +@@ -181,7 +199,7 @@ runtime: + + FORCE: + +-.PHONY: proof extraction runtime FORCE ++.PHONY: proof proof_open_source extraction runtime FORCE + + documentation: $(FILES) + mkdir -p doc/html +@@ -278,6 +296,18 @@ ifeq ($(INSTALL_COQDEV),true) + @(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README + endif + ++# ToDo: copy exactly the files in FILES_OPEN_SOURCE as soon as the issue with Builtins1 ins fixed ++install_open_source: ++ifeq ($(INSTALL_COQDEV),true) ++ install -d $(DESTDIR)$(COQDEVDIR) ++ for d in $(DIRS); do \ ++ install -d $(DESTDIR)$(COQDEVDIR)/$$d && \ ++ install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \ ++ done ++ install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR) ++ install -m 0644 ./compcert.config $(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 + + clean: + rm -f $(patsubst %, %/*.vo*, $(DIRS)) +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch new file mode 100644 index 000000000..1adbba4b5 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch @@ -0,0 +1,123 @@ +From e47591667fea0cc22ccd0ba407d8c1463005686b Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Thu, 30 Apr 2020 16:25:19 +0200 +Subject: [PATCH 3/3] Use Coq platform supplied Flocq + +--- + aarch64/Archi.v | 2 +- + arm/Archi.v | 2 +- + lib/Floats.v | 2 +- + lib/IEEE754_extra.v | 2 +- + powerpc/Archi.v | 2 +- + riscV/Archi.v | 2 +- + x86_32/Archi.v | 2 +- + x86_64/Archi.v | 2 +- + 8 files changed, 8 insertions(+), 8 deletions(-) + +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. +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam new file mode 100644 index 000000000..d11bf2f00 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam @@ -0,0 +1,53 @@ +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 "depend"] + [make "-j%{jobs}%" {ocaml:version >= "4.06"} "proof_open_source"] +] +patches: [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "0002-Added-open-source-build-to-makefile.patch" + "0003-Use-Coq-platform-supplied-Flocq.patch" +] +extra-files: [ + ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=f9354b4b52f2956842d395b8d26afe91530e7262db539439cd6b0d0f2e756f48"] + ["0002-Added-open-source-build-to-makefile.patch" "sha256=86d412ccc1ba6d7c53e856d3b3683d4a6bdf91d39808410364d1a35bab9cf292"] + ["0003-Use-Coq-platform-supplied-Flocq.patch" "sha256=13ad400aa972dacb925376c2168b4b9be28f372b4ba42be35fbeae47c9a6773c"] +] +install: [ + [make "install_open_source"] +] +depends: [ + "coq" {>= "8.7.0" & < "8.12"} + "coq-flocq" {>= "3.2.1"} + "menhir" {>= "20190626" & < "20200123"} + "ocaml" {>= "4.05.0"} +] +synopsis: "The CompCert C compiler (only open source files + Builtins1.vo)" +tags: [ + "category:CS/Semantics and Compilation/Compilation" + "category:CS/Semantics and Compilation/Semantics" + "keyword:C" + "keyword:compiler" + "logpath:compcert" + "date:2020-04-29" +] +url { + src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz" + checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0" +} From 8e0602eae808472d51247fdbad847384854f82e7 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Tue, 5 May 2020 18:29:18 +0200 Subject: [PATCH 4/4] Included CompCert license file changes as patch Use opam supplied MenhirLib in the Coq platform packages --- ....config-file-along-the-Coq-developme.patch | 3 +- ...ch64-Archi.v-Cbuiltins.ml-extraction.patch | 60 +++++++++++++++++++ ...date-the-list-of-dual-licensed-files.patch | 28 +++++++++ ...011-Use-Coq-platform-supplied-Flocq.patch} | 10 ++-- ...plied-menhirlib-as-suggested-by-jhjo.patch | 26 ++++++++ .../coq-compcert.3.7~coq-platform/opam | 13 +++- ....config-file-along-the-Coq-developme.patch | 3 +- ...ch64-Archi.v-Cbuiltins.ml-extraction.patch | 60 +++++++++++++++++++ ...date-the-list-of-dual-licensed-files.patch | 28 +++++++++ ...Added-open-source-build-to-makefile.patch} | 4 +- ...011-Use-Coq-platform-supplied-Flocq.patch} | 10 ++-- ...plied-menhirlib-as-suggested-by-jhjo.patch | 26 ++++++++ .../opam | 19 ++++-- 13 files changed, 267 insertions(+), 23 deletions(-) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch rename released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/{0003-Use-Coq-platform-supplied-Flocq.patch => 0011-Use-Coq-platform-supplied-Flocq.patch} (93%) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch rename released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/{0002-Added-open-source-build-to-makefile.patch => 0010-Added-open-source-build-to-makefile.patch} (96%) rename released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/{0003-Use-Coq-platform-supplied-Flocq.patch => 0011-Use-Coq-platform-supplied-Flocq.patch} (93%) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch index 63df61d08..d160e66e2 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch @@ -1,7 +1,8 @@ From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 29 Apr 2020 15:40:13 +0200 -Subject: [PATCH 1/3] Install "compcert.config" file along the Coq development +Subject: [PATCH 01/12] Install "compcert.config" file along the Coq + development The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch new file mode 100644 index 000000000..f74202a53 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch @@ -0,0 +1,60 @@ +From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Sun, 3 May 2020 09:43:14 +0200 +Subject: [PATCH 07/12] Dual-license + aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v} + +The corresponding files in all other ports are dual-licensed +(GPL + non-commercial), there is no reason it should be different for +aarch64. +--- + aarch64/Archi.v | 3 +++ + aarch64/CBuiltins.ml | 3 +++ + aarch64/extractionMachdep.v | 3 +++ + 3 files changed, 9 insertions(+) + +diff --git a/aarch64/Archi.v b/aarch64/Archi.v +index aef4ab77..24431cb2 100644 +--- a/aarch64/Archi.v ++++ b/aarch64/Archi.v +@@ -6,6 +6,9 @@ + (* *) + (* Copyright Institut National de Recherche en Informatique et en *) + (* Automatique. All rights reserved. This file is distributed *) ++(* under the terms of the GNU General Public License as published by *) ++(* the Free Software Foundation, either version 2 of the License, or *) ++(* (at your option) any later version. This file is also distributed *) + (* under the terms of the INRIA Non-Commercial License Agreement. *) + (* *) + (* *********************************************************************) +diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml +index fdc1372d..dfd5b768 100644 +--- a/aarch64/CBuiltins.ml ++++ b/aarch64/CBuiltins.ml +@@ -6,6 +6,9 @@ + (* *) + (* Copyright Institut National de Recherche en Informatique et en *) + (* Automatique. All rights reserved. This file is distributed *) ++(* under the terms of the GNU General Public License as published by *) ++(* the Free Software Foundation, either version 2 of the License, or *) ++(* (at your option) any later version. This file is also distributed *) + (* under the terms of the INRIA Non-Commercial License Agreement. *) + (* *) + (* *********************************************************************) +diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v +index e82056e2..5f26dc28 100644 +--- a/aarch64/extractionMachdep.v ++++ b/aarch64/extractionMachdep.v +@@ -6,6 +6,9 @@ + (* *) + (* Copyright Institut National de Recherche en Informatique et en *) + (* Automatique. All rights reserved. This file is distributed *) ++(* under the terms of the GNU General Public License as published by *) ++(* the Free Software Foundation, either version 2 of the License, or *) ++(* (at your option) any later version. This file is also distributed *) + (* under the terms of the INRIA Non-Commercial License Agreement. *) + (* *) + (* *********************************************************************) +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch new file mode 100644 index 000000000..57bef5e51 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch @@ -0,0 +1,28 @@ +From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Mon, 4 May 2020 10:51:47 +0200 +Subject: [PATCH 08/12] Update the list of dual-licensed files + +Closes: #351 +--- + LICENSE | 4 ++-- + 1 file changed, 2 insertions(+), 2 deletions(-) + +diff --git a/LICENSE b/LICENSE +index 5a7ae79f..61b84219 100644 +--- a/LICENSE ++++ b/LICENSE +@@ -46,8 +46,8 @@ option) any later version: + + all files in the exportclight/ directory + +- the Archi.v, CBuiltins.ml, and extractionMachdep.v files +- in directories arm, powerpc, riscV, x86, x86_32, x86_64 ++ the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files ++ in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64 + + extraction/extraction.v + +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch similarity index 93% rename from released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch rename to released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch index 1adbba4b5..0dc512b45 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch @@ -1,7 +1,7 @@ -From e47591667fea0cc22ccd0ba407d8c1463005686b Mon Sep 17 00:00:00 2001 +From 05448adb7642b3c1189139cec18c914b116d5d40 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Thu, 30 Apr 2020 16:25:19 +0200 -Subject: [PATCH 3/3] Use Coq platform supplied Flocq +Subject: [PATCH 11/12] Use Coq platform supplied Flocq --- aarch64/Archi.v | 2 +- @@ -15,10 +15,10 @@ Subject: [PATCH 3/3] Use Coq platform supplied Flocq 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/aarch64/Archi.v b/aarch64/Archi.v -index aef4ab77..c99569c0 100644 +index 24431cb2..6c5655d8 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v -@@ -13,7 +13,7 @@ +@@ -16,7 +16,7 @@ (** Architecture-dependent parameters for AArch64 *) Require Import ZArith List. @@ -41,7 +41,7 @@ index 16d6c71d..9b4cc96a 100644 Definition ptr64 := false. diff --git a/lib/Floats.v b/lib/Floats.v -index 13350dd0..ea9e220d 100644 +index 6a126c3f..25a55620 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,7 +17,7 @@ diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch new file mode 100644 index 000000000..58a641f07 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch @@ -0,0 +1,26 @@ +From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Tue, 5 May 2020 17:10:06 +0200 +Subject: [PATCH 12/12] Use platform supplied menhirlib as suggested by + jhjourdan + +--- + Makefile | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/Makefile b/Makefile +index 48770ebd..c4130630 100644 +--- a/Makefile ++++ b/Makefile +@@ -265,7 +265,7 @@ driver/Version.ml: VERSION + + cparser/Parser.v: cparser/Parser.vy + @rm -f $@ +- $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy ++ $(MENHIR) --coq cparser/Parser.vy + @chmod a-w $@ + + depend: $(GENERATED) depend1 +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam index bc1de523c..7592e3b84 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam @@ -20,11 +20,17 @@ build: [ ] patches: [ "0001-Install-compcert.config-file-along-the-Coq-developme.patch" - "0003-Use-Coq-platform-supplied-Flocq.patch" + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "0008-Update-the-list-of-dual-licensed-files.patch" + "0011-Use-Coq-platform-supplied-Flocq.patch" + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=f9354b4b52f2956842d395b8d26afe91530e7262db539439cd6b0d0f2e756f48"] - ["0003-Use-Coq-platform-supplied-Flocq.patch" "sha256=13ad400aa972dacb925376c2168b4b9be28f372b4ba42be35fbeae47c9a6773c"] + ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] + ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] + ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] + ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] + ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] ] install: [ [make "install"] @@ -32,6 +38,7 @@ install: [ depends: [ "coq" {>= "8.7.0" & < "8.12"} "coq-flocq" {>= "3.2.1"} + "coq-menhirlib" {>= "20190626" & < "20200123"} "menhir" {>= "20190626" & < "20200123"} "ocaml" {>= "4.05.0"} ] diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch index 63df61d08..d160e66e2 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch @@ -1,7 +1,8 @@ From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 29 Apr 2020 15:40:13 +0200 -Subject: [PATCH 1/3] Install "compcert.config" file along the Coq development +Subject: [PATCH 01/12] Install "compcert.config" file along the Coq + development The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch new file mode 100644 index 000000000..f74202a53 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch @@ -0,0 +1,60 @@ +From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Sun, 3 May 2020 09:43:14 +0200 +Subject: [PATCH 07/12] Dual-license + aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v} + +The corresponding files in all other ports are dual-licensed +(GPL + non-commercial), there is no reason it should be different for +aarch64. +--- + aarch64/Archi.v | 3 +++ + aarch64/CBuiltins.ml | 3 +++ + aarch64/extractionMachdep.v | 3 +++ + 3 files changed, 9 insertions(+) + +diff --git a/aarch64/Archi.v b/aarch64/Archi.v +index aef4ab77..24431cb2 100644 +--- a/aarch64/Archi.v ++++ b/aarch64/Archi.v +@@ -6,6 +6,9 @@ + (* *) + (* Copyright Institut National de Recherche en Informatique et en *) + (* Automatique. All rights reserved. This file is distributed *) ++(* under the terms of the GNU General Public License as published by *) ++(* the Free Software Foundation, either version 2 of the License, or *) ++(* (at your option) any later version. This file is also distributed *) + (* under the terms of the INRIA Non-Commercial License Agreement. *) + (* *) + (* *********************************************************************) +diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml +index fdc1372d..dfd5b768 100644 +--- a/aarch64/CBuiltins.ml ++++ b/aarch64/CBuiltins.ml +@@ -6,6 +6,9 @@ + (* *) + (* Copyright Institut National de Recherche en Informatique et en *) + (* Automatique. All rights reserved. This file is distributed *) ++(* under the terms of the GNU General Public License as published by *) ++(* the Free Software Foundation, either version 2 of the License, or *) ++(* (at your option) any later version. This file is also distributed *) + (* under the terms of the INRIA Non-Commercial License Agreement. *) + (* *) + (* *********************************************************************) +diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v +index e82056e2..5f26dc28 100644 +--- a/aarch64/extractionMachdep.v ++++ b/aarch64/extractionMachdep.v +@@ -6,6 +6,9 @@ + (* *) + (* Copyright Institut National de Recherche en Informatique et en *) + (* Automatique. All rights reserved. This file is distributed *) ++(* under the terms of the GNU General Public License as published by *) ++(* the Free Software Foundation, either version 2 of the License, or *) ++(* (at your option) any later version. This file is also distributed *) + (* under the terms of the INRIA Non-Commercial License Agreement. *) + (* *) + (* *********************************************************************) +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch new file mode 100644 index 000000000..57bef5e51 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch @@ -0,0 +1,28 @@ +From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Mon, 4 May 2020 10:51:47 +0200 +Subject: [PATCH 08/12] Update the list of dual-licensed files + +Closes: #351 +--- + LICENSE | 4 ++-- + 1 file changed, 2 insertions(+), 2 deletions(-) + +diff --git a/LICENSE b/LICENSE +index 5a7ae79f..61b84219 100644 +--- a/LICENSE ++++ b/LICENSE +@@ -46,8 +46,8 @@ option) any later version: + + all files in the exportclight/ directory + +- the Archi.v, CBuiltins.ml, and extractionMachdep.v files +- in directories arm, powerpc, riscV, x86, x86_32, x86_64 ++ the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files ++ in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64 + + extraction/extraction.v + +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch similarity index 96% rename from released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch rename to released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch index 6c30f3edc..28dbd0687 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch @@ -1,7 +1,7 @@ -From d585a348abe669b57854de2dbaec68ea06e8848a Mon Sep 17 00:00:00 2001 +From b55c97d7930caec06d559faae4684761f258fd0f Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Thu, 30 Apr 2020 13:50:08 +0200 -Subject: [PATCH 2/3] Added open source build to makefile +Subject: [PATCH 10/12] Added open source build to makefile --- Makefile | 36 +++++++++++++++++++++++++++++++++--- diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch similarity index 93% rename from released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch rename to released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch index 1adbba4b5..0dc512b45 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch @@ -1,7 +1,7 @@ -From e47591667fea0cc22ccd0ba407d8c1463005686b Mon Sep 17 00:00:00 2001 +From 05448adb7642b3c1189139cec18c914b116d5d40 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Thu, 30 Apr 2020 16:25:19 +0200 -Subject: [PATCH 3/3] Use Coq platform supplied Flocq +Subject: [PATCH 11/12] Use Coq platform supplied Flocq --- aarch64/Archi.v | 2 +- @@ -15,10 +15,10 @@ Subject: [PATCH 3/3] Use Coq platform supplied Flocq 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/aarch64/Archi.v b/aarch64/Archi.v -index aef4ab77..c99569c0 100644 +index 24431cb2..6c5655d8 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v -@@ -13,7 +13,7 @@ +@@ -16,7 +16,7 @@ (** Architecture-dependent parameters for AArch64 *) Require Import ZArith List. @@ -41,7 +41,7 @@ index 16d6c71d..9b4cc96a 100644 Definition ptr64 := false. diff --git a/lib/Floats.v b/lib/Floats.v -index 13350dd0..ea9e220d 100644 +index 6a126c3f..25a55620 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,7 +17,7 @@ diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch new file mode 100644 index 000000000..58a641f07 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch @@ -0,0 +1,26 @@ +From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Tue, 5 May 2020 17:10:06 +0200 +Subject: [PATCH 12/12] Use platform supplied menhirlib as suggested by + jhjourdan + +--- + Makefile | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/Makefile b/Makefile +index 48770ebd..c4130630 100644 +--- a/Makefile ++++ b/Makefile +@@ -265,7 +265,7 @@ driver/Version.ml: VERSION + + cparser/Parser.v: cparser/Parser.vy + @rm -f $@ +- $(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy ++ $(MENHIR) --coq cparser/Parser.vy + @chmod a-w $@ + + depend: $(GENERATED) depend1 +-- +2.24.2 (Apple Git-127) + diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam index d11bf2f00..8a4d7b390 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam @@ -21,13 +21,19 @@ build: [ ] patches: [ "0001-Install-compcert.config-file-along-the-Coq-developme.patch" - "0002-Added-open-source-build-to-makefile.patch" - "0003-Use-Coq-platform-supplied-Flocq.patch" + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "0008-Update-the-list-of-dual-licensed-files.patch" + "0010-Added-open-source-build-to-makefile.patch" + "0011-Use-Coq-platform-supplied-Flocq.patch" + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=f9354b4b52f2956842d395b8d26afe91530e7262db539439cd6b0d0f2e756f48"] - ["0002-Added-open-source-build-to-makefile.patch" "sha256=86d412ccc1ba6d7c53e856d3b3683d4a6bdf91d39808410364d1a35bab9cf292"] - ["0003-Use-Coq-platform-supplied-Flocq.patch" "sha256=13ad400aa972dacb925376c2168b4b9be28f372b4ba42be35fbeae47c9a6773c"] + ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] + ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] + ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] + ["0010-Added-open-source-build-to-makefile.patch" "sha256=fc3b8c1e097b53f209e7cf2e9b2e822609e8370857dbf1a4b34d909c37dcdfb5"] + ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] + ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] ] install: [ [make "install_open_source"] @@ -35,10 +41,11 @@ install: [ depends: [ "coq" {>= "8.7.0" & < "8.12"} "coq-flocq" {>= "3.2.1"} + "coq-menhirlib" {>= "20190626" & < "20200123"} "menhir" {>= "20190626" & < "20200123"} "ocaml" {>= "4.05.0"} ] -synopsis: "The CompCert C compiler (only open source files + Builtins1.vo)" +synopsis: "The CompCert C compiler (only open source files + using coq-platform)" tags: [ "category:CS/Semantics and Compilation/Compilation" "category:CS/Semantics and Compilation/Semantics"