From b2f0adda1ee9d0361b0339dddff4e6058c71905c Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 20 Apr 2020 14:49:31 +0200 Subject: [PATCH] Added latest CompCert version (3.7) and platform Flocq variant of CompCert --- .../coq-compcert/coq-compcert.3.7/opam | 41 +++++++ .../files/copy_ini_to_coqlib.patch | 12 ++ .../files/platform-flocq.patch | 104 ++++++++++++++++++ .../coq-compcert.3.7~platform-flocq/opam | 48 ++++++++ 4 files changed, 205 insertions(+) create mode 100644 released/packages/coq-compcert/coq-compcert.3.7/opam create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/platform-flocq.patch create mode 100644 released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam 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 0000000000..c77b51f439 --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7/opam @@ -0,0 +1,41 @@ +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"] + ["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/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch b/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/files/copy_ini_to_coqlib.patch new file mode 100644 index 0000000000..1a9eb14ed2 --- /dev/null +++ b/released/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 new file mode 100644 index 0000000000..10fd7ea471 --- /dev/null +++ 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 new file mode 100644 index 0000000000..cd3bf4e3ed --- /dev/null +++ b/released/packages/coq-compcert/coq-compcert.3.7~platform-flocq/opam @@ -0,0 +1,48 @@ +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: ["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" +}