Merge pull request #421 from MSoegtropIMC/fix-coq-metacoq-template

Fix coq metacoq template
coq · Jul 10, 2024 · d446c8e · d446c8e
2 parents 499489d + bbeb04c
commit d446c8e
Show file tree

Hide file tree

Showing 14 changed files with 618 additions and 1 deletion.
diff --git a/...etacoq-template/coq-metacoq-template.1.1+8.15/files/Fix make issues Coq Platform CI.patch b/...etacoq-template/coq-metacoq-template.1.1+8.15/files/Fix make issues Coq Platform CI.patch
@@ -0,0 +1,52 @@
+From 9cdb37bb79af1c37e2fba8b8cdd6f806108e4b85 Mon Sep 17 00:00:00 2001
+From: Matthieu Sozeau <[email protected]>
+Date: Mon, 8 Jul 2024 10:47:12 +0200
+Subject: [PATCH] Fix make issues (Coq Platform CI)
+
+---
+ erasure-plugin/clean_extraction.sh     | 2 +-
+ pcuic/clean_extraction.sh              | 2 +-
+ safechecker-plugin/clean_extraction.sh | 2 +-
+ translations/param_binary.v            | 2 +-
+ translations/param_original.v          | 2 +-
+ 5 files changed, 5 insertions(+), 5 deletions(-)
+
+diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh
+index 4187f6ddc..562a941fa 100755
+--- a/erasure-plugin/clean_extraction.sh
++++ b/erasure-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
+            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]
+diff --git a/pcuic/clean_extraction.sh b/pcuic/clean_extraction.sh
+index d8ce50aff..7c5f8a0de 100755
+--- a/pcuic/clean_extraction.sh
++++ b/pcuic/clean_extraction.sh
+@@ -4,7 +4,7 @@ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+ echo "Cleaning result of extraction"
+
+-files=`cat ../template-coq/_PluginProject ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ cd src
+ # Move extracted modules to build the certicoq compiler plugin
+diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh
+index 44164597f..85e2f761a 100755
+--- a/safechecker-plugin/clean_extraction.sh
++++ b/safechecker-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" ||
+            "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]]
diff --git a/...pam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam b/...pam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam
@@ -20,9 +20,11 @@ authors: ["Abhishek Anand <[email protected]>"
 license: "MIT"
 patches: [
   "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch"
+  "Fix make issues Coq Platform CI.patch"
 ]
 build: [
   ["bash" "./configure.sh"]
+  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "template-coq"]
 ]
 install: [

diff --git a/...q-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch b/...q-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch
@@ -0,0 +1,29 @@
+From 838930ef5983c0e19bd9e12ddb5b12cf5b367c8e Mon Sep 17 00:00:00 2001
+From: Michael Soegtrop <[email protected]>
+Date: Fri, 30 Sep 2022 09:15:08 +0200
+Subject: [PATCH] Fix line ending issues with generated code on Windows
+
+---
+ template-coq/update_plugin.sh | 6 ++++++
+ 1 file changed, 6 insertions(+)
+
+diff --git a/template-coq/update_plugin.sh b/template-coq/update_plugin.sh
+index 9b3d2a5f..1842cfde 100755
+--- a/template-coq/update_plugin.sh
++++ b/template-coq/update_plugin.sh
+@@ -12,6 +12,12 @@ then
+     echo "Renaming files to camelCase"
+     (cd gen-src; ./to-lower.sh)
+     rm -f gen-src/*.d gen-src/*.cm*
++    echo "Prepare line endings for patching (for Windows)"
++    for f in gen-src/*.ml*
++    do
++      tr -d '\r' < "$f" > tmp
++      mv -f tmp $f
++    done
+     # Fix an extraction bug: wrong type annotation on eq_equivalence
+     patch -N -p0 < extraction.patch
+     patch -N -p0 < specFloat.patch
+-- 
+2.37.3
+
diff --git a/...etacoq-template/coq-metacoq-template.1.1+8.16/files/Fix make issues Coq Platform CI.patch b/...etacoq-template/coq-metacoq-template.1.1+8.16/files/Fix make issues Coq Platform CI.patch
@@ -0,0 +1,52 @@
+From 9cdb37bb79af1c37e2fba8b8cdd6f806108e4b85 Mon Sep 17 00:00:00 2001
+From: Matthieu Sozeau <[email protected]>
+Date: Mon, 8 Jul 2024 10:47:12 +0200
+Subject: [PATCH] Fix make issues (Coq Platform CI)
+
+---
+ erasure-plugin/clean_extraction.sh     | 2 +-
+ pcuic/clean_extraction.sh              | 2 +-
+ safechecker-plugin/clean_extraction.sh | 2 +-
+ translations/param_binary.v            | 2 +-
+ translations/param_original.v          | 2 +-
+ 5 files changed, 5 insertions(+), 5 deletions(-)
+
+diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh
+index 4187f6ddc..562a941fa 100755
+--- a/erasure-plugin/clean_extraction.sh
++++ b/erasure-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
+            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]
+diff --git a/pcuic/clean_extraction.sh b/pcuic/clean_extraction.sh
+index d8ce50aff..7c5f8a0de 100755
+--- a/pcuic/clean_extraction.sh
++++ b/pcuic/clean_extraction.sh
+@@ -4,7 +4,7 @@ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+ echo "Cleaning result of extraction"
+
+-files=`cat ../template-coq/_PluginProject ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ cd src
+ # Move extracted modules to build the certicoq compiler plugin
+diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh
+index 44164597f..85e2f761a 100755
+--- a/safechecker-plugin/clean_extraction.sh
++++ b/safechecker-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" ||
+            "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]]
diff --git a/...pam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam b/...pam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam
@@ -0,0 +1,58 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <[email protected]>"
+          "Danil Annenkov <[email protected]>"
+          "Simon Boulier <[email protected]>"
+          "Cyril Cohen <[email protected]>"
+          "Yannick Forster <[email protected]>"
+          "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
+          "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
+          "Matthieu Sozeau <[email protected]>"
+          "Nicolas Tabareau <[email protected]>"
+          "Théo Winterhalter <[email protected]>"
+]
+license: "MIT"
+patches: [
+  "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch"
+  "Fix make issues Coq Platform CI.patch"
+]
+build: [
+  ["bash" "./configure.sh"]
+  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
+  [make "-j" "%{jobs}%" "template-coq"]
+]
+install: [
+  [make "-C" "template-coq" "install"]
+]
+depends: [
+  "stdlib-shims"
+  "coq" { >= "8.16" & < "8.17~" }
+  "coq-equations" { >= "1.3" }
+]
+synopsis: "A quoting and unquoting library for Coq in Coq"
+description: """
+MetaCoq is a meta-programming framework for Coq.
+
+Template Coq is a quoting library for Coq. It takes Coq terms and
+constructs a representation of their syntax tree as a Coq inductive data
+type. The representation is based on the kernel's term representation.
+
+In addition to a complete reification and denotation of CIC terms,
+Template Coq includes:
+
+- Reification of the environment structures, for constant and inductive declarations.
+- Denotation of terms and global declarations
+- A monad for manipulating global declarations, calling the type
+  checker, and inserting them in the global environment, in the style of
+  MetaCoq/MTac.
+"""
+url {
+  src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.16.tar.gz"
+  checksum: "sha512=abd34042fc2804954abc8b1fba4c2b3d1d1c0c780874ad0cbe698a19756e26985c77bb231b2e9b40ea01261f3fbbb36fbdd2b7095931e947bf933359cb0154f7"
+}
diff --git a/...etacoq-template/coq-metacoq-template.1.2+8.16/files/Fix make issues Coq Platform CI.patch b/...etacoq-template/coq-metacoq-template.1.2+8.16/files/Fix make issues Coq Platform CI.patch
@@ -0,0 +1,52 @@
+From 9cdb37bb79af1c37e2fba8b8cdd6f806108e4b85 Mon Sep 17 00:00:00 2001
+From: Matthieu Sozeau <[email protected]>
+Date: Mon, 8 Jul 2024 10:47:12 +0200
+Subject: [PATCH] Fix make issues (Coq Platform CI)
+
+---
+ erasure-plugin/clean_extraction.sh     | 2 +-
+ pcuic/clean_extraction.sh              | 2 +-
+ safechecker-plugin/clean_extraction.sh | 2 +-
+ translations/param_binary.v            | 2 +-
+ translations/param_original.v          | 2 +-
+ 5 files changed, 5 insertions(+), 5 deletions(-)
+
+diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh
+index 4187f6ddc..562a941fa 100755
+--- a/erasure-plugin/clean_extraction.sh
++++ b/erasure-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
+            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]
+diff --git a/pcuic/clean_extraction.sh b/pcuic/clean_extraction.sh
+index d8ce50aff..7c5f8a0de 100755
+--- a/pcuic/clean_extraction.sh
++++ b/pcuic/clean_extraction.sh
+@@ -4,7 +4,7 @@ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+ echo "Cleaning result of extraction"
+
+-files=`cat ../template-coq/_PluginProject ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ cd src
+ # Move extracted modules to build the certicoq compiler plugin
+diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh
+index 44164597f..85e2f761a 100755
+--- a/safechecker-plugin/clean_extraction.sh
++++ b/safechecker-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" ||
+            "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]]
diff --git a/...pam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam b/...pam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam
@@ -0,0 +1,54 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <[email protected]>"
+          "Danil Annenkov <[email protected]>"
+          "Simon Boulier <[email protected]>"
+          "Cyril Cohen <[email protected]>"
+          "Yannick Forster <[email protected]>"
+          "Jason Gross <[email protected]>"
+          "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
+          "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
+          "Matthieu Sozeau <[email protected]>"
+          "Nicolas Tabareau <[email protected]>"
+          "Théo Winterhalter <[email protected]>"
+]
+license: "MIT"
+patches: [ "Fix make issues Coq Platform CI.patch" ]
+build: [
+  ["bash" "./configure.sh"]
+  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
+  [make "-j" "%{jobs}%" "template-coq"]
+]
+install: [
+  [make "-C" "template-coq" "install"]
+]
+depends: [
+  "coq-metacoq-common" {= version}
+]
+synopsis: "A quoting and unquoting library for Coq in Coq"
+description: """
+MetaCoq is a meta-programming framework for Coq.
+
+Template Coq is a quoting library for Coq. It takes Coq terms and
+constructs a representation of their syntax tree as a Coq inductive data
+type. The representation is based on the kernel's term representation.
+
+In addition to a complete reification and denotation of CIC terms,
+Template Coq includes:
+
+- Reification of the environment structures, for constant and inductive declarations.
+- Denotation of terms and global declarations
+- A monad for manipulating global declarations, calling the type
+  checker, and inserting them in the global environment, in the style of
+  MetaCoq/MTac.
+"""
+url {
+  src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.16.tar.gz"
+  checksum: "sha512=1fc976740f2ff5a6c4137cf4722e09cae5765d0d71f55e6a020883218396856558a6534aa7d2bd192b60778427edbbc2f096a0e738e95551808702613edbbb31"
+}
diff --git a/...etacoq-template/coq-metacoq-template.1.2+8.17/files/Fix make issues Coq Platform CI.patch b/...etacoq-template/coq-metacoq-template.1.2+8.17/files/Fix make issues Coq Platform CI.patch
@@ -0,0 +1,52 @@
+From 9cdb37bb79af1c37e2fba8b8cdd6f806108e4b85 Mon Sep 17 00:00:00 2001
+From: Matthieu Sozeau <[email protected]>
+Date: Mon, 8 Jul 2024 10:47:12 +0200
+Subject: [PATCH] Fix make issues (Coq Platform CI)
+
+---
+ erasure-plugin/clean_extraction.sh     | 2 +-
+ pcuic/clean_extraction.sh              | 2 +-
+ safechecker-plugin/clean_extraction.sh | 2 +-
+ translations/param_binary.v            | 2 +-
+ translations/param_original.v          | 2 +-
+ 5 files changed, 5 insertions(+), 5 deletions(-)
+
+diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh
+index 4187f6ddc..562a941fa 100755
+--- a/erasure-plugin/clean_extraction.sh
++++ b/erasure-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
+            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]
+diff --git a/pcuic/clean_extraction.sh b/pcuic/clean_extraction.sh
+index d8ce50aff..7c5f8a0de 100755
+--- a/pcuic/clean_extraction.sh
++++ b/pcuic/clean_extraction.sh
+@@ -4,7 +4,7 @@ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+ echo "Cleaning result of extraction"
+
+-files=`cat ../template-coq/_PluginProject ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ cd src
+ # Move extracted modules to build the certicoq compiler plugin
+diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh
+index 44164597f..85e2f761a 100755
+--- a/safechecker-plugin/clean_extraction.sh
++++ b/safechecker-plugin/clean_extraction.sh
+@@ -9,7 +9,7 @@ fi
+
+ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
+
+-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
++files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+
+ if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" ||
+            "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]]