Merge pull request #3204 from MSoegtropIMC/opam-230-adjustments

Add extra-files records where need to support opam 2.3.0 - Fixes #3203
coq · Nov 14, 2024 · 971e294 · 971e294
2 parents 4c90b59 + f1dd3d2
commit 971e294
Show file tree

Hide file tree

Showing 74 changed files with 445 additions and 95 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -14,7 +14,7 @@ depends: [
 ]
 synopsis: "The CompCert C compiler"
 authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-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
@@ -15,7 +15,7 @@ depends: [
 ]
 synopsis: "The CompCert C compiler"
 authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-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
@@ -15,7 +15,7 @@ depends: [
 ]
 synopsis: "The CompCert C compiler"
 authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-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
@@ -29,7 +29,7 @@ depends: [
 patches: "fix-coq-version.patch"
 synopsis: "The CompCert C compiler"
 authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-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
@@ -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
@@ -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
@@ -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"]