Opam: coq-metacoq-template: add additional make fix

opam/opam-coq-archive/released/packages/coq-metacoq-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" ]]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam

@@ -20,6 +20,7 @@ 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"]

opam/opam-coq-archive/released/packages/coq-metacoq-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" ]]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam

@@ -20,6 +20,7 @@ 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"]

opam/opam-coq-archive/released/packages/coq-metacoq-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" ]]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam

@@ -19,6 +19,7 @@ authors: ["Abhishek Anand <[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"]

opam/opam-coq-archive/released/packages/coq-metacoq-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" ]]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam

@@ -19,6 +19,7 @@ authors: ["Abhishek Anand <[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"]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/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" ]]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam

@@ -19,6 +19,7 @@ authors: ["Abhishek Anand <[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"]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/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" ]]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam

@@ -19,6 +19,7 @@ authors: ["Abhishek Anand <[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"]