diff --git a/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch b/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch new file mode 100755 index 000000000..52c92775f --- /dev/null +++ b/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch @@ -0,0 +1,44 @@ +From b2f8e4d0fdea4611b56f8e2c2feade3e8fb632b7 Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Sun, 27 Dec 2020 15:18:54 +0100 +Subject: [PATCH] Allow dev version of Menhir + +--- + configure | 14 +++++++++++++- + 1 file changed, 13 insertions(+), 1 deletion(-) + +diff --git a/configure b/configure +index 7cbb9d7d..4c494379 100755 +--- a/configure ++++ b/configure +@@ -556,7 +556,7 @@ fi + + MENHIR_REQUIRED=20190626 + echo "Testing Menhir... " | tr -d '\n' +-menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` ++menhir_ver=$(menhir --version 2>/dev/null | sed -n -E -e 's/^.*version (unreleased|[0-9]*).*$/\1/p') + case "$menhir_ver" in + 20[0-9][0-9][0-9][0-9][0-9][0-9]) + if test "$menhir_ver" -ge $MENHIR_REQUIRED; then +@@ -576,6 +576,18 @@ case "$menhir_ver" in + echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." + missingtools=true + fi;; ++ unreleased) ++ echo "version $menhir_ver -- acceptable!" ++ menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ ++ menhir_dir=$(menhir --suggest-menhirLib) || \ ++ menhir_dir="" ++ menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') ++ if test ! -d "$menhir_dir"; then ++ echo "Error: cannot determine the location of the Menhir API library." ++ echo "This can be due to an incorrect Menhir package." ++ echo "Consider using the OPAM package for Menhir." ++ missingtools=true ++ fi;; + *) + echo "NOT FOUND" + echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed." +-- +2.29.2 + diff --git a/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam b/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam new file mode 100755 index 000000000..beabd314e --- /dev/null +++ b/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam @@ -0,0 +1,61 @@ +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" +available: os != "macos" +patches: [ "0001-Allow-dev-version-of-Menhir.patch" ] +build: [ + ["./configure" + "ia32-linux" {os = "linux"} + "ia32-cygwin" {os = "cygwin"} + # This is for building a MinGW CompCert with cygwin host and cygwin target + "ia32-cygwin" {os = "win32" & os-distribution = "cygwinports"} + # This is for building a 32 bit CompCert on 64 bit MinGW with cygwin build host + "-toolprefix" {os = "win32" & os-distribution = "cygwinports" & arch = "x86_64"} + "i686-pc-cygwin-" {os = "win32" & os-distribution = "cygwinports" & arch = "x86_64"} + # The 32 bit CompCert is a variant which is installed in a non standard folder + "-prefix" "%{prefix}%/variants/compcert32" + "-install-coqdev" + "-clightgen" + "-use-external-Flocq" + "-use-external-MenhirLib" + "-coqdevdir" "%{lib}%/coq-variant/compcert32/compcert" + "-ignore-coq-version"] + [make "-j%{jobs}%" {ocaml:version >= "4.06"}] +] +install: [ + [make "install"] +] +depends: [ + "coq" {>= "8.8" | = "dev"} + "menhir" {>= "20190626" | = "dev"} + "ocaml" {>= "4.05.0"} + "coq-flocq" {>= "3.1.0" | = "dev"} + "coq-menhirlib" {>= "20190626" | = "dev"} +] +synopsis: "The CompCert C compiler (32 bit)" +description: "This package installs the 32 bit version of CompCert. +For coexistence with the 64 bit version, the files are installed in: +%{prefix}%/variants/compcert32/bin (ccomp and clightgen binaries) +%{prefix}%/variants/compcert32/lib/compcert (C library) +%{lib}%/coq-variant/compcert32/compcert (Coq library) +Please note that the coq module path is compcert and not compcert32, +so the files cannot be directly Required as compcert32. +Instead -Q or -R options must be used to bind the compcert32 folder +to the module path compcert. This is more convenient if one development +supports both 32 and 64 bit versions. Otherwise all files would have to +be duplicated with module paths compcert and compcert32. +Please also note that the binary folder is usually not in the path." +tags: [ + "category:CS/Semantics and Compilation/Compilation" + "category:CS/Semantics and Compilation/Semantics" + "keyword:C" + "keyword:compiler" + "logpath:compcert32" +] +url { + src: "git+https://github.com/AbsInt/CompCert.git" +} diff --git a/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch b/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch new file mode 100755 index 000000000..52c92775f --- /dev/null +++ b/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch @@ -0,0 +1,44 @@ +From b2f8e4d0fdea4611b56f8e2c2feade3e8fb632b7 Mon Sep 17 00:00:00 2001 +From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> +Date: Sun, 27 Dec 2020 15:18:54 +0100 +Subject: [PATCH] Allow dev version of Menhir + +--- + configure | 14 +++++++++++++- + 1 file changed, 13 insertions(+), 1 deletion(-) + +diff --git a/configure b/configure +index 7cbb9d7d..4c494379 100755 +--- a/configure ++++ b/configure +@@ -556,7 +556,7 @@ fi + + MENHIR_REQUIRED=20190626 + echo "Testing Menhir... " | tr -d '\n' +-menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` ++menhir_ver=$(menhir --version 2>/dev/null | sed -n -E -e 's/^.*version (unreleased|[0-9]*).*$/\1/p') + case "$menhir_ver" in + 20[0-9][0-9][0-9][0-9][0-9][0-9]) + if test "$menhir_ver" -ge $MENHIR_REQUIRED; then +@@ -576,6 +576,18 @@ case "$menhir_ver" in + echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." + missingtools=true + fi;; ++ unreleased) ++ echo "version $menhir_ver -- acceptable!" ++ menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ ++ menhir_dir=$(menhir --suggest-menhirLib) || \ ++ menhir_dir="" ++ menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') ++ if test ! -d "$menhir_dir"; then ++ echo "Error: cannot determine the location of the Menhir API library." ++ echo "This can be due to an incorrect Menhir package." ++ echo "Consider using the OPAM package for Menhir." ++ missingtools=true ++ fi;; + *) + echo "NOT FOUND" + echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed." +-- +2.29.2 + diff --git a/extra-dev/packages/coq-compcert/coq-compcert.dev/opam b/extra-dev/packages/coq-compcert/coq-compcert.dev/opam index 81e8b5683..2dfefcfb2 100644 --- a/extra-dev/packages/coq-compcert/coq-compcert.dev/opam +++ b/extra-dev/packages/coq-compcert/coq-compcert.dev/opam @@ -1,45 +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" +patches: [ "0001-Allow-dev-version-of-Menhir.patch" ] 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}%"] + ["./configure" + "amd64-linux" {os = "linux"} + "amd64-macosx" {os = "macos"} + "amd64-cygwin" {os = "cygwin"} + # This is for building a MinGW CompCert with cygwin host and cygwin target + "amd64-cygwin" {os = "win32" & os-distribution = "cygwinports"} + # This is for building a 64 bit CompCert on 32 bit MinGW with cygwin build host + "-toolprefix" {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} + "x86_64-pc-cygwin-" {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} + "-prefix" "%{prefix}%" + "-install-coqdev" + "-clightgen" + "-use-external-Flocq" + "-use-external-MenhirLib" + "-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/"] -] -remove: [ - ["rm" "%{bin}%/ccomp"] - ["rm" "%{bin}%/clightgen"] - ["rm" "-R" "%{lib}%/coq/user-contrib/compcert"] - ["rm" "%{share}%/compcert.ini"] ] depends: [ - "ocaml" - "coq" {>= "8.8"} - "menhir" {>= "20190626"} + "coq" {>= "8.8.0" | = "dev"} + "menhir" {>= "20190626" | = "dev"} + "ocaml" {>= "4.05.0"} + "coq-flocq" {>= "3.1.0" | = "dev"} + "coq-menhirlib" {>= "20190626" | = "dev"} +] +synopsis: "The CompCert C compiler (64 bit)" +tags: [ + "category:CS/Semantics and Compilation/Compilation" + "category:CS/Semantics and Compilation/Semantics" + "keyword:C" + "keyword:compiler" + "logpath:compcert" ] -synopsis: "The CompCert C compiler." -authors: "Xavier Leroy " -flags: light-uninstall url { src: "git+https://github.com/AbsInt/CompCert.git" }