From 4585d17709d583aae69ec05d53ecc446e744f9da Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Tue, 5 May 2020 18:34:18 +0200 Subject: [PATCH] Include CompCert license file update to resolve issues with open source variant Use opam supplied version of MenhirLib --- ....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 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch create mode 100644 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch rename opam-prerelease/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 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch create mode 100644 opam-prerelease/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 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch rename opam-prerelease/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 opam-prerelease/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 opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch index 63df61d08c..d160e66e23 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/opam-prerelease/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 0000000000..f74202a53c --- /dev/null +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch new file mode 100644 index 0000000000..57bef5e519 --- /dev/null +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch similarity index 93% rename from opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch rename to opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch index 1adbba4b55..0dc512b457 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0003-Use-Coq-platform-supplied-Flocq.patch +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/opam-prerelease/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 0000000000..58a641f077 --- /dev/null +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam index bc1de523cf..7592e3b849 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch index 63df61d08c..d160e66e23 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/opam-prerelease/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 0000000000..f74202a53c --- /dev/null +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch b/opam-prerelease/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 0000000000..57bef5e519 --- /dev/null +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch b/opam-prerelease/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 opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch rename to opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch index 6c30f3edcb..28dbd06878 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0002-Added-open-source-build-to-makefile.patch +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch similarity index 93% rename from opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch rename to opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch index 1adbba4b55..0dc512b457 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0003-Use-Coq-platform-supplied-Flocq.patch +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/opam-prerelease/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 0000000000..58a641f077 --- /dev/null +++ b/opam-prerelease/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/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam b/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam index d11bf2f00c..8a4d7b3907 100644 --- a/opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam +++ b/opam-prerelease/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"