diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/files/Fix make issues Coq Platform CI.patch b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/files/Fix make issues Coq Platform CI.patch new file mode 100644 index 0000000000..b5e461fccd --- /dev/null +++ b/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 +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/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam index f4c8446f32..c3e62c7d4d 100755 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam @@ -20,6 +20,7 @@ authors: ["Abhishek Anand " 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"] diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/Fix make issues Coq Platform CI.patch b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/Fix make issues Coq Platform CI.patch new file mode 100644 index 0000000000..b5e461fccd --- /dev/null +++ b/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 +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/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam index dd47c27892..2794b47f82 100755 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam @@ -20,6 +20,7 @@ authors: ["Abhishek Anand " 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"] diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/files/Fix make issues Coq Platform CI.patch b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/files/Fix make issues Coq Platform CI.patch new file mode 100644 index 0000000000..b5e461fccd --- /dev/null +++ b/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 +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/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam index 350211ed28..cc8534f175 100644 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam @@ -19,6 +19,7 @@ authors: ["Abhishek Anand " "Théo Winterhalter " ] license: "MIT" +patches: [ "Fix make issues Coq Platform CI.patch" ] build: [ ["bash" "./configure.sh"] ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"] diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/files/Fix make issues Coq Platform CI.patch b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/files/Fix make issues Coq Platform CI.patch new file mode 100644 index 0000000000..b5e461fccd --- /dev/null +++ b/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 +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/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam index dd47266f3c..632bd70471 100644 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam @@ -19,6 +19,7 @@ authors: ["Abhishek Anand " "Théo Winterhalter " ] license: "MIT" +patches: [ "Fix make issues Coq Platform CI.patch" ] build: [ ["bash" "./configure.sh"] ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"] diff --git a/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 b/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 new file mode 100644 index 0000000000..b5e461fccd --- /dev/null +++ b/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 +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/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam index 813a7bced5..818a0e5ddf 100644 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam +++ b/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 " "Théo Winterhalter " ] license: "MIT" +patches: [ "Fix make issues Coq Platform CI.patch" ] build: [ ["bash" "./configure.sh"] ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"] diff --git a/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 b/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 new file mode 100644 index 0000000000..b5e461fccd --- /dev/null +++ b/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 +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/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam index 8fa036ee46..84af95bfff 100644 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam +++ b/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 " "Théo Winterhalter " ] license: "MIT" +patches: [ "Fix make issues Coq Platform CI.patch" ] build: [ ["bash" "./configure.sh"] ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]