From cc289addd67635607083fb569a92f22178aad07d Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Tue, 9 Jul 2024 10:27:35 +0200 Subject: [PATCH 1/3] Opam: patch coq-metacoq-template opam files to fix spurious CI issue --- .../coq-metacoq-template.1.1+8.15/opam | 1 + ...issues-with-generated-code-on-Window.patch | 29 ++++++++++ .../coq-metacoq-template.1.1+8.16/opam | 57 +++++++++++++++++++ .../coq-metacoq-template.1.2+8.16/opam | 53 +++++++++++++++++ .../coq-metacoq-template.1.2+8.17/opam | 53 +++++++++++++++++ .../coq-metacoq-template.1.2.1+8.18/opam | 53 +++++++++++++++++ .../coq-metacoq-template.1.3.1+8.19/opam | 53 +++++++++++++++++ 7 files changed, 299 insertions(+) create mode 100755 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch create mode 100755 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam 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 4c4a96c274..f4c8446f32 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 @@ -23,6 +23,7 @@ patches: [ ] build: [ ["bash" "./configure.sh"] + ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"] [make "-j" "%{jobs}%" "template-coq"] ] install: [ diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch new file mode 100755 index 0000000000..a420880d66 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-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 <7895506+MSoegtropIMC@users.noreply.github.com> +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/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 new file mode 100755 index 0000000000..dd47c27892 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam @@ -0,0 +1,57 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +license: "MIT" +patches: [ + "0001-Fix-line-ending-issues-with-generated-code-on-Window.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/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 new file mode 100644 index 0000000000..350211ed28 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam @@ -0,0 +1,53 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +license: "MIT" +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/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 new file mode 100644 index 0000000000..dd47266f3c --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam @@ -0,0 +1,53 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +homepage: "https://metacoq.github.io/metacoq" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.17" +bug-reports: "https://github.com/MetaCoq/metacoq/issues" +authors: ["Abhishek Anand " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +license: "MIT" +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.17.tar.gz" + checksum: "sha512=a5ce2f5d94120a00703331a3cfdb7d51653fb44adeba89fa84b5f76e711ee9f582a22551f81fd144dc974e3f05e58d85cd716f8fcf69ec89923bc64774d82668" +} 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 new file mode 100644 index 0000000000..813a7bced5 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam @@ -0,0 +1,53 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +homepage: "https://metacoq.github.io/metacoq" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" +bug-reports: "https://github.com/MetaCoq/metacoq/issues" +authors: ["Abhishek Anand " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +license: "MIT" +build: [ + ["bash" "./configure.sh"] + ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"] + [make "-j" "%{jobs}%" "-C" "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/v1.2.1-8.18.tar.gz" + checksum: "sha256=dd129826edd22e611f84cdc82f6486fc57343e13c8223ce041a3d0574b6f5262" +} 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 new file mode 100644 index 0000000000..8fa036ee46 --- /dev/null +++ b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam @@ -0,0 +1,53 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +homepage: "https://metacoq.github.io/metacoq" +dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main" +bug-reports: "https://github.com/MetaCoq/metacoq/issues" +authors: ["Abhishek Anand " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +license: "MIT" +build: [ + ["bash" "./configure.sh"] + ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"] + [make "-j" "%{jobs}%" "-C" "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/releases/download/v1.3.1-8.19/v1.3.1-8.19.tar.gz" + checksum: "sha512=ff4c46e4a86aebfda0673f1dbea0d27751007b103dfe686657fb29237ff24abb119daa41ee4e921be6772686350be81a07a558fb9ff44e619f93d6b6ffde4c26" +} From 79872efa6077905ad4265fc28f7f2dc9758a48d7 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Tue, 9 Jul 2024 10:28:25 +0200 Subject: [PATCH 2/3] Pick dev: update OCaml version to 4.14.2 --- package_picks/package-pick-dev.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-dev.sh b/package_picks/package-pick-dev.sh index bdaca3039d..0119afc8aa 100644 --- a/package_picks/package-pick-dev.sh +++ b/package_picks/package-pick-dev.sh @@ -31,7 +31,7 @@ COQ_PLATFORM_USE_DEV_REPOSITORY='Y' COQ_PLATFORM_VERSION_DESCRIPTION='This is the latest development version of Coq and all packages.' # The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way) -COQ_PLATFORM_OCAML_VERSION='4.13.1' +COQ_PLATFORM_OCAML_VERSION='4.14.2' ###################### PACKAGE SELECTION ##################### From bbeb04c9519cb1a081d1a40be254ff5442f80fc6 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Tue, 9 Jul 2024 15:49:15 +0200 Subject: [PATCH 3/3] Opam: coq-metacoq-template: add additional make fix --- .../Fix make issues Coq Platform CI.patch | 52 +++++++++++++++++++ .../coq-metacoq-template.1.1+8.15/opam | 1 + .../Fix make issues Coq Platform CI.patch | 52 +++++++++++++++++++ .../coq-metacoq-template.1.1+8.16/opam | 1 + .../Fix make issues Coq Platform CI.patch | 52 +++++++++++++++++++ .../coq-metacoq-template.1.2+8.16/opam | 1 + .../Fix make issues Coq Platform CI.patch | 52 +++++++++++++++++++ .../coq-metacoq-template.1.2+8.17/opam | 1 + .../Fix make issues Coq Platform CI.patch | 52 +++++++++++++++++++ .../coq-metacoq-template.1.2.1+8.18/opam | 1 + .../Fix make issues Coq Platform CI.patch | 52 +++++++++++++++++++ .../coq-metacoq-template.1.3.1+8.19/opam | 1 + 12 files changed, 318 insertions(+) create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/files/Fix make issues Coq Platform CI.patch create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/Fix make issues Coq Platform CI.patch create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/files/Fix make issues Coq Platform CI.patch create mode 100644 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/files/Fix make issues Coq Platform CI.patch create mode 100644 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 create mode 100644 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 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"]