Added latest CompCert version (3.7) and platform Flocq variant of Com…

…pCert
coq · Apr 20, 2020 · b2f0add · b2f0add
1 parent bd98187
commit b2f0add
Show file tree

Hide file tree

Showing 4 changed files with 205 additions and 0 deletions.
diff --git a/released/packages/coq-compcert/coq-compcert.3.7/opam b/released/packages/coq-compcert/coq-compcert.3.7/opam
@@ -0,0 +1,41 @@
+opam-version: "2.0"
+authors: "Xavier Leroy <[email protected]>"
+maintainer: "Jacques-Henri Jourdan <[email protected]>"
+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/...ased/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch b/...ased/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch
@@ -0,0 +1,12 @@
+diff --git a/Makefile b/Makefile
+index af069e3f..46133788 100644
+--- a/Makefile
++++ b/Makefile
+@@ -253,6 +253,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
@@ -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
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+authors: "Xavier Leroy <[email protected]>"
+maintainer: "Jacques-Henri Jourdan <[email protected]>"
+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=a7ec83d8b66f0ae28cb352f0c34fe7b6482ded46534746c041468a02f15c2161"]
+]
+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"
+}