Skip to content

Commit

Permalink
Include CompCert license file update to resolve issues with open source
Browse files Browse the repository at this point in the history 
variant
Use opam supplied version of MenhirLib
  • Loading branch information
@MSoegtropIMC
MSoegtropIMC committed May 5, 2020
1 parent 818bcb3 commit 4585d17
Show file tree
Hide file tree
Showing 13 changed files with 267 additions and 23 deletions.
3 changes: 2 additions & 1 deletion ...rt.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <[email protected]>
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.
Expand Down
60 changes: 60 additions & 0 deletions ...rt.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <[email protected]>
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)

28 changes: 28 additions & 0 deletions ...ert/coq-compcert.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <[email protected]>
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)

10 changes: 5 additions & 5 deletions ...003-Use-Coq-platform-supplied-Flocq.patch → ...011-Use-Coq-platform-supplied-Flocq.patch
View file
Original file line number Diff line number Diff line change
@@ -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 <[email protected]>
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 +-
Expand All @@ -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.
Expand All @@ -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 @@
Expand Down
26 changes: 26 additions & 0 deletions ...rt.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <[email protected]>
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)

13 changes: 10 additions & 3 deletions opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,18 +20,25 @@ 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"]
]
depends: [
"coq" {>= "8.7.0" & < "8.12"}
"coq-flocq" {>= "3.2.1"}
"coq-menhirlib" {>= "20190626" & < "20200123"}
"menhir" {>= "20190626" & < "20200123"}
"ocaml" {>= "4.05.0"}
]
Expand Down
3 changes: 2 additions & 1 deletion ...latform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <[email protected]>
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.
Expand Down
60 changes: 60 additions & 0 deletions ...latform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <[email protected]>
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)

28 changes: 28 additions & 0 deletions ...cert.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <[email protected]>
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)

4 changes: 2 additions & 2 deletions ...Added-open-source-build-to-makefile.patch → ...Added-open-source-build-to-makefile.patch
View file
Original file line number Diff line number Diff line change
@@ -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 <[email protected]>
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 +++++++++++++++++++++++++++++++++---
Expand Down
10 changes: 5 additions & 5 deletions ...003-Use-Coq-platform-supplied-Flocq.patch → ...011-Use-Coq-platform-supplied-Flocq.patch
View file
Original file line number Diff line number Diff line change
@@ -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 <[email protected]>
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 +-
Expand All @@ -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.
Expand All @@ -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 @@
Expand Down
26 changes: 26 additions & 0 deletions ...latform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <[email protected]>
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)

19 changes: 13 additions & 6 deletions opam-prerelease/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,24 +21,31 @@ 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"]
]
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"
Expand Down

0 comments on commit 4585d17

Please sign in to comment.