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..f58109163 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7/opam @@ -0,0 +1,40 @@ +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"] +] +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~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..d160e66e2 --- /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,82 @@ +From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Wed, 29 Apr 2020 15:40:13 +0200 +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. + +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/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/0011-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 new file mode 100644 index 000000000..0dc512b45 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch @@ -0,0 +1,123 @@ +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 11/12] 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 24431cb2..6c5655d8 100644 +--- a/aarch64/Archi.v ++++ b/aarch64/Archi.v +@@ -16,7 +16,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 6a126c3f..25a55620 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/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 new file mode 100644 index 000000000..7592e3b84 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam @@ -0,0 +1,57 @@ +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: [ + "0001-Install-compcert.config-file-along-the-Coq-developme.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=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"] +] +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 (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-04-29" +] +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~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..d160e66e2 --- /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,82 @@ +From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001 +From: Xavier Leroy +Date: Wed, 29 Apr 2020 15:40:13 +0200 +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. + +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/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/0010-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 new file mode 100644 index 000000000..28dbd0687 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch @@ -0,0 +1,106 @@ +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 10/12] 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/0011-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 new file mode 100644 index 000000000..0dc512b45 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch @@ -0,0 +1,123 @@ +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 11/12] 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 24431cb2..6c5655d8 100644 +--- a/aarch64/Archi.v ++++ b/aarch64/Archi.v +@@ -16,7 +16,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 6a126c3f..25a55620 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/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 new file mode 100644 index 000000000..8a4d7b390 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam @@ -0,0 +1,60 @@ +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" + "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=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"] +] +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 + using coq-platform)" +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" +}