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

…pCert

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"
+}

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.

released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam

@@ -0,0 +1,45 @@
+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"
+extra-files: ["platform-flocq.patch" "sha256=36371f28651ac2310b96ea4e3fc6bf2a0c48074e088da46de6cc45458b8b4d82"]
+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"
+}