From 8d88e4f5c5931cbc21e6f1312a5f0426e32e8d0a Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Thu, 14 Nov 2024 19:08:24 +0100 Subject: [PATCH] Add extra-files records where need to support opam 2.3.0 - Fixes #3203 --- .../coq-compcert-32/coq-compcert-32.dev/opam | 4 ++ .../coq-compcert/coq-compcert.dev/opam | 4 ++ extra-dev/packages/gappa/gappa.dev/opam | 4 ++ .../coq-compcert-32/coq-compcert-32.3.12/opam | 4 ++ .../coq-compcert-32/coq-compcert-32.3.8/opam | 4 ++ .../opam | 46 +++++++++++++---- .../opam | 51 +++++++++++++++---- .../coq-compcert-64.3.7~coq-platform/opam | 26 +++++++--- .../opam | 31 ++++++++--- .../coq-compcert/coq-compcert.2.0.0/opam | 2 +- .../coq-compcert/coq-compcert.2.3.2/opam | 2 +- .../coq-compcert/coq-compcert.2.4.0/opam | 2 +- .../coq-compcert/coq-compcert.2.7.1/opam | 2 +- .../coq-compcert/coq-compcert.3.12/opam | 4 ++ .../coq-compcert/coq-compcert.3.6+8.11/opam | 2 +- .../coq-compcert.3.7+8.12~coq_platform/opam | 46 +++++++++++++---- .../opam | 51 +++++++++++++++---- .../coq-compcert.3.7~coq-platform/opam | 26 +++++++--- .../opam | 31 ++++++++--- .../coq-compcert/coq-compcert.3.8/opam | 4 ++ .../coq-concurrency-pluto.1.0.0/opam | 2 +- .../coq-concurrency-pluto.1.1.0/opam | 2 +- .../coq-concurrency-proxy.1.0.0/opam | 2 +- .../coq-coquelicot/coq-coquelicot.3.1.0/opam | 4 ++ .../packages/coq-flocq/coq-flocq.3.3.1/opam | 4 ++ .../packages/coq-gappa/coq-gappa.1.4.4/opam | 4 ++ .../packages/coq-gappa/coq-gappa.1.4.5/opam | 4 ++ .../coq-geocoq-axioms.2.4.0/opam | 2 +- .../coq-geocoq-axioms.2.4.1/opam | 2 +- .../coq-geocoq-elements.2.4.0/opam | 2 +- .../coq-geocoq-elements.2.4.1/opam | 2 +- .../coq-geocoq-main.2.4.0/opam | 2 +- .../coq-geocoq-main.2.4.1/opam | 2 +- .../coq-geocoq-pof/coq-geocoq-pof.2.4.0/opam | 2 +- .../coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam | 2 +- .../coq-graph2tac/coq-graph2tac.1.0.anon/opam | 10 ++++ .../coq-interval/coq-interval.4.0.0/opam | 4 ++ .../coq-interval/coq-interval.4.1.0/opam | 4 ++ .../coq-io-hello-world.1.0.0/opam | 2 +- .../coq-io-hello-world.1.1.0/opam | 2 +- .../coq-mathcomp-analysis.0.7.0/opam | 4 ++ .../coq-metacoq-template.1.1+8.16/opam | 4 ++ .../coq-metacoq-translations.1.0+8.16/opam | 4 ++ .../packages/coq-mmaps/coq-mmaps.1.0/opam | 4 ++ .../packages/coq-mmaps/coq-mmaps.1.1/opam | 4 ++ .../coq-mtac2/coq-mtac2.1.4+8.19/opam | 4 ++ .../coq-of-ocaml/coq-of-ocaml.1.1.1/opam | 2 +- .../coq-of-ocaml/coq-of-ocaml.1.2.1/opam | 2 +- .../coq-of-ocaml/coq-of-ocaml.2.0.0/opam | 4 ++ .../coq-of-ocaml/coq-of-ocaml.2.1.0/opam | 4 ++ released/packages/coq-ott/coq-ott.0.32/opam | 4 ++ released/packages/coq-ott/coq-ott.0.33/opam | 4 ++ .../packages/coq-stdpp/coq-stdpp.1.5.0/opam | 4 ++ .../packages/coq-stdpp/coq-stdpp.1.6.0/opam | 4 ++ .../packages/coq-stdpp/coq-stdpp.1.8.0/opam | 4 ++ .../coq-text2tac/coq-text2tac.1.0/opam | 10 ++++ .../coq-unimath-category-theory.0.1.0/opam | 2 +- .../coq-unimath-dedekind.0.1.0/opam | 2 +- .../coq-unimath-foundations.0.1.0/opam | 2 +- .../coq-unimath-ktheory.0.1.0/opam | 2 +- .../opam | 2 +- .../coq-unimath-tactics.0.1.0/opam | 2 +- .../coq-vcfloat/coq-vcfloat.2.1.1/opam | 4 ++ .../packages/coq-vcfloat/coq-vcfloat.2.1/opam | 4 ++ .../packages/coq-vst-32/coq-vst-32.2.12/opam | 4 ++ .../packages/coq-vst-32/coq-vst-32.2.7/opam | 4 ++ .../packages/coq-vst-32/coq-vst-32.2.8/opam | 10 ++++ .../packages/coq-vst-32/coq-vst-32.2.9.1/opam | 4 ++ .../packages/coq-vst-64/coq-vst-64.2.6/opam | 4 ++ released/packages/coq-vst/coq-vst.2.12/opam | 4 ++ released/packages/coq-vst/coq-vst.2.6/opam | 4 ++ released/packages/coq-vst/coq-vst.2.7/opam | 4 ++ released/packages/coq-vst/coq-vst.2.8/opam | 4 ++ released/packages/coq-vst/coq-vst.2.9.1/opam | 4 ++ 74 files changed, 444 insertions(+), 94 deletions(-) diff --git a/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam b/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam index 51f53246ce..00da78cd4e 100755 --- a/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam +++ b/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam @@ -59,3 +59,7 @@ tags: [ url { src: "git+https://github.com/AbsInt/CompCert.git" } +extra-files: [ + "0001-Allow-dev-version-of-Menhir.patch" + "sha512=76f4222174fe2ff396ccef236b249a5094f4258459c3d74a074e714ddab7da6ea22d66a264386202988e16e6e5713c7ef06c043751890369e0c35c5915e2c832" +] diff --git a/extra-dev/packages/coq-compcert/coq-compcert.dev/opam b/extra-dev/packages/coq-compcert/coq-compcert.dev/opam index 58827aab78..12332f0303 100644 --- a/extra-dev/packages/coq-compcert/coq-compcert.dev/opam +++ b/extra-dev/packages/coq-compcert/coq-compcert.dev/opam @@ -46,3 +46,7 @@ tags: [ url { src: "git+https://github.com/AbsInt/CompCert.git" } +extra-files: [ + "0001-Allow-dev-version-of-Menhir.patch" + "sha512=76f4222174fe2ff396ccef236b249a5094f4258459c3d74a074e714ddab7da6ea22d66a264386202988e16e6e5713c7ef06c043751890369e0c35c5915e2c832" +] diff --git a/extra-dev/packages/gappa/gappa.dev/opam b/extra-dev/packages/gappa/gappa.dev/opam index f5dfdc374f..03e0eb067f 100755 --- a/extra-dev/packages/gappa/gappa.dev/opam +++ b/extra-dev/packages/gappa/gappa.dev/opam @@ -42,3 +42,7 @@ synopsis: "Tool intended for formally proving properties on numerical programs d url { src: "git+https://gitlab.inria.fr/gappa/gappa.git/#master" } +extra-files: [ + "0001-Added-configure-for-c-11.patch" + "sha512=af8bb8a81f87af91e5f8b137e10a2b06e9ccff0f167a4065f19fcea091e57ee5c892a0e2a0d4cb34753955c416e0d66b8e0ef759a1b0b276b79c470b59997f73" +] diff --git a/released/packages/coq-compcert-32/coq-compcert-32.3.12/opam b/released/packages/coq-compcert-32/coq-compcert-32.3.12/opam index b6e620f104..aefffc4e4e 100644 --- a/released/packages/coq-compcert-32/coq-compcert-32.3.12/opam +++ b/released/packages/coq-compcert-32/coq-compcert-32.3.12/opam @@ -67,3 +67,7 @@ url { checksum: "sha512=fec9badf0051928cc876d8d06a82372973d0e853f345b38ce3ddb16bc0d932b5be88f8d1c270208444163742e9adcac22915bc1e6d495ec861b17474deb5f306" } +extra-files: [ + "0001-Fix-incomplete-checking-of-unsolved-holes-465.patch" + "sha512=0d291488fd205c87c3de9cc2152cc24b994515ce45e4e54ee540cfef1f43756aef6f3a71824d01c4325143ecbcccb8a34a65d5f3ee6377c0a8f3490ce2d50598" +] diff --git a/released/packages/coq-compcert-32/coq-compcert-32.3.8/opam b/released/packages/coq-compcert-32/coq-compcert-32.3.8/opam index 2647c36345..7ee3f193f2 100755 --- a/released/packages/coq-compcert-32/coq-compcert-32.3.8/opam +++ b/released/packages/coq-compcert-32/coq-compcert-32.3.8/opam @@ -61,3 +61,7 @@ url { src: "https://github.com/AbsInt/CompCert/archive/v3.8.tar.gz" checksum: "sha512=ba669eb2098eb80ba393404f45b814113cf9e1d9497b074f7158c8e3857fdfdf72a95c7b177b1342689cf802efd7e0004356a89bb010cbbf496fca8a4f9fbda7" } +extra-files: [ + "0001-Configure-the-correct-archiver-to-build-runtime-libc.patch" + "sha512=e4e0865341ff067b27e3bf896c4b3479fd1ba926f83597594ae620356e4a0b9da0e85b2ce8712814d61bfbb51de2ae02096f024e9330a1a0ce33de005d3c739c" +] diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform/opam index 86c8d77033..07a20be9e7 100755 --- a/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform/opam +++ b/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "amd64-linux" {os = "linux"} @@ -30,15 +29,42 @@ patches: [ "0009-Don-t-build-MenhirLib-platform-version-is-used.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=62e36964ed3d06a213caea8639be51641c25df3c4ea384e01ce57d015de698d3"] - ["0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=1af58e827aa24be60e115878b9f70f1bf715f83bb1b91da8e2a9d749f4195d29"] - ["0003-Update-the-list-of-dual-licensed-files.patch" "sha256=bf91c7d3e2177620296838658cafbeffdd50d8d1ef56649b56a35644410e1337"] - ["0004-Use-Coq-platform-supplied-Flocq.patch" "sha256=83261a1fae459c319c0288a543787d3abcadaa2cccb1c34543c9784fe645f942"] - ["0005-Import-ListNotations-explicitly.patch" "sha256=c4f29203e8dcaa17c76543ad77dabefdb555588567d4f6055cd53e19a9c81081"] - ["0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" "sha256=3b7f59d4736d36878bbe3c0fed80e7db1ae75b9c8a5a9c90a57df2c1a4f4ae78"] - ["0007-Use-ocamlfind-to-find-menhirLib.patch" "sha256=df3f103977fa02bd339f6a8537da6bd4eaf1baa54c9675508e3bd16dbe11464e"] - ["0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=bcd2eb6eafb5a71fd0ee8ecf6f1b100b06723c636adb0ef2f915fa0ac3585c64"] - ["0009-Don-t-build-MenhirLib-platform-version-is-used.patch" "sha256=77835a85124eb1e8afefdcaf9eaa5beab64ed0fea22fceab78b7fd550778c857"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=cd0a6101b3ab9092fb611f57d2b55d3d4b5b98fdea5c8cbab8bde55f0a5ff3f988accf0a2c019fdebbffc232c9dee3474f1a3db95b1741bd380f935cf24ad786" +] + [ + "0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=eb7d92f6cec51f6a1a5936e70594967577f95bd71e411aee5e88d2097fe91838083aed312800b35f17aec6c5b538df6d363d64a80df37e71d3969851898ea779" +] + [ + "0003-Update-the-list-of-dual-licensed-files.patch" + "sha512=a5a43833cfe0783d8ce129110d63ddca893efeb72e923614422ab3402227ec74f824f35adbc86482b87624173adc82e0043f4dcb05be3492d0910a94620eaf9f" +] + [ + "0004-Use-Coq-platform-supplied-Flocq.patch" + "sha512=c6f2f759789721bcb3a7111be293f455a7dc7b6542cd8bebce13e637a6328b0f659fef0daa4a6723ecb94b9119874dbec37a99add46b7a8071b10fcd72494669" +] + [ + "0005-Import-ListNotations-explicitly.patch" + "sha512=b1ff8c85b7707a6c37f573ba7d4bc936ffb28e9807b03207bfdf44770fdfdd37bfc3973bfbbb12c88aca33a0c593d6247ccfb1ba4f34e4f7c0dfc2f93ae1db74" +] + [ + "0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" + "sha512=f7aa69f6f81778247c5f3e01a44b9341b11950d7a555b7c6a680b686ad095931c1a000eb4479ba37841e0b13a7109302168b62a9dc97b4780739b2ff2bfd3569" +] + [ + "0007-Use-ocamlfind-to-find-menhirLib.patch" + "sha512=fd4f3bbc96c195172ea86ffc495a6388d07b4009e3bf9c923d3c4bc37814eea58f67bbd301a93df2dbeae282e86a62d043ff60bb109c0ced16386e05827cfb9f" +] + [ + "0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=0200eaee2f577fd7b79cdac07a7c80903e718fe55de3cf9acb97718f36357d0e1a5b695364e3f892cbd94ddf0b903fdb17754dbe7aaaed45f7e15d60e1b6fcb7" +] + [ + "0009-Don-t-build-MenhirLib-platform-version-is-used.patch" + "sha512=f7aeb089b1325d41912b84dff130ee44f0d6d28618ac4345867a3c6081033108949e8c51707c5f71cefafdfb5433597216197917c6c6348394c04431d1218b56" +] ] install: [ [make "install"] diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform~open_source/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform~open_source/opam index b7ea546cf9..2ad9dbc1f6 100755 --- a/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform~open_source/opam +++ b/released/packages/coq-compcert-64/coq-compcert-64.3.7+8.12~coq_platform~open_source/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "amd64-linux" {os = "linux"} @@ -32,16 +31,46 @@ patches: [ "0010-Added-open-source-build-to-makefile.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=62e36964ed3d06a213caea8639be51641c25df3c4ea384e01ce57d015de698d3"] - ["0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=1af58e827aa24be60e115878b9f70f1bf715f83bb1b91da8e2a9d749f4195d29"] - ["0003-Update-the-list-of-dual-licensed-files.patch" "sha256=bf91c7d3e2177620296838658cafbeffdd50d8d1ef56649b56a35644410e1337"] - ["0004-Use-Coq-platform-supplied-Flocq.patch" "sha256=83261a1fae459c319c0288a543787d3abcadaa2cccb1c34543c9784fe645f942"] - ["0005-Import-ListNotations-explicitly.patch" "sha256=c4f29203e8dcaa17c76543ad77dabefdb555588567d4f6055cd53e19a9c81081"] - ["0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" "sha256=3b7f59d4736d36878bbe3c0fed80e7db1ae75b9c8a5a9c90a57df2c1a4f4ae78"] - ["0007-Use-ocamlfind-to-find-menhirLib.patch" "sha256=df3f103977fa02bd339f6a8537da6bd4eaf1baa54c9675508e3bd16dbe11464e"] - ["0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=bcd2eb6eafb5a71fd0ee8ecf6f1b100b06723c636adb0ef2f915fa0ac3585c64"] - ["0009-Don-t-build-MenhirLib-platform-version-is-used.patch" "sha256=77835a85124eb1e8afefdcaf9eaa5beab64ed0fea22fceab78b7fd550778c857"] - ["0010-Added-open-source-build-to-makefile.patch" "sha256=0c30ba166c0687395eef15aa92dee66b02d46ee12417de74a69fc3b479ea3e4c"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=cd0a6101b3ab9092fb611f57d2b55d3d4b5b98fdea5c8cbab8bde55f0a5ff3f988accf0a2c019fdebbffc232c9dee3474f1a3db95b1741bd380f935cf24ad786" +] + [ + "0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=eb7d92f6cec51f6a1a5936e70594967577f95bd71e411aee5e88d2097fe91838083aed312800b35f17aec6c5b538df6d363d64a80df37e71d3969851898ea779" +] + [ + "0003-Update-the-list-of-dual-licensed-files.patch" + "sha512=a5a43833cfe0783d8ce129110d63ddca893efeb72e923614422ab3402227ec74f824f35adbc86482b87624173adc82e0043f4dcb05be3492d0910a94620eaf9f" +] + [ + "0004-Use-Coq-platform-supplied-Flocq.patch" + "sha512=c6f2f759789721bcb3a7111be293f455a7dc7b6542cd8bebce13e637a6328b0f659fef0daa4a6723ecb94b9119874dbec37a99add46b7a8071b10fcd72494669" +] + [ + "0005-Import-ListNotations-explicitly.patch" + "sha512=b1ff8c85b7707a6c37f573ba7d4bc936ffb28e9807b03207bfdf44770fdfdd37bfc3973bfbbb12c88aca33a0c593d6247ccfb1ba4f34e4f7c0dfc2f93ae1db74" +] + [ + "0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" + "sha512=f7aa69f6f81778247c5f3e01a44b9341b11950d7a555b7c6a680b686ad095931c1a000eb4479ba37841e0b13a7109302168b62a9dc97b4780739b2ff2bfd3569" +] + [ + "0007-Use-ocamlfind-to-find-menhirLib.patch" + "sha512=fd4f3bbc96c195172ea86ffc495a6388d07b4009e3bf9c923d3c4bc37814eea58f67bbd301a93df2dbeae282e86a62d043ff60bb109c0ced16386e05827cfb9f" +] + [ + "0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=0200eaee2f577fd7b79cdac07a7c80903e718fe55de3cf9acb97718f36357d0e1a5b695364e3f892cbd94ddf0b903fdb17754dbe7aaaed45f7e15d60e1b6fcb7" +] + [ + "0009-Don-t-build-MenhirLib-platform-version-is-used.patch" + "sha512=f7aeb089b1325d41912b84dff130ee44f0d6d28618ac4345867a3c6081033108949e8c51707c5f71cefafdfb5433597216197917c6c6348394c04431d1218b56" +] + [ + "0010-Added-open-source-build-to-makefile.patch" + "sha512=fe7ca2df99c16667a289bd39a083f89c411828f5867fc8f70ff218e318da8e86508310d8053c62722dee8739baf1315136026d92763e47e8eca553c55da0b504" +] ] install: [ [make "install_open_source"] diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam index 243e3be02e..674fa708f6 100644 --- a/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam +++ b/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "amd64-linux" {os = "linux"} "amd64-macosx" {os = "macos"} @@ -25,11 +24,26 @@ patches: [ "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] - ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] - ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] - ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] - ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=d4c003f707eb4e2f7c7c006121b95353b74b4f6dbebe6e57fbdf0f5d8742f2fbb1f5ce572383462eea2f9e7b7895b390fb81b78186c2c7360fe0cf16ebd2e227" +] + [ + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=1aed05d792e3008af75439513dbdf950ad8ee12d6baca1392a8f3b7a535215593461f898db67b50fa4e9959380cc42ac5d7b51ff2bf0af411d85d86fa014c7e0" +] + [ + "0008-Update-the-list-of-dual-licensed-files.patch" + "sha512=1923357eedfec55c4b68e89b0504057fdc0df33c759fb63b2e33afefe888ee0a83578cec24b0d706009b3d5bcdc56511dfa494925fc5316182dcda83de0376d4" +] + [ + "0011-Use-Coq-platform-supplied-Flocq.patch" + "sha512=00da51808dca14385c8e4ffadf6d233f9bb1955c153b7a0dfb877342bffaac5622f7e3fa1255fc2e960327fda2bd6ed6154a0132c75b1bfaff928e9eaabca22a" +] + [ + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=59fe6ac6cd70809b3e7772872e729d11677e8f2c19294f1386541f9b9105863a5738dc648fd71df717cf023afcc685c3b33da7a6f476498c3f45b0a43ba526f5" +] ] install: [ [make "install"] diff --git a/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam b/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam index 150e76e63a..610807fc59 100644 --- a/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam +++ b/released/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "amd64-linux" {os = "linux"} "amd64-macosx" {os = "macos"} @@ -27,12 +26,30 @@ patches: [ "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] - ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] - ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] - ["0010-Added-open-source-build-to-makefile.patch" "sha256=fc3b8c1e097b53f209e7cf2e9b2e822609e8370857dbf1a4b34d909c37dcdfb5"] - ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] - ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=d4c003f707eb4e2f7c7c006121b95353b74b4f6dbebe6e57fbdf0f5d8742f2fbb1f5ce572383462eea2f9e7b7895b390fb81b78186c2c7360fe0cf16ebd2e227" +] + [ + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=1aed05d792e3008af75439513dbdf950ad8ee12d6baca1392a8f3b7a535215593461f898db67b50fa4e9959380cc42ac5d7b51ff2bf0af411d85d86fa014c7e0" +] + [ + "0008-Update-the-list-of-dual-licensed-files.patch" + "sha512=1923357eedfec55c4b68e89b0504057fdc0df33c759fb63b2e33afefe888ee0a83578cec24b0d706009b3d5bcdc56511dfa494925fc5316182dcda83de0376d4" +] + [ + "0010-Added-open-source-build-to-makefile.patch" + "sha512=ecb589c5e927dfdbeffb16d2d86a32323e0e51792fbd0be0b341a401d5c7312d58f3d1687612d8915fa68d79734519bac754f67db188adaac3b8beee5e10ab77" +] + [ + "0011-Use-Coq-platform-supplied-Flocq.patch" + "sha512=00da51808dca14385c8e4ffadf6d233f9bb1955c153b7a0dfb877342bffaac5622f7e3fa1255fc2e960327fda2bd6ed6154a0132c75b1bfaff928e9eaabca22a" +] + [ + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=59fe6ac6cd70809b3e7772872e729d11677e8f2c19294f1386541f9b9105863a5738dc648fd71df717cf023afcc685c3b33da7a6f476498c3f45b0a43ba526f5" +] ] install: [ [make "install_open_source"] diff --git a/released/packages/coq-compcert/coq-compcert.2.0.0/opam b/released/packages/coq-compcert/coq-compcert.2.0.0/opam index 077878c306..27703a696b 100644 --- a/released/packages/coq-compcert/coq-compcert.2.0.0/opam +++ b/released/packages/coq-compcert/coq-compcert.2.0.0/opam @@ -14,7 +14,7 @@ depends: [ ] synopsis: "The CompCert C compiler" authors: "Xavier Leroy " -extra-files: ["coq-compcert.install" "md5=a7efe759bff32c6aac2c2ca483d5a266"] +extra-files: ["coq-compcert.install" "sha512=97a334931f3c7df124513edd8f53a935ada63247ffd7e3a3048652a9bd696db783e3e3ef568069b9c14b0a0b1bcfa533a2d88fb5b4a37f371d22b7e143e4fe61"] url { src: "http://compcert.inria.fr/release/compcert-2.0.tgz" checksum: "md5=931325ad6a1faf22df73c249509c0b9f" diff --git a/released/packages/coq-compcert/coq-compcert.2.3.2/opam b/released/packages/coq-compcert/coq-compcert.2.3.2/opam index f2e9ed00d6..430b806aeb 100644 --- a/released/packages/coq-compcert/coq-compcert.2.3.2/opam +++ b/released/packages/coq-compcert/coq-compcert.2.3.2/opam @@ -15,7 +15,7 @@ depends: [ ] synopsis: "The CompCert C compiler" authors: "Xavier Leroy " -extra-files: ["coq-compcert.install" "md5=a7efe759bff32c6aac2c2ca483d5a266"] +extra-files: ["coq-compcert.install" "sha512=97a334931f3c7df124513edd8f53a935ada63247ffd7e3a3048652a9bd696db783e3e3ef568069b9c14b0a0b1bcfa533a2d88fb5b4a37f371d22b7e143e4fe61"] url { src: "http://compcert.inria.fr/release/compcert-2.3pl2.tgz" checksum: "md5=f97700e91163e6fbdb645721e2c1350f" diff --git a/released/packages/coq-compcert/coq-compcert.2.4.0/opam b/released/packages/coq-compcert/coq-compcert.2.4.0/opam index 34f0d3ea2c..c1fc75732d 100644 --- a/released/packages/coq-compcert/coq-compcert.2.4.0/opam +++ b/released/packages/coq-compcert/coq-compcert.2.4.0/opam @@ -15,7 +15,7 @@ depends: [ ] synopsis: "The CompCert C compiler" authors: "Xavier Leroy " -extra-files: ["coq-compcert.install" "md5=a7efe759bff32c6aac2c2ca483d5a266"] +extra-files: ["coq-compcert.install" "sha512=97a334931f3c7df124513edd8f53a935ada63247ffd7e3a3048652a9bd696db783e3e3ef568069b9c14b0a0b1bcfa533a2d88fb5b4a37f371d22b7e143e4fe61"] url { src: "http://compcert.inria.fr/release/compcert-2.4.tgz" checksum: "md5=26f0f55316be9e8d65568d05e8dcb89f" diff --git a/released/packages/coq-compcert/coq-compcert.2.7.1/opam b/released/packages/coq-compcert/coq-compcert.2.7.1/opam index c5f935bea3..e1a0cd48c5 100644 --- a/released/packages/coq-compcert/coq-compcert.2.7.1/opam +++ b/released/packages/coq-compcert/coq-compcert.2.7.1/opam @@ -29,7 +29,7 @@ depends: [ patches: "fix-coq-version.patch" synopsis: "The CompCert C compiler" authors: "Xavier Leroy " -extra-files: ["fix-coq-version.patch" "md5=00fcc55512084b421a97922fb1eb4422"] +extra-files: ["fix-coq-version.patch" "sha512=d915cd1e1a05af14b8d8bc390bae929a5ef0694598afc4bada4bc384eec64616fc38af1a758753bc025ec2e848129ea5638b81d51b08e8219618bf05a675dc87"] url { src: "https://github.com/AbsInt/CompCert/archive/v2.7.1.tar.gz" checksum: "md5=e1a36bad26870384912de4b4e9eb43b0" diff --git a/released/packages/coq-compcert/coq-compcert.3.12/opam b/released/packages/coq-compcert/coq-compcert.3.12/opam index 0a7d9505ec..16e9f172d0 100644 --- a/released/packages/coq-compcert/coq-compcert.3.12/opam +++ b/released/packages/coq-compcert/coq-compcert.3.12/opam @@ -56,3 +56,7 @@ url { checksum: "sha512=fec9badf0051928cc876d8d06a82372973d0e853f345b38ce3ddb16bc0d932b5be88f8d1c270208444163742e9adcac22915bc1e6d495ec861b17474deb5f306" } +extra-files: [ + "0001-Fix-incomplete-checking-of-unsolved-holes-465.patch" + "sha512=0d291488fd205c87c3de9cc2152cc24b994515ce45e4e54ee540cfef1f43756aef6f3a71824d01c4325143ecbcccb8a34a65d5f3ee6377c0a8f3490ce2d50598" +] diff --git a/released/packages/coq-compcert/coq-compcert.3.6+8.11/opam b/released/packages/coq-compcert/coq-compcert.3.6+8.11/opam index 14061d25c2..38d2727a12 100644 --- a/released/packages/coq-compcert/coq-compcert.3.6+8.11/opam +++ b/released/packages/coq-compcert/coq-compcert.3.6+8.11/opam @@ -18,7 +18,7 @@ build: [ [make "-j%{jobs}%" {ocaml:version >= "4.06"}] ] patches: "compat-8-11.patch" -extra-files: ["compat-8-11.patch" "sha256=1d54e39e9cda9ce8a408158580c09d0d76ff2accbd7524d1986aee4a7b0563dd"] +extra-files: ["compat-8-11.patch" "sha512=b16ed5b72266b0e5319deee5aa6c61b1c883e8f32469e088905301eb9474e130c2d79c2134328bb9a6ac7ce8c95c15a40d0f72cfbda18d0b44f9eebf76225964"] install: [ [make "install"] ["install" "-m" "0644" "VERSION" "%{lib}%/coq/user-contrib/compcert/"] diff --git a/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform/opam b/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform/opam index a0909bebf0..0b0feae1fc 100755 --- a/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "ia32-linux" {os = "linux"} @@ -32,15 +31,42 @@ patches: [ "0009-Don-t-build-MenhirLib-platform-version-is-used.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=62e36964ed3d06a213caea8639be51641c25df3c4ea384e01ce57d015de698d3"] - ["0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=1af58e827aa24be60e115878b9f70f1bf715f83bb1b91da8e2a9d749f4195d29"] - ["0003-Update-the-list-of-dual-licensed-files.patch" "sha256=bf91c7d3e2177620296838658cafbeffdd50d8d1ef56649b56a35644410e1337"] - ["0004-Use-Coq-platform-supplied-Flocq.patch" "sha256=83261a1fae459c319c0288a543787d3abcadaa2cccb1c34543c9784fe645f942"] - ["0005-Import-ListNotations-explicitly.patch" "sha256=c4f29203e8dcaa17c76543ad77dabefdb555588567d4f6055cd53e19a9c81081"] - ["0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" "sha256=3b7f59d4736d36878bbe3c0fed80e7db1ae75b9c8a5a9c90a57df2c1a4f4ae78"] - ["0007-Use-ocamlfind-to-find-menhirLib.patch" "sha256=df3f103977fa02bd339f6a8537da6bd4eaf1baa54c9675508e3bd16dbe11464e"] - ["0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=bcd2eb6eafb5a71fd0ee8ecf6f1b100b06723c636adb0ef2f915fa0ac3585c64"] - ["0009-Don-t-build-MenhirLib-platform-version-is-used.patch" "sha256=77835a85124eb1e8afefdcaf9eaa5beab64ed0fea22fceab78b7fd550778c857"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=cd0a6101b3ab9092fb611f57d2b55d3d4b5b98fdea5c8cbab8bde55f0a5ff3f988accf0a2c019fdebbffc232c9dee3474f1a3db95b1741bd380f935cf24ad786" +] + [ + "0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=eb7d92f6cec51f6a1a5936e70594967577f95bd71e411aee5e88d2097fe91838083aed312800b35f17aec6c5b538df6d363d64a80df37e71d3969851898ea779" +] + [ + "0003-Update-the-list-of-dual-licensed-files.patch" + "sha512=a5a43833cfe0783d8ce129110d63ddca893efeb72e923614422ab3402227ec74f824f35adbc86482b87624173adc82e0043f4dcb05be3492d0910a94620eaf9f" +] + [ + "0004-Use-Coq-platform-supplied-Flocq.patch" + "sha512=c6f2f759789721bcb3a7111be293f455a7dc7b6542cd8bebce13e637a6328b0f659fef0daa4a6723ecb94b9119874dbec37a99add46b7a8071b10fcd72494669" +] + [ + "0005-Import-ListNotations-explicitly.patch" + "sha512=b1ff8c85b7707a6c37f573ba7d4bc936ffb28e9807b03207bfdf44770fdfdd37bfc3973bfbbb12c88aca33a0c593d6247ccfb1ba4f34e4f7c0dfc2f93ae1db74" +] + [ + "0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" + "sha512=f7aa69f6f81778247c5f3e01a44b9341b11950d7a555b7c6a680b686ad095931c1a000eb4479ba37841e0b13a7109302168b62a9dc97b4780739b2ff2bfd3569" +] + [ + "0007-Use-ocamlfind-to-find-menhirLib.patch" + "sha512=fd4f3bbc96c195172ea86ffc495a6388d07b4009e3bf9c923d3c4bc37814eea58f67bbd301a93df2dbeae282e86a62d043ff60bb109c0ced16386e05827cfb9f" +] + [ + "0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=0200eaee2f577fd7b79cdac07a7c80903e718fe55de3cf9acb97718f36357d0e1a5b695364e3f892cbd94ddf0b903fdb17754dbe7aaaed45f7e15d60e1b6fcb7" +] + [ + "0009-Don-t-build-MenhirLib-platform-version-is-used.patch" + "sha512=f7aeb089b1325d41912b84dff130ee44f0d6d28618ac4345867a3c6081033108949e8c51707c5f71cefafdfb5433597216197917c6c6348394c04431d1218b56" +] ] install: [ [make "install"] diff --git a/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform~open_source/opam b/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform~open_source/opam index c6b6fa1c4e..369c7a1e9f 100755 --- a/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform~open_source/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7+8.12~coq_platform~open_source/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "ia32-linux" {os = "linux"} @@ -34,16 +33,46 @@ patches: [ "0010-Added-open-source-build-to-makefile.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=62e36964ed3d06a213caea8639be51641c25df3c4ea384e01ce57d015de698d3"] - ["0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=1af58e827aa24be60e115878b9f70f1bf715f83bb1b91da8e2a9d749f4195d29"] - ["0003-Update-the-list-of-dual-licensed-files.patch" "sha256=bf91c7d3e2177620296838658cafbeffdd50d8d1ef56649b56a35644410e1337"] - ["0004-Use-Coq-platform-supplied-Flocq.patch" "sha256=83261a1fae459c319c0288a543787d3abcadaa2cccb1c34543c9784fe645f942"] - ["0005-Import-ListNotations-explicitly.patch" "sha256=c4f29203e8dcaa17c76543ad77dabefdb555588567d4f6055cd53e19a9c81081"] - ["0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" "sha256=3b7f59d4736d36878bbe3c0fed80e7db1ae75b9c8a5a9c90a57df2c1a4f4ae78"] - ["0007-Use-ocamlfind-to-find-menhirLib.patch" "sha256=df3f103977fa02bd339f6a8537da6bd4eaf1baa54c9675508e3bd16dbe11464e"] - ["0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=bcd2eb6eafb5a71fd0ee8ecf6f1b100b06723c636adb0ef2f915fa0ac3585c64"] - ["0009-Don-t-build-MenhirLib-platform-version-is-used.patch" "sha256=77835a85124eb1e8afefdcaf9eaa5beab64ed0fea22fceab78b7fd550778c857"] - ["0010-Added-open-source-build-to-makefile.patch" "sha256=0c30ba166c0687395eef15aa92dee66b02d46ee12417de74a69fc3b479ea3e4c"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=cd0a6101b3ab9092fb611f57d2b55d3d4b5b98fdea5c8cbab8bde55f0a5ff3f988accf0a2c019fdebbffc232c9dee3474f1a3db95b1741bd380f935cf24ad786" +] + [ + "0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=eb7d92f6cec51f6a1a5936e70594967577f95bd71e411aee5e88d2097fe91838083aed312800b35f17aec6c5b538df6d363d64a80df37e71d3969851898ea779" +] + [ + "0003-Update-the-list-of-dual-licensed-files.patch" + "sha512=a5a43833cfe0783d8ce129110d63ddca893efeb72e923614422ab3402227ec74f824f35adbc86482b87624173adc82e0043f4dcb05be3492d0910a94620eaf9f" +] + [ + "0004-Use-Coq-platform-supplied-Flocq.patch" + "sha512=c6f2f759789721bcb3a7111be293f455a7dc7b6542cd8bebce13e637a6328b0f659fef0daa4a6723ecb94b9119874dbec37a99add46b7a8071b10fcd72494669" +] + [ + "0005-Import-ListNotations-explicitly.patch" + "sha512=b1ff8c85b7707a6c37f573ba7d4bc936ffb28e9807b03207bfdf44770fdfdd37bfc3973bfbbb12c88aca33a0c593d6247ccfb1ba4f34e4f7c0dfc2f93ae1db74" +] + [ + "0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch" + "sha512=f7aa69f6f81778247c5f3e01a44b9341b11950d7a555b7c6a680b686ad095931c1a000eb4479ba37841e0b13a7109302168b62a9dc97b4780739b2ff2bfd3569" +] + [ + "0007-Use-ocamlfind-to-find-menhirLib.patch" + "sha512=fd4f3bbc96c195172ea86ffc495a6388d07b4009e3bf9c923d3c4bc37814eea58f67bbd301a93df2dbeae282e86a62d043ff60bb109c0ced16386e05827cfb9f" +] + [ + "0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=0200eaee2f577fd7b79cdac07a7c80903e718fe55de3cf9acb97718f36357d0e1a5b695364e3f892cbd94ddf0b903fdb17754dbe7aaaed45f7e15d60e1b6fcb7" +] + [ + "0009-Don-t-build-MenhirLib-platform-version-is-used.patch" + "sha512=f7aeb089b1325d41912b84dff130ee44f0d6d28618ac4345867a3c6081033108949e8c51707c5f71cefafdfb5433597216197917c6c6348394c04431d1218b56" +] + [ + "0010-Added-open-source-build-to-makefile.patch" + "sha512=fe7ca2df99c16667a289bd39a083f89c411828f5867fc8f70ff218e318da8e86508310d8053c62722dee8739baf1315136026d92763e47e8eca553c55da0b504" +] ] install: [ [make "install_open_source"] diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam index 9f5a2a91a9..f3c5446c1b 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "ia32-linux" {os = "linux"} "ia32-macosx" {os = "macos"} @@ -26,11 +25,26 @@ patches: [ "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] - ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] - ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] - ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] - ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=d4c003f707eb4e2f7c7c006121b95353b74b4f6dbebe6e57fbdf0f5d8742f2fbb1f5ce572383462eea2f9e7b7895b390fb81b78186c2c7360fe0cf16ebd2e227" +] + [ + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=1aed05d792e3008af75439513dbdf950ad8ee12d6baca1392a8f3b7a535215593461f898db67b50fa4e9959380cc42ac5d7b51ff2bf0af411d85d86fa014c7e0" +] + [ + "0008-Update-the-list-of-dual-licensed-files.patch" + "sha512=1923357eedfec55c4b68e89b0504057fdc0df33c759fb63b2e33afefe888ee0a83578cec24b0d706009b3d5bcdc56511dfa494925fc5316182dcda83de0376d4" +] + [ + "0011-Use-Coq-platform-supplied-Flocq.patch" + "sha512=00da51808dca14385c8e4ffadf6d233f9bb1955c153b7a0dfb877342bffaac5622f7e3fa1255fc2e960327fda2bd6ed6154a0132c75b1bfaff928e9eaabca22a" +] + [ + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=59fe6ac6cd70809b3e7772872e729d11677e8f2c19294f1386541f9b9105863a5738dc648fd71df717cf023afcc685c3b33da7a6f476498c3f45b0a43ba526f5" +] ] install: [ [make "install"] diff --git a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam index 16fcc2b0ae..6f5c331e75 100644 --- a/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam +++ b/released/packages/coq-compcert/coq-compcert.3.7~coq-platform~open-source/opam @@ -5,7 +5,6 @@ homepage: "http://compcert.inria.fr/" dev-repo: "git+https://github.com/AbsInt/CompCert.git" bug-reports: "https://github.com/AbsInt/CompCert/issues" license: "INRIA Non-Commercial License Agreement" -version: "3.7" build: [ ["./configure" "ia32-linux" {os = "linux"} "ia32-macosx" {os = "macos"} @@ -28,12 +27,30 @@ patches: [ "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" ] extra-files: [ - ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"] - ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"] - ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"] - ["0010-Added-open-source-build-to-makefile.patch" "sha256=fc3b8c1e097b53f209e7cf2e9b2e822609e8370857dbf1a4b34d909c37dcdfb5"] - ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"] - ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"] + [ + "0001-Install-compcert.config-file-along-the-Coq-developme.patch" + "sha512=d4c003f707eb4e2f7c7c006121b95353b74b4f6dbebe6e57fbdf0f5d8742f2fbb1f5ce572383462eea2f9e7b7895b390fb81b78186c2c7360fe0cf16ebd2e227" +] + [ + "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" + "sha512=1aed05d792e3008af75439513dbdf950ad8ee12d6baca1392a8f3b7a535215593461f898db67b50fa4e9959380cc42ac5d7b51ff2bf0af411d85d86fa014c7e0" +] + [ + "0008-Update-the-list-of-dual-licensed-files.patch" + "sha512=1923357eedfec55c4b68e89b0504057fdc0df33c759fb63b2e33afefe888ee0a83578cec24b0d706009b3d5bcdc56511dfa494925fc5316182dcda83de0376d4" +] + [ + "0010-Added-open-source-build-to-makefile.patch" + "sha512=ecb589c5e927dfdbeffb16d2d86a32323e0e51792fbd0be0b341a401d5c7312d58f3d1687612d8915fa68d79734519bac754f67db188adaac3b8beee5e10ab77" +] + [ + "0011-Use-Coq-platform-supplied-Flocq.patch" + "sha512=00da51808dca14385c8e4ffadf6d233f9bb1955c153b7a0dfb877342bffaac5622f7e3fa1255fc2e960327fda2bd6ed6154a0132c75b1bfaff928e9eaabca22a" +] + [ + "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" + "sha512=59fe6ac6cd70809b3e7772872e729d11677e8f2c19294f1386541f9b9105863a5738dc648fd71df717cf023afcc685c3b33da7a6f476498c3f45b0a43ba526f5" +] ] install: [ [make "install_open_source"] diff --git a/released/packages/coq-compcert/coq-compcert.3.8/opam b/released/packages/coq-compcert/coq-compcert.3.8/opam index d645e31dd2..179d8524c6 100755 --- a/released/packages/coq-compcert/coq-compcert.3.8/opam +++ b/released/packages/coq-compcert/coq-compcert.3.8/opam @@ -48,3 +48,7 @@ url { src: "https://github.com/AbsInt/CompCert/archive/v3.8.tar.gz" checksum: "sha512=ba669eb2098eb80ba393404f45b814113cf9e1d9497b074f7158c8e3857fdfdf72a95c7b177b1342689cf802efd7e0004356a89bb010cbbf496fca8a4f9fbda7" } +extra-files: [ + "0001-Configure-the-correct-archiver-to-build-runtime-libc.patch" + "sha512=e4e0865341ff067b27e3bf896c4b3479fd1ba926f83597594ae620356e4a0b9da0e85b2ce8712814d61bfbb51de2ae02096f024e9330a1a0ce33de005d3c739c" +] diff --git a/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.0.0/opam b/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.0.0/opam index 23a5a1dd25..006f37e205 100644 --- a/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.0.0/opam +++ b/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.0.0/opam @@ -30,7 +30,7 @@ tags: [ ] synopsis: "A web server written in Coq" extra-files: [ - "coq-concurrency-pluto.install" "md5=c191e439136807d785f0d582e0b8783e" + "coq-concurrency-pluto.install" "sha512=df2cd4dd5cdc892a66ebfb07aceae6f4d5921ca5a1ad7fbaad5de8b24313c67e13aa842095d9959d2b0eb7ce71b7d6122ad6ee638b723d2bb4e66627bf6851aa" ] url { src: "https://github.com/coq-concurrency/pluto/archive/1.0.0.tar.gz" diff --git a/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.1.0/opam b/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.1.0/opam index 72ddfeefd0..f9f93c279f 100644 --- a/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.1.0/opam +++ b/released/packages/coq-concurrency-pluto/coq-concurrency-pluto.1.1.0/opam @@ -24,7 +24,7 @@ depends: [ ] synopsis: "A web server written in Coq" extra-files: [ - "coq-concurrency-pluto.install" "md5=c191e439136807d785f0d582e0b8783e" + "coq-concurrency-pluto.install" "sha512=df2cd4dd5cdc892a66ebfb07aceae6f4d5921ca5a1ad7fbaad5de8b24313c67e13aa842095d9959d2b0eb7ce71b7d6122ad6ee638b723d2bb4e66627bf6851aa" ] url { src: "https://github.com/coq-concurrency/pluto/archive/1.1.0.tar.gz" diff --git a/released/packages/coq-concurrency-proxy/coq-concurrency-proxy.1.0.0/opam b/released/packages/coq-concurrency-proxy/coq-concurrency-proxy.1.0.0/opam index a99cb754a4..9bdb195add 100644 --- a/released/packages/coq-concurrency-proxy/coq-concurrency-proxy.1.0.0/opam +++ b/released/packages/coq-concurrency-proxy/coq-concurrency-proxy.1.0.0/opam @@ -25,7 +25,7 @@ tags: [ ] synopsis: "A proxy to interface concurrent Coq programs with the operating system" extra-files: [ - "coq-concurrency-proxy.install" "md5=96f86b964fc4cd99c310011b83de5f61" + "coq-concurrency-proxy.install" "sha512=6dfeebf230cd1a02c6f9b7cf0a98389ec66f66d010fd1a755e5c4860e6fcfe5e3039a9f399fcb07031b5e6c672fd7beb2eaa091891fce8c25e28c3439b108f3f" ] url { src: "https://github.com/coq-concurrency/proxy/archive/1.0.0.tar.gz" diff --git a/released/packages/coq-coquelicot/coq-coquelicot.3.1.0/opam b/released/packages/coq-coquelicot/coq-coquelicot.3.1.0/opam index 648f472fd9..906c890179 100644 --- a/released/packages/coq-coquelicot/coq-coquelicot.3.1.0/opam +++ b/released/packages/coq-coquelicot/coq-coquelicot.3.1.0/opam @@ -38,3 +38,7 @@ url { src: "https://coquelicot.gitlabpages.inria.fr/releases/coquelicot-3.1.0.tar.gz" checksum: "sha512=f9aa6279250d3bf47255273d7af96d1d1845bc531426e4ce8de7ede183975cfd894d88baaa13af6cd056656ad434add4d9fd2e5f9b4d59f6887cc235ec6f0a5b" } +extra-files: [ + "remake.patch" + "sha512=4151a6a8fb2f96b217f7ad678d96b2be42521682bbfafe4ab8f9a01cd1983b1ff3ea8bd6d2c4ee9c003e172ca586bb7a279fbbfe6fec8b0349fcb9897d13a5d5" +] diff --git a/released/packages/coq-flocq/coq-flocq.3.3.1/opam b/released/packages/coq-flocq/coq-flocq.3.3.1/opam index daa804a37d..8a8a78d461 100644 --- a/released/packages/coq-flocq/coq-flocq.3.3.1/opam +++ b/released/packages/coq-flocq/coq-flocq.3.3.1/opam @@ -29,3 +29,7 @@ url { src: "https://flocq.gitlabpages.inria.fr/releases/flocq-3.3.1.tar.gz" checksum: "sha512=4c8079df683d838ef61b3f16ecd2084751a4752c129620efe06dfa847be59257f0c0c342fca2ae510d87c085e857a4d32bac10af8be6f29a8c462df0ee72f557" } +extra-files: [ + "remake.patch" + "sha512=4151a6a8fb2f96b217f7ad678d96b2be42521682bbfafe4ab8f9a01cd1983b1ff3ea8bd6d2c4ee9c003e172ca586bb7a279fbbfe6fec8b0349fcb9897d13a5d5" +] diff --git a/released/packages/coq-gappa/coq-gappa.1.4.4/opam b/released/packages/coq-gappa/coq-gappa.1.4.4/opam index 809987c7c3..85dbb681a9 100644 --- a/released/packages/coq-gappa/coq-gappa.1.4.4/opam +++ b/released/packages/coq-gappa/coq-gappa.1.4.4/opam @@ -34,3 +34,7 @@ url { src: "https://gappa.gitlabpages.inria.fr/releases/gappalib-coq-1.4.4.tar.gz" checksum: "sha512=910cb7d8f084fc93a8e59c2792093f252f1c8e9f7b63aa408c03de41dced1ff64b4cf2c9ee9610729f7885bdf42dd68c85a9a844c63781ba9fe8cfdfc5192665" } +extra-files: [ + "remake.patch" + "sha512=4151a6a8fb2f96b217f7ad678d96b2be42521682bbfafe4ab8f9a01cd1983b1ff3ea8bd6d2c4ee9c003e172ca586bb7a279fbbfe6fec8b0349fcb9897d13a5d5" +] diff --git a/released/packages/coq-gappa/coq-gappa.1.4.5/opam b/released/packages/coq-gappa/coq-gappa.1.4.5/opam index 805437fb78..12a8a5a0b8 100644 --- a/released/packages/coq-gappa/coq-gappa.1.4.5/opam +++ b/released/packages/coq-gappa/coq-gappa.1.4.5/opam @@ -34,3 +34,7 @@ url { src: "https://gappa.gitlabpages.inria.fr/releases/gappalib-coq-1.4.5.tar.gz" checksum: "sha512=79232f0132bc888fac83c45751d1a030c7fefd4a00b3be41941baaf1b5b8057a17b7a635323b07ec0de6b1cfc502cc664a77ae7864ae5387a5cc2727831aaa61" } +extra-files: [ + "remake.patch" + "sha512=0107d6aa9a3e326741cacbbcff8569dd2ca05f31854d8705a5d6f102df8ae53dd29058cadf3b98a177fcf80861281ee04e9498c82f657016235a6291db0549a1" +] diff --git a/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.0/opam b/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.0/opam index 83fc95fd0c..39945669fa 100644 --- a/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.0/opam +++ b/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.0/opam @@ -32,7 +32,7 @@ tags: [ "keyword:geometry" "keyword:parallel postulates" "category:Mathematics/Geometry/General" "date:2018-06-13" ] -extra-files : [["Make.in" "md5=4012b8ca78abe89ced161b10c93efdc9"]] +extra-files : ["Make.in""sha512=dfd7bad5862c57f1a7d13da8f4304a1e8aedcd6d362b93970f46cf8f7d12d19ad99d7124c65d7ab32e9675b5b9a3c17b08988b1d4cd784ddb765e0b5d92b0710"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.0.tar.gz" checksum: "md5=4a4ad33b4cad9b815a9b5c6308524c63" diff --git a/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.1/opam b/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.1/opam index 3b5c20f36b..7c86cb7251 100644 --- a/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.1/opam +++ b/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.1/opam @@ -29,7 +29,7 @@ tags: [ "keyword:geometry" "keyword:parallel postulates" "category:Mathematics/Geometry/General" "date:2024-03-03" ] -extra-files : [[ "_CoqProject.in" "md5=4012b8ca78abe89ced161b10c93efdc9" ]] +extra-files : ["_CoqProject.in""sha512=dfd7bad5862c57f1a7d13da8f4304a1e8aedcd6d362b93970f46cf8f7d12d19ad99d7124c65d7ab32e9675b5b9a3c17b08988b1d4cd784ddb765e0b5d92b0710"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz" checksum: "md5=14212f17e868a53ec0b6b84feda5c44d" diff --git a/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.0/opam b/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.0/opam index 424a1c9e4e..f0ef4b92fc 100644 --- a/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.0/opam +++ b/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.0/opam @@ -23,7 +23,7 @@ tags: [ "keyword:geometry" "keyword:Elements" "category:Mathematics/Geometry/General" "date:2018-06-13" ] -extra-files : [[ "Make.in" "md5=cac845bd85ad41adeeb32378cf505f1c" ]] +extra-files : ["Make.in""sha512=b338c6468b220f14c59a191c0e888e47c0f5648815e16f986ee86c92a12e400ec98a8b836d69912a311ee73ce867f26998459c39dbba903c2fe09b7a59d829fc"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.0.tar.gz" checksum: "md5=4a4ad33b4cad9b815a9b5c6308524c63" diff --git a/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.1/opam b/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.1/opam index e97d96fa21..b84b424b7e 100644 --- a/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.1/opam +++ b/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.1/opam @@ -23,7 +23,7 @@ tags: [ "keyword:geometry" "keyword:Elements" "category:Mathematics/Geometry/General" "date:2024-03-03" ] -extra-files : [[ "_CoqProject.in" "md5=cac845bd85ad41adeeb32378cf505f1c" ]] +extra-files : ["_CoqProject.in""sha512=b338c6468b220f14c59a191c0e888e47c0f5648815e16f986ee86c92a12e400ec98a8b836d69912a311ee73ce867f26998459c39dbba903c2fe09b7a59d829fc"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz" checksum: "md5=14212f17e868a53ec0b6b84feda5c44d" diff --git a/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.0/opam b/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.0/opam index 0cd19d02a0..e0898ec68f 100644 --- a/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.0/opam +++ b/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.0/opam @@ -36,7 +36,7 @@ tags: [ "keyword:geometry" "keyword:parallel postulates" "category:Mathematics/Geometry/General" "date:2018-06-13" ] -extra-files: [["Make.in" "md5=ee7f1852debd8d9621ebafa3c8b25dcc"]] +extra-files: ["Make.in""sha512=1f2926898f38b03f8fc233fbe226e30c94fd27693df82d16ba43ee6afb72600400705774572241d6d381aea56e242ed4b24dc81792287a353385fa9abdfe6c3a"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.0.tar.gz" checksum: "md5=4a4ad33b4cad9b815a9b5c6308524c63" diff --git a/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.1/opam b/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.1/opam index 7b4bc43438..e062bf44d0 100644 --- a/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.1/opam +++ b/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.1/opam @@ -36,7 +36,7 @@ tags: [ "keyword:geometry" "keyword:parallel postulates" "category:Mathematics/Geometry/General" "date:2024-03-03" ] -extra-files : [[ "_CoqProject.in" "md5=ee7f1852debd8d9621ebafa3c8b25dcc" ]] +extra-files : ["_CoqProject.in""sha512=1f2926898f38b03f8fc233fbe226e30c94fd27693df82d16ba43ee6afb72600400705774572241d6d381aea56e242ed4b24dc81792287a353385fa9abdfe6c3a"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz" checksum: "md5=14212f17e868a53ec0b6b84feda5c44d" diff --git a/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.0/opam b/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.0/opam index f29dfd43af..c83ad4316a 100644 --- a/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.0/opam +++ b/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.0/opam @@ -27,7 +27,7 @@ tags: [ "keyword:geometry" "keyword:Cartesian space" "category:Mathematics/Geometry/General" "date:2018-06-13" ] -extra-files: [["Make.in" "md5=5d3dc0a3321d9f0070c55129dc9df408"]] +extra-files: ["Make.in""sha512=ac0020cc76823e7e213d6a2cab7662b0e9eacdf3d4ec29db414f860d05acc1ddd9bddf8c423cf85009701d74b070a7503297d36b1202311272f2392f0954390f"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.0.tar.gz" checksum: "md5=4a4ad33b4cad9b815a9b5c6308524c63" diff --git a/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam b/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam index dfb0aeb0d4..174733c4d4 100644 --- a/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam +++ b/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam @@ -27,7 +27,7 @@ tags: [ "keyword:geometry" "keyword:Cartesian space" "category:Mathematics/Geometry/General" "date:2024-03-03" ] -extra-files : [[ "_CoqProject.in" "md5=5d3dc0a3321d9f0070c55129dc9df408" ]] +extra-files : ["_CoqProject.in""sha512=ac0020cc76823e7e213d6a2cab7662b0e9eacdf3d4ec29db414f860d05acc1ddd9bddf8c423cf85009701d74b070a7503297d36b1202311272f2392f0954390f"] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz" checksum: "md5=14212f17e868a53ec0b6b84feda5c44d" diff --git a/released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/opam b/released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/opam index ca911e0f8b..9082321ca5 100644 --- a/released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/opam +++ b/released/packages/coq-graph2tac/coq-graph2tac.1.0.anon/opam @@ -48,3 +48,13 @@ depends: [ substs: [ "Graph2TacConfig.v" ] +extra-files: [ + [ + "Graph2TacConfig.v.in" + "sha512=3033d42d7f51941aa9dd6f92c5608167f711941284aedba9b95442c1c980925b80e7bfd982c1eb28b6c69a361516043013d313da5316d3bb06152e252cfa73c4" + ] + [ + "injection-flags" + "sha512=b8154112fd12cedeabb4bcb9af126a9556d3043ef29b1eb8f95f011bd6c05e5de4f8fa47da91c9c2d30aa7337db8d975836bcc3226ba3247da4570423b6291e3" + ] +] diff --git a/released/packages/coq-interval/coq-interval.4.0.0/opam b/released/packages/coq-interval/coq-interval.4.0.0/opam index ba88d2c4a5..85e2810f14 100644 --- a/released/packages/coq-interval/coq-interval.4.0.0/opam +++ b/released/packages/coq-interval/coq-interval.4.0.0/opam @@ -39,3 +39,7 @@ url { src: "https://coqinterval.gitlabpages.inria.fr/releases/interval-4.0.0.tar.gz" checksum: "sha512=e8fc34e4b38565e9bb5b0ec9423d12d06c33c708235df97222fc6be9035cfdcba9b0b209b7123de4f9fca1b1ef7c6d7eb7f1383dca59795d8142ad737feb6597" } +extra-files: [ + "remake.patch" + "sha512=4151a6a8fb2f96b217f7ad678d96b2be42521682bbfafe4ab8f9a01cd1983b1ff3ea8bd6d2c4ee9c003e172ca586bb7a279fbbfe6fec8b0349fcb9897d13a5d5" +] diff --git a/released/packages/coq-interval/coq-interval.4.1.0/opam b/released/packages/coq-interval/coq-interval.4.1.0/opam index 42d0642950..824b9cdf43 100644 --- a/released/packages/coq-interval/coq-interval.4.1.0/opam +++ b/released/packages/coq-interval/coq-interval.4.1.0/opam @@ -44,3 +44,7 @@ url { src: "https://coqinterval.gitlabpages.inria.fr/releases/interval-4.1.0.tar.gz" checksum: "sha512=74f94e1d5a1f9b6562a84e5e3addced7bb2a36fd38b2ed6bcbbd0493ba9c4d470bbb2b5d07e3b322d9a5736bc18358966b4101e0ab9b0b18c2cab4efbb7b8c08" } +extra-files: [ + "remake.patch" + "sha512=0107d6aa9a3e326741cacbbcff8569dd2ca05f31854d8705a5d6f102df8ae53dd29058cadf3b98a177fcf80861281ee04e9498c82f657016235a6291db0549a1" +] diff --git a/released/packages/coq-io-hello-world/coq-io-hello-world.1.0.0/opam b/released/packages/coq-io-hello-world/coq-io-hello-world.1.0.0/opam index 049976b166..10be330cc5 100644 --- a/released/packages/coq-io-hello-world/coq-io-hello-world.1.0.0/opam +++ b/released/packages/coq-io-hello-world/coq-io-hello-world.1.0.0/opam @@ -22,7 +22,7 @@ tags: [ ] synopsis: "A Hello World program in Coq" extra-files: [ - "coq-io-hello-world.install" "md5=63d2dca2628eb17acf4b57b72d248663" + "coq-io-hello-world.install" "sha512=34c95260ce538f771395d5b04d83fcfa02898512d722ca463e6f105b2955581898b5d6d9bb6229c78e314374b4eef7d00d1c7aa403ab3d60fda05361849b29a9" ] url { src: "https://github.com/coq-io/hello-world/archive/1.0.0.tar.gz" diff --git a/released/packages/coq-io-hello-world/coq-io-hello-world.1.1.0/opam b/released/packages/coq-io-hello-world/coq-io-hello-world.1.1.0/opam index f2e1d73220..18f161fc21 100644 --- a/released/packages/coq-io-hello-world/coq-io-hello-world.1.1.0/opam +++ b/released/packages/coq-io-hello-world/coq-io-hello-world.1.1.0/opam @@ -22,7 +22,7 @@ tags: [ ] synopsis: "A Hello World program in Coq" extra-files: [ - "coq-io-hello-world.install" "md5=63d2dca2628eb17acf4b57b72d248663" + "coq-io-hello-world.install" "sha512=34c95260ce538f771395d5b04d83fcfa02898512d722ca463e6f105b2955581898b5d6d9bb6229c78e314374b4eef7d00d1c7aa403ab3d60fda05361849b29a9" ] url { src: "https://github.com/coq-io/hello-world/archive/1.1.0.tar.gz" diff --git a/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam b/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam index bf79d6646c..8066a700a7 100644 --- a/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam +++ b/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam @@ -66,4 +66,8 @@ url { src: "https://github.com/math-comp/analysis/archive/0.7.0.tar.gz" checksum: "sha512=d970066c54da0e2941f5aefd8c8d79c2c9c4fc08afc771993e72eeb50566f07812501a7e076f53aa2e33822c051b958c4c7b5fc55f3c67aa17e59b5576708645" } +extra-files: [ + "future-coercion-class-field.patch" + "sha512=e407ca51490acf9ef3c3d9a940f5d4f47825ed73ce17b4f7b525aaf8f79db73ec12054a1c65f52bacfb9532dc11f3ae62b1a4155bc0609f94309483e5a4dbc60" +] diff --git a/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam b/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam index eb52cfa082..42449eb9b6 100755 --- a/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam +++ b/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam @@ -54,3 +54,7 @@ url { src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.16.tar.gz" checksum: "sha512=abd34042fc2804954abc8b1fba4c2b3d1d1c0c780874ad0cbe698a19756e26985c77bb231b2e9b40ea01261f3fbbb36fbdd2b7095931e947bf933359cb0154f7" } +extra-files: [ + "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch" + "sha512=6b626b68ea3376ee3e532c8cbd024bd083be4b37e7fc933c4445c8fe7bc22022bc06a63b4f49e610381ee8a0218b0b42950ca417ca9404e84cbd16068191294e" +] diff --git a/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.0+8.16/opam b/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.0+8.16/opam index ea8f1510d0..1bbba57dbc 100644 --- a/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.0+8.16/opam +++ b/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.0+8.16/opam @@ -40,3 +40,7 @@ url { src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" } +extra-files: [ + "fix-build.patch" + "sha512=69fdb25bbfa75e3fb06cf7c0e53974ea1ae18a6105df87217a847fc56574b86dbece0a0005990ec78d5a41bddffa3b8d3d9a9f72a10c446f0b1ffb6e93afb7a7" +] diff --git a/released/packages/coq-mmaps/coq-mmaps.1.0/opam b/released/packages/coq-mmaps/coq-mmaps.1.0/opam index 668ecd4c8f..4e49ba5cf9 100644 --- a/released/packages/coq-mmaps/coq-mmaps.1.0/opam +++ b/released/packages/coq-mmaps/coq-mmaps.1.0/opam @@ -37,3 +37,7 @@ url { src: "https://github.com/coq-community/coq-mmaps/archive/v1.0.tar.gz" checksum: "sha512=4e98b43afea6732c53a5e9c2e410ec1ff186c32ba896292dbad0e7630397b836bed30e6f71c20a4c5664eee5edba5ea04aa017e62e5ddf004936ab403b157032" } +extra-files: [ + "locality-warnings.patch" + "sha512=91f24f4206f0ab5291574a38b7a8f8541e5afdb5d3730e32257544af2e22f9098ae095896e7c544db19c7c662c3b8466ef194d77b3059488b7b55f5335917e18" +] diff --git a/released/packages/coq-mmaps/coq-mmaps.1.1/opam b/released/packages/coq-mmaps/coq-mmaps.1.1/opam index 69d79b3979..445fc4038d 100644 --- a/released/packages/coq-mmaps/coq-mmaps.1.1/opam +++ b/released/packages/coq-mmaps/coq-mmaps.1.1/opam @@ -39,3 +39,7 @@ url { src: "https://github.com/coq-community/coq-mmaps/releases/download/v1.1/coq-mmaps-1.1.tar.gz" checksum: "sha512=55d2949391edf325e872a1ffa3fe55a4cef3120ee4b4d3498b510ffa22c877c4a40549b8d85e9adb1e06a002334c245608ff4d0a505035dc6710d46efe65b65f" } +extra-files: [ + "class-field-instance.patch" + "sha512=e2a31edebd40f3526acd8017dd3aafd623851ca200b4b1d4d29d7a99bddfcbee08fedddcf3120db7e97b29c3c02f8097f68af259d88a8f4df29c24ff98cbef64" +] diff --git a/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam b/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam index 3fd4729753..5893452b6f 100644 --- a/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam +++ b/released/packages/coq-mtac2/coq-mtac2.1.4+8.19/opam @@ -29,3 +29,7 @@ url { "sha512=4c5f17576bdfa6e127d5901666da640352ad472211bf21cf5ae67944e84ba9bf6306215cfcad83ca2117e29ec40429db8daf7421249e857537a08e827b3c4132" ] } +extra-files: [ + "declare-module.patch" + "sha512=1e719907f13bff785fc28bf1a1eb4e1179d71e2e9fb7831c2dd982808e39296af66b6e08b79a65325411aaf04638f6e6d46f9b7bce742b63ea9141db37e925e2" +] diff --git a/released/packages/coq-of-ocaml/coq-of-ocaml.1.1.1/opam b/released/packages/coq-of-ocaml/coq-of-ocaml.1.1.1/opam index 8cef81a387..ebdb60de06 100644 --- a/released/packages/coq-of-ocaml/coq-of-ocaml.1.1.1/opam +++ b/released/packages/coq-of-ocaml/coq-of-ocaml.1.1.1/opam @@ -25,7 +25,7 @@ tags: [ "keyword:OCaml" ] synopsis: "Compile OCaml to Coq" -extra-files: ["coq-of-ocaml.install" "md5=aaa1f52ec40bedefd2674f46a44cd578"] +extra-files: ["coq-of-ocaml.install" "sha512=55fb085980e7b09981d927fdd4c123e5e473de5888761e12e14ec9d1810eaad2ef599245e3ceaef22b0369c51f16533b0893ffdc7c1b54b4b91dd232bd4ba4db"] url { src: "https://github.com/clarus/coq-of-ocaml/archive/1.1.1.tar.gz" checksum: "md5=6148587be3cee4ec577e9909fabd45ce" diff --git a/released/packages/coq-of-ocaml/coq-of-ocaml.1.2.1/opam b/released/packages/coq-of-ocaml/coq-of-ocaml.1.2.1/opam index 4e5d66385f..8df1be76f8 100644 --- a/released/packages/coq-of-ocaml/coq-of-ocaml.1.2.1/opam +++ b/released/packages/coq-of-ocaml/coq-of-ocaml.1.2.1/opam @@ -25,7 +25,7 @@ tags: [ "keyword:OCaml" ] synopsis: "Compile OCaml to Coq" -extra-files: ["coq-of-ocaml.install" "md5=aaa1f52ec40bedefd2674f46a44cd578"] +extra-files: ["coq-of-ocaml.install" "sha512=55fb085980e7b09981d927fdd4c123e5e473de5888761e12e14ec9d1810eaad2ef599245e3ceaef22b0369c51f16533b0893ffdc7c1b54b4b91dd232bd4ba4db"] url { src: "https://github.com/clarus/coq-of-ocaml/archive/1.2.1.tar.gz" checksum: "md5=e8cb5565b8ce622d2afa5bcc59873ad2" diff --git a/released/packages/coq-of-ocaml/coq-of-ocaml.2.0.0/opam b/released/packages/coq-of-ocaml/coq-of-ocaml.2.0.0/opam index b0e0a863bd..eca567f3be 100644 --- a/released/packages/coq-of-ocaml/coq-of-ocaml.2.0.0/opam +++ b/released/packages/coq-of-ocaml/coq-of-ocaml.2.0.0/opam @@ -34,3 +34,7 @@ url { src: "https://github.com/clarus/coq-of-ocaml/archive/2.0.0.tar.gz" checksum: "sha512=bd18ac17e34dcf04d1d361ddbd230a943371976a46df4f0f0a51ac755643d1c1d8b1e69de6eb6d15f744fac8884f5e644b4f7d9bfc50e4ed13c51fde1863b17c" } +extra-files: [ + "coq-of-ocaml.install" + "sha512=05517cd59a014cf223dd7caa95210ad3835aa6d3b49c6f6a1ce5b8fe7c0daf1c85a0ffa332d6542315eec8dc9bc13da62b3b9b292809441b87646af80db80d53" +] diff --git a/released/packages/coq-of-ocaml/coq-of-ocaml.2.1.0/opam b/released/packages/coq-of-ocaml/coq-of-ocaml.2.1.0/opam index 0e41e551a2..f535d63a3b 100644 --- a/released/packages/coq-of-ocaml/coq-of-ocaml.2.1.0/opam +++ b/released/packages/coq-of-ocaml/coq-of-ocaml.2.1.0/opam @@ -34,3 +34,7 @@ url { src: "https://github.com/clarus/coq-of-ocaml/archive/2.1.0.tar.gz" checksum: "sha512=c90c2830c0cf749359a9e1381b8c3dbc0cfb98ca91e174f6d7f07fb031bff732a0e3abf4b3643418024249dbbd6e241859bbab4e75a66b0abab471d7734004c2" } +extra-files: [ + "coq-of-ocaml.install" + "sha512=05517cd59a014cf223dd7caa95210ad3835aa6d3b49c6f6a1ce5b8fe7c0daf1c85a0ffa332d6542315eec8dc9bc13da62b3b9b292809441b87646af80db80d53" +] diff --git a/released/packages/coq-ott/coq-ott.0.32/opam b/released/packages/coq-ott/coq-ott.0.32/opam index cce7889d28..097bed8174 100644 --- a/released/packages/coq-ott/coq-ott.0.32/opam +++ b/released/packages/coq-ott/coq-ott.0.32/opam @@ -39,3 +39,7 @@ url { src: "https://github.com/ott-lang/ott/archive/0.32.tar.gz" checksum: "sha512=f38e12c079426c5a460a9ab24e58f098410ceb5ae0284c1719c50f6d7cd88f6b9c4da6beb5425c03f2dc056c7a9cb597f9bf2983abb525e3c003e45858496ad3" } +extra-files: [ + "locality-warnings.patch" + "sha512=f3617f62b7ba903cae645e73d9546e3e6637adae8e81445ab9512165fb95914a20c81a1ebcb0aa7d293c38333af2724f4d2abcbc0384732d38f2a35bac0396d8" +] diff --git a/released/packages/coq-ott/coq-ott.0.33/opam b/released/packages/coq-ott/coq-ott.0.33/opam index 2fdf5c56ad..c7029e0820 100644 --- a/released/packages/coq-ott/coq-ott.0.33/opam +++ b/released/packages/coq-ott/coq-ott.0.33/opam @@ -39,3 +39,7 @@ url { src: "https://github.com/ott-lang/ott/archive/0.33.tar.gz" checksum: "sha512=fd601ef958e52ca461eaff8175323416e3e524e1ba11fcf5328827ef2cb9ee3d54111843adb54d3c32e2f08c7c70214558bf5519fb8385bfa58049f22237c3c6" } +extra-files: [ + "arith-elimtype.patch" + "sha512=c35f1f2ed05da9842d5474bf7d445dfca6829deb50237863d4baf84764b66936aafd97bb93d6da1fee869c49d49fde0b4a61de5d4f8de8d8ca38ecc882746fb2" +] diff --git a/released/packages/coq-stdpp/coq-stdpp.1.5.0/opam b/released/packages/coq-stdpp/coq-stdpp.1.5.0/opam index e47f838c88..fccc9437cb 100755 --- a/released/packages/coq-stdpp/coq-stdpp.1.5.0/opam +++ b/released/packages/coq-stdpp/coq-stdpp.1.5.0/opam @@ -45,3 +45,7 @@ url { checksum: "sha512=393ae68782370e4206e452d46c44300d5e6e27be15d9aa1dfd33ef0ccef1640f83e741f0a799c106453f305c59c5af1698ef276b47522daaefc86ece0b40f530" } +extra-files: [ + "0001-Windows-CI-strip-CR-in-result-comparison.patch" + "sha512=a44b6eb06ec85852aa00b4a029612a3b4572e23356f89259adfb3e1974d759c13e0c9a9187e174fdebcb328aec01b6e91733a3b3f8b029f8ed0cd0cd78e772fd" +] diff --git a/released/packages/coq-stdpp/coq-stdpp.1.6.0/opam b/released/packages/coq-stdpp/coq-stdpp.1.6.0/opam index cc013e62a0..f0c4c4a78e 100644 --- a/released/packages/coq-stdpp/coq-stdpp.1.6.0/opam +++ b/released/packages/coq-stdpp/coq-stdpp.1.6.0/opam @@ -46,3 +46,7 @@ url { checksum: "sha512=47de4f889a1eebce066e03512c19731a5e52f4f3bbd46e158ac00a693d983a0c8f93ec45692b3f8d16f4522296e18100ebe711cf854d50b03731bfa1914362b8" } +extra-files: [ + "ocamlrunparam.patch" + "sha512=aa778a62829f95d102c1be6a27391f1c26d8a50032cf328a44dfcef895443a12387b191f752d9f05a42535d9b0ef00bd5a87367356ba6298be1ca4af56f72663" +] diff --git a/released/packages/coq-stdpp/coq-stdpp.1.8.0/opam b/released/packages/coq-stdpp/coq-stdpp.1.8.0/opam index 4c817959d4..495d972dd4 100644 --- a/released/packages/coq-stdpp/coq-stdpp.1.8.0/opam +++ b/released/packages/coq-stdpp/coq-stdpp.1.8.0/opam @@ -46,3 +46,7 @@ url { checksum: "sha512=c894cc0574ab00efa41c807628f97abdeff917bee71b40e2f98251bcdc91ebfb7a2964683e61e7cefbe6e578b2e123098ddd7694252406f8c4835176c1d0df37" } +extra-files: [ + "curry.patch" + "sha512=504d6df94ed44ce66162d0ef5a4460dc630910e1a3228655c641d34604ec7bced723b8c6cd541fca1e16d024bae12087435656d193c0a6f7752b4c44d0270623" +] diff --git a/released/packages/coq-text2tac/coq-text2tac.1.0/opam b/released/packages/coq-text2tac/coq-text2tac.1.0/opam index 408d7bd9c9..0513dfc72f 100644 --- a/released/packages/coq-text2tac/coq-text2tac.1.0/opam +++ b/released/packages/coq-text2tac/coq-text2tac.1.0/opam @@ -36,3 +36,13 @@ extra-source "model.tar.gz" { substs: [ "Text2TacConfig.v" ] +extra-files: [ + [ + "Text2TacConfig.v.in" + "sha512=d74ad78335f373873f7ef0e6b43d426f412ff760aa933f21f4c0eef1b2dfb50fefe939a455130c0bbf15c7eeeaf834bc926645639fc48a4b46591e8d6fbef76d" + ] + [ + "injection-flags" + "sha512=08326251b37f00c79f8b74a294b9b20ee6756aaf6110bc760002b10c864fa078838406947425df66c0741e0436dcd4d4330c7958d2d04dd3831396d49e4dbb5c" + ] +] diff --git a/released/packages/coq-unimath-category-theory/coq-unimath-category-theory.0.1.0/opam b/released/packages/coq-unimath-category-theory/coq-unimath-category-theory.0.1.0/opam index 274a1d4558..08faba0078 100644 --- a/released/packages/coq-unimath-category-theory/coq-unimath-category-theory.0.1.0/opam +++ b/released/packages/coq-unimath-category-theory/coq-unimath-category-theory.0.1.0/opam @@ -18,7 +18,7 @@ depends: [ "coq-unimath-foundations" ] synopsis: "Aims to formalize a substantial body of mathematics using the univalent point of view" -extra-files: ["Make" "md5=2d439c0305755682eb748f6d6e24e74a"] +extra-files: ["Make" "sha512=83e7c98ce76848b56a7cdb225d8c308dba764b51282b7c3cbf9901e967bcc86adf20bf916a0d16c0feae27b0971b8791ddd39b1abc3d2c65b487ad034e06c948"] url { src: "https://github.com/UniMath/UniMath/archive/v0.1.tar.gz" checksum: "md5=1ed57c1028e227a309f428a6dc5f0866" diff --git a/released/packages/coq-unimath-dedekind/coq-unimath-dedekind.0.1.0/opam b/released/packages/coq-unimath-dedekind/coq-unimath-dedekind.0.1.0/opam index 799f2f037f..42d74b0b9c 100644 --- a/released/packages/coq-unimath-dedekind/coq-unimath-dedekind.0.1.0/opam +++ b/released/packages/coq-unimath-dedekind/coq-unimath-dedekind.0.1.0/opam @@ -19,7 +19,7 @@ depends: [ "coq-unimath-ktheory" ] synopsis: "Aims to formalize a substantial body of mathematics using the univalent point of view" -extra-files: ["Make" "md5=a0fc39047261f4494c06264fc9801eb6"] +extra-files: ["Make" "sha512=aee43bde4c9ea6668d88360103538b8b5ff33f9d6e2f78befcb29cd4ada6fafe39743d7a452fdc890bcf2fc555170c31c4e6430290cbed8d14cb1c54b0316c44"] url { src: "https://github.com/UniMath/UniMath/archive/v0.1.tar.gz" checksum: "md5=1ed57c1028e227a309f428a6dc5f0866" diff --git a/released/packages/coq-unimath-foundations/coq-unimath-foundations.0.1.0/opam b/released/packages/coq-unimath-foundations/coq-unimath-foundations.0.1.0/opam index 8224311e0b..1c96a641be 100644 --- a/released/packages/coq-unimath-foundations/coq-unimath-foundations.0.1.0/opam +++ b/released/packages/coq-unimath-foundations/coq-unimath-foundations.0.1.0/opam @@ -17,7 +17,7 @@ depends: [ "coq" {>= "8.5.0" & < "8.6"} ] synopsis: "Aims to formalize a substantial body of mathematics using the univalent point of view" -extra-files: ["Make" "md5=a6a04d4d56f0d1edf996019e353ca316"] +extra-files: ["Make" "sha512=5670080b4fbfc3437dd9114963e3d1a74e26934da378a67caa00711a634296aaf5104b31249f9a3b38a3ee104130b7d6eec93700a1c78fed5f4f5a3008745788"] url { src: "https://github.com/UniMath/UniMath/archive/v0.1.tar.gz" checksum: "md5=1ed57c1028e227a309f428a6dc5f0866" diff --git a/released/packages/coq-unimath-ktheory/coq-unimath-ktheory.0.1.0/opam b/released/packages/coq-unimath-ktheory/coq-unimath-ktheory.0.1.0/opam index 9cb522a4c7..3ae3678286 100644 --- a/released/packages/coq-unimath-ktheory/coq-unimath-ktheory.0.1.0/opam +++ b/released/packages/coq-unimath-ktheory/coq-unimath-ktheory.0.1.0/opam @@ -19,7 +19,7 @@ depends: [ "coq-unimath-foundations" ] synopsis: "Aims to formalize a substantial body of mathematics using the univalent point of view" -extra-files: ["Make" "md5=ba645952ced22f5cf37e29da5175d432"] +extra-files: ["Make" "sha512=f953203ffae225f4efc46eaad91fbbcfae35aa2b6841ca334585fdc24c2e394a73ff580cc3132176dc876d1377cef42a417e27c60adf706adc02a8fa647de647"] url { src: "https://github.com/UniMath/UniMath/archive/v0.1.tar.gz" checksum: "md5=1ed57c1028e227a309f428a6dc5f0866" diff --git a/released/packages/coq-unimath-substitution-systems/coq-unimath-substitution-systems.0.1.0/opam b/released/packages/coq-unimath-substitution-systems/coq-unimath-substitution-systems.0.1.0/opam index 5de8dc3ce7..1e2f92c3f8 100644 --- a/released/packages/coq-unimath-substitution-systems/coq-unimath-substitution-systems.0.1.0/opam +++ b/released/packages/coq-unimath-substitution-systems/coq-unimath-substitution-systems.0.1.0/opam @@ -19,7 +19,7 @@ depends: [ "coq-unimath-foundations" ] synopsis: "Aims to formalize a substantial body of mathematics using the univalent point of view" -extra-files: ["Make" "md5=8606de3f7fc761f04872219361ba9c7d"] +extra-files: ["Make" "sha512=eb1aaa5e70f7ed00ba2c134f9fb2fdec5112f794dc889698bf774b48524db52b8ffb9e610ffe5ad4b71742eab356d81b328ce749a3485395677f2d70b469b620"] url { src: "https://github.com/UniMath/UniMath/archive/v0.1.tar.gz" checksum: "md5=1ed57c1028e227a309f428a6dc5f0866" diff --git a/released/packages/coq-unimath-tactics/coq-unimath-tactics.0.1.0/opam b/released/packages/coq-unimath-tactics/coq-unimath-tactics.0.1.0/opam index aea6ac4e66..ad904a24a1 100644 --- a/released/packages/coq-unimath-tactics/coq-unimath-tactics.0.1.0/opam +++ b/released/packages/coq-unimath-tactics/coq-unimath-tactics.0.1.0/opam @@ -18,7 +18,7 @@ depends: [ "coq-unimath-foundations" ] synopsis: "Aims to formalize a substantial body of mathematics using the univalent point of view" -extra-files: ["Make" "md5=a92a35b43ed15f53e6e5fe7a49b6428a"] +extra-files: ["Make" "sha512=a9091f8d016402c7b0fcaf6e140ed75bd05a92172b5c00be37b8de0d639db86953e83728a56ec6285a1bd0341262ecc22909263be0b3a3eb08df172bc051aabb"] url { src: "https://github.com/UniMath/UniMath/archive/v0.1.tar.gz" checksum: "md5=1ed57c1028e227a309f428a6dc5f0866" diff --git a/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam b/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam index fcfd7cd8f3..21f8c75cd3 100644 --- a/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam +++ b/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam @@ -45,3 +45,7 @@ tags: [ "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" "logpath:VCFloat" ] +extra-files: [ + "0001-coq-native-compat.patch" + "sha512=b6f3a861b3a990a9e3e02e4517ff27672b20c9a82b3f021e7e2232f0471113f6061b3bbd2bff4732c9b105dec813918c214e21876c2a87e6ea9b69daf903ead6" +] diff --git a/released/packages/coq-vcfloat/coq-vcfloat.2.1/opam b/released/packages/coq-vcfloat/coq-vcfloat.2.1/opam index f8dee35c67..9374fcb825 100644 --- a/released/packages/coq-vcfloat/coq-vcfloat.2.1/opam +++ b/released/packages/coq-vcfloat/coq-vcfloat.2.1/opam @@ -45,3 +45,7 @@ tags: [ "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" "logpath:VCFloat" ] +extra-files: [ + "0001-coq-native-compat.patch" + "sha512=9d7e5595034dc2e2e46a7b9f5865a2c9000f9832fcd3f8aed707f6a35f164bfc7faf6773f1526def58ca862f17f7381cf2fdac00f14fc4de9d6eabe7963b3788" +] diff --git a/released/packages/coq-vst-32/coq-vst-32.2.12/opam b/released/packages/coq-vst-32/coq-vst-32.2.12/opam index ded89e205b..0a232ef035 100644 --- a/released/packages/coq-vst-32/coq-vst-32.2.12/opam +++ b/released/packages/coq-vst-32/coq-vst-32.2.12/opam @@ -54,3 +54,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.12.tar.gz" checksum: "sha512=7ca3bf55a7e5888dbfd271d9955c463d00de0e7125c60a45ca568d7de2a75104f0e740ba002e10ce7fd1ab94761c0b876816ffac4ac3f2c49af187891be604b5" } +extra-files: [ + "0001-coq-native-fix.patch" + "sha512=e5cbbd21948aa3c5bb7d9edbbb3f41d5b392a04ad8860fe074a31b89676a5e5aef91e26a45dd85e0be4f9553900c97f72533fb0a23c380fdeba59a007bafd398" +] diff --git a/released/packages/coq-vst-32/coq-vst-32.2.7/opam b/released/packages/coq-vst-32/coq-vst-32.2.7/opam index c3d8246242..0b31cec9ad 100755 --- a/released/packages/coq-vst-32/coq-vst-32.2.7/opam +++ b/released/packages/coq-vst-32/coq-vst-32.2.7/opam @@ -43,3 +43,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/v2.7.tar.gz" checksum: "sha256=970be13e71bdb013e2b9de64aecf1dda08228dd8ef3a1f6e4bb23ccd3a0896d3" } +extra-files: [ + "makefile.patch" + "sha512=13e4e4f5d102458ff10b78909015dfe2db14a818160e12fe5590ef885c1e2eb13bf40ec96b2fd764f1d7ce2b18a837d15fa565f455a9151ebe53bd0cec99a0e0" +] diff --git a/released/packages/coq-vst-32/coq-vst-32.2.8/opam b/released/packages/coq-vst-32/coq-vst-32.2.8/opam index a64307ae16..42098e0b7d 100644 --- a/released/packages/coq-vst-32/coq-vst-32.2.8/opam +++ b/released/packages/coq-vst-32/coq-vst-32.2.8/opam @@ -43,3 +43,13 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/v2.8.tar.gz" checksum: "sha512=80fae7277baf77319c9789fe4d170857862798988980f14c6ca4e11e5e027aff5dbf908848a193f90b0fb2a0dd7d12cf5f4446e2e5c13682e636d89838a08cae" } +extra-files: [ + [ + "0001-Fix-issue-485-make-install-with-IGNORECOQVERSION.patch" + "sha512=354d6890b2a8cf3fe489ef1d197e54758cd654624a82b90aa56888dd90754355dd942da10e20ace850f920cff4e573316659672c316d4b7bdaac312c1390d24c" + ] + [ + "0002-Fix-Coq-8.14.0.patch" + "sha512=567532dac5fa2b516fbcd7d61ccc9f6309b3743c3859d37516bd71659750abf2262a8fe3186d39664f292a188912021792b79649ea1026bafc233b93328d72ac" + ] +] diff --git a/released/packages/coq-vst-32/coq-vst-32.2.9.1/opam b/released/packages/coq-vst-32/coq-vst-32.2.9.1/opam index aa0cd74d88..5aa1bb3d51 100644 --- a/released/packages/coq-vst-32/coq-vst-32.2.9.1/opam +++ b/released/packages/coq-vst-32/coq-vst-32.2.9.1/opam @@ -52,3 +52,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.9.1.tar.gz" checksum: "sha512=b278947644850a7f2a1079d1fd276b96c9b0a41e2c1a80e561098117811fb3c754101a3d18f3be0b62af71044686d26a69d92ddff2d3229c864b3bcd7fa86ff2" } +extra-files: [ + "0001-Fix-issue-that-make-install-does-not-install-anythin.patch" + "sha512=36422c9314d7c5db72421ee97975cc50d256de5a19d5d672143467db839b107569aaaebcb6c098a8f28c898671d174fce38998580a14f7f3a2e9bfdfdad1b401" +] diff --git a/released/packages/coq-vst-64/coq-vst-64.2.6/opam b/released/packages/coq-vst-64/coq-vst-64.2.6/opam index 7a3f6f8ead..f06afc3459 100644 --- a/released/packages/coq-vst-64/coq-vst-64.2.6/opam +++ b/released/packages/coq-vst-64/coq-vst-64.2.6/opam @@ -45,3 +45,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/v2.6.tar.gz" checksum: "sha512=4fea46c423fd5abfa403ae88bc34a859960c6e7bbafddc1f208fc4d93af29b0711804a5eb3c917cd70d407f9a3deffa7157edc4bbfef186635280080153f47b3" } +extra-files: [ + "makefile.patch" + "sha512=d2de46c86bae55992c74361e6072ceff38e47154753276dd2dcdf5ebc453cd6ae7433efcce943bccafd6d86b59e2ac19c8c1597d6c996682b0622eaafa1eb5a8" +] diff --git a/released/packages/coq-vst/coq-vst.2.12/opam b/released/packages/coq-vst/coq-vst.2.12/opam index b97353e6ae..6ba1351219 100644 --- a/released/packages/coq-vst/coq-vst.2.12/opam +++ b/released/packages/coq-vst/coq-vst.2.12/opam @@ -51,3 +51,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.12.tar.gz" checksum: "sha512=7ca3bf55a7e5888dbfd271d9955c463d00de0e7125c60a45ca568d7de2a75104f0e740ba002e10ce7fd1ab94761c0b876816ffac4ac3f2c49af187891be604b5" } +extra-files: [ + "0001-coq-native-fix.patch" + "sha512=e5cbbd21948aa3c5bb7d9edbbb3f41d5b392a04ad8860fe074a31b89676a5e5aef91e26a45dd85e0be4f9553900c97f72533fb0a23c380fdeba59a007bafd398" +] diff --git a/released/packages/coq-vst/coq-vst.2.6/opam b/released/packages/coq-vst/coq-vst.2.6/opam index a155999b18..c690e8b512 100644 --- a/released/packages/coq-vst/coq-vst.2.6/opam +++ b/released/packages/coq-vst/coq-vst.2.6/opam @@ -45,3 +45,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/v2.6.tar.gz" checksum: "sha512=4fea46c423fd5abfa403ae88bc34a859960c6e7bbafddc1f208fc4d93af29b0711804a5eb3c917cd70d407f9a3deffa7157edc4bbfef186635280080153f47b3" } +extra-files: [ + "makefile.patch" + "sha512=d2de46c86bae55992c74361e6072ceff38e47154753276dd2dcdf5ebc453cd6ae7433efcce943bccafd6d86b59e2ac19c8c1597d6c996682b0622eaafa1eb5a8" +] diff --git a/released/packages/coq-vst/coq-vst.2.7/opam b/released/packages/coq-vst/coq-vst.2.7/opam index b0b7b60723..240dec3814 100755 --- a/released/packages/coq-vst/coq-vst.2.7/opam +++ b/released/packages/coq-vst/coq-vst.2.7/opam @@ -47,3 +47,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/v2.7.tar.gz" checksum: "sha256=970be13e71bdb013e2b9de64aecf1dda08228dd8ef3a1f6e4bb23ccd3a0896d3" } +extra-files: [ + "makefile.patch" + "sha512=13e4e4f5d102458ff10b78909015dfe2db14a818160e12fe5590ef885c1e2eb13bf40ec96b2fd764f1d7ce2b18a837d15fa565f455a9151ebe53bd0cec99a0e0" +] diff --git a/released/packages/coq-vst/coq-vst.2.8/opam b/released/packages/coq-vst/coq-vst.2.8/opam index fc91fab13c..6076cb8b01 100755 --- a/released/packages/coq-vst/coq-vst.2.8/opam +++ b/released/packages/coq-vst/coq-vst.2.8/opam @@ -43,3 +43,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/v2.8.tar.gz" checksum: "sha512=80fae7277baf77319c9789fe4d170857862798988980f14c6ca4e11e5e027aff5dbf908848a193f90b0fb2a0dd7d12cf5f4446e2e5c13682e636d89838a08cae" } +extra-files: [ + "0001-Fix-issue-485-make-install-with-IGNORECOQVERSION.patch" + "sha512=354d6890b2a8cf3fe489ef1d197e54758cd654624a82b90aa56888dd90754355dd942da10e20ace850f920cff4e573316659672c316d4b7bdaac312c1390d24c" +] diff --git a/released/packages/coq-vst/coq-vst.2.9.1/opam b/released/packages/coq-vst/coq-vst.2.9.1/opam index 58ce33ed71..72c522b6c0 100755 --- a/released/packages/coq-vst/coq-vst.2.9.1/opam +++ b/released/packages/coq-vst/coq-vst.2.9.1/opam @@ -52,3 +52,7 @@ url { src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.9.1.tar.gz" checksum: "sha512=b278947644850a7f2a1079d1fd276b96c9b0a41e2c1a80e561098117811fb3c754101a3d18f3be0b62af71044686d26a69d92ddff2d3229c864b3bcd7fa86ff2" } +extra-files: [ + "0001-Fix-issue-that-make-install-does-not-install-anythin.patch" + "sha512=36422c9314d7c5db72421ee97975cc50d256de5a19d5d672143467db839b107569aaaebcb6c098a8f28c898671d174fce38998580a14f7f3a2e9bfdfdad1b401" +]