Merge pull request #1319 from MSoegtropIMC/compcert64-3.7-b

Changed installation target folders for 64 bit CompCert
coq · Jun 29, 2020 · 68db542 · 68db542
2 parents bb98ea6 + 2b9a8e3
commit 68db542
Show file tree

Hide file tree

Showing 3 changed files with 45 additions and 12 deletions.
diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7/opam
@@ -9,11 +9,10 @@ build: [
   ["./configure" "amd64-linux" {os = "linux"}
   "amd64-macosx" {os = "macos"}
   "amd64-cygwin" {os = "cygwin"}
-  "-bindir" "%{bin}%"
-  "-libdir" "%{lib}%/compcert"
+  "-prefix" "%{prefix}%/variants/compcert64"
   "-install-coqdev"
   "-clightgen"
-  "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64"
+  "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert"
   "-ignore-coq-version"]
   [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
 ]
@@ -25,7 +24,19 @@ depends: [
   "menhir" {>= "20190626" & < "20200123"}
   "ocaml" {>= "4.05.0"}
 ]
-synopsis: "The CompCert C compiler"
+synopsis: "The CompCert C compiler (64 bit)"
+description: "This package installs the 64 bit version of CompCert.
+For coexistence with the 32 bit version, the files are installed in:
+%{prefix}%/variants/compcert64/bin  (ccomp and clightgen binaries)
+%{prefix}%/variants/compcert64/lib/compcert  (C library)
+%{lib}%/coq/user-contrib/compcert64  (Coq library)
+Please note that the coq module path is compcert and not compcert64,
+so the files cannot be directly Required as compcert64.
+Instead -Q or -R options must be used to bind the compcert64 folder
+to the module path compcert. This is more convenient if one development
+uses both 32 and 64 bit versions. Otherwise all files would have to
+be duplicated with module paths compcert and compcert64.
+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"

diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam
@@ -10,11 +10,10 @@ build: [
   ["./configure" "amd64-linux" {os = "linux"}
   "amd64-macosx" {os = "macos"}
   "amd64-cygwin" {os = "cygwin"}
-  "-bindir" "%{bin}%"
-  "-libdir" "%{lib}%/compcert"
+  "-prefix" "%{prefix}%/variants/compcert64"
   "-install-coqdev"
   "-clightgen"
-  "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64"
+  "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert"
   "-ignore-coq-version"]
   [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
 ]
@@ -42,7 +41,19 @@ depends: [
   "menhir" {>= "20190626" & < "20200123"}
   "ocaml" {>= "4.05.0"}
 ]
-synopsis: "The CompCert C compiler (using coq-platform supplied version of Flocq)"
+synopsis: "The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)"
+description: "This package installs the 64 bit version of CompCert.
+For coexistence with the 32 bit version, the files are installed in:
+%{prefix}%/variants/compcert64/bin  (ccomp and clightgen binaries)
+%{prefix}%/variants/compcert64/lib/compcert  (C library)
+%{lib}%/coq/user-contrib/compcert64  (Coq library)
+Please note that the coq module path is compcert and not compcert64,
+so the files cannot be directly Required as compcert64.
+Instead -Q or -R options must be used to bind the compcert64 folder
+to the module path compcert. This is more convenient if one development
+uses both 32 and 64 bit versions. Otherwise all files would have to
+be duplicated with module paths compcert and compcert64.
+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"

diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam
@@ -10,11 +10,10 @@ build: [
   ["./configure" "amd64-linux" {os = "linux"}
   "amd64-macosx" {os = "macos"}
   "amd64-cygwin" {os = "cygwin"}
-  "-bindir" "%{bin}%"
-  "-libdir" "%{lib}%/compcert"
+  "-prefix" "%{prefix}%/variants/compcert64"
   "-install-coqdev"
   "-clightgen"
-  "-coqdevdir" "%{lib}%/coq/user-contrib/compcert64"
+  "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert"
   "-ignore-coq-version"]
   [make "depend"]
   [make "-j%{jobs}%" {ocaml:version >= "4.06"} "proof_open_source"]
@@ -45,7 +44,19 @@ depends: [
   "menhir" {>= "20190626" & < "20200123"}
   "ocaml" {>= "4.05.0"}
 ]
-synopsis: "The CompCert C compiler (only open source files + using coq-platform)"
+synopsis: "The CompCert C compiler (64 bit, only open source files + using coq-platform)"
+description: "This package installs the 64 bit version of CompCert.
+For coexistence with the 32 bit version, the files are installed in:
+%{prefix}%/variants/compcert64/bin  (ccomp and clightgen binaries)
+%{prefix}%/variants/compcert64/lib/compcert  (C library)
+%{lib}%/coq/user-contrib/compcert64  (Coq library)
+Please note that the coq module path is compcert and not compcert64,
+so the files cannot be directly Required as compcert64.
+Instead -Q or -R options must be used to bind the compcert64 folder
+to the module path compcert. This is more convenient if one development
+uses both 32 and 64 bit versions. Otherwise all files would have to
+be duplicated with module paths compcert and compcert64.
+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"