coq · palmskog · Dec 28, 2020 · Dec 28, 2020
diff --git a/...packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch b/...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 <[email protected]>
+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
@@ -0,0 +1,61 @@
+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"
+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/...a-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch b/...a-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 <[email protected]>
+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
@@ -1,45 +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"
+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 <[email protected]>"
-flags: light-uninstall
 url {
   src: "git+https://github.com/AbsInt/CompCert.git"
 }