From f7258d4f2bafbc697bd435893f0fb22f03a15db6 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 12:18:01 +0100 Subject: [PATCH 1/9] Pick 8.20~2025.01: updated coq-coqprime-generator to version 1.1.2 --- package_picks/package-pick-8.20~2025.01.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index e69c150435..8ffc64204a 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -94,7 +94,7 @@ then # Number theory PACKAGES="${PACKAGES} coq-coqprime.1.6.0" - PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" #TODO: this points to https://github.com/thery/coqprime/archive/v8.14.1.tar.gz + PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.2" # Numerical mathematics PACKAGES="${PACKAGES} coq-flocq.4.2.0" From de1f88b0dd6518277495d4e65f9de0cf55932283 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 13:27:36 +0100 Subject: [PATCH 2/9] Pick 8.20~2025.01: updated ott and coq-ott to version 0.34 --- package_picks/package-pick-8.20~2025.01.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index 8ffc64204a..e423a1883c 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -153,8 +153,8 @@ then PACKAGES="${PACKAGES} coq-reglang.1.2.1" PACKAGES="${PACKAGES} coq-iris.4.3.0" PACKAGES="${PACKAGES} coq-iris-heap-lang.4.3.0" - PACKAGES="${PACKAGES} coq-ott.0.33" - PACKAGES="${PACKAGES} ott.0.33" + PACKAGES="${PACKAGES} coq-ott.0.34" + PACKAGES="${PACKAGES} ott.0.34" PACKAGES="${PACKAGES} coq-mathcomp-word.3.2" # Works with version relaxation case "$COQ_PLATFORM_COMPCERT" in From 74b5333ae8b710f54c308d7ac31a2b1b2fe42ee7 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 13:29:32 +0100 Subject: [PATCH 3/9] Pick 8.20~2025.01: updated coq-compcert to version 3.15 --- package_picks/package-pick-8.20~2025.01.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index e423a1883c..45ee272284 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -158,7 +158,7 @@ then PACKAGES="${PACKAGES} coq-mathcomp-word.3.2" # Works with version relaxation case "$COQ_PLATFORM_COMPCERT" in - [yY]) PACKAGES="${PACKAGES} coq-compcert.3.13.1" ;; # ToDo: there is CompCert 3.14, but VST requires 3.13.1 + [yY]) PACKAGES="${PACKAGES} coq-compcert.3.15" [nN]) true ;; *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;; esac From 286f25f90fedd08860b913626ef575ad8bfe7d5d Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 13:30:03 +0100 Subject: [PATCH 4/9] Pick 8.20~2025.01: updated coq-vst to version 2.15 --- package_picks/package-pick-8.20~2025.01.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index 45ee272284..bb88b4da04 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -165,7 +165,7 @@ then case "$COQ_PLATFORM_VST" in [yY]) - PACKAGES="${PACKAGES} coq-vst.2.14" + PACKAGES="${PACKAGES} coq-vst.2.15" true ;; [nN]) true ;; *) echo "Illegal value for COQ_PLATFORM_VST - aborting"; false ;; From 61c83945a0766a6466e55eacf75a3af7e4b195ab Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 13:43:55 +0100 Subject: [PATCH 5/9] Opam: removed local packages from opam-coq-archive which are available upstream --- .../coq-mathcomp-algebra-tactics.1.2.3/opam | 43 ------------- .../coq-mathcomp-word.3.2/opam | 29 --------- ...issues-with-generated-code-on-Window.patch | 29 --------- .../coq-metacoq-template.1.1+8.16/opam | 60 ------------------- .../coq-unimath/coq-unimath.20240923/opam | 18 ------ 5 files changed, 179 deletions(-) delete mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.3/opam delete mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-word/coq-mathcomp-word.3.2/opam delete mode 100755 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch delete mode 100755 opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam delete mode 100644 opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20240923/opam diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.3/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.3/opam deleted file mode 100644 index c99fbc049e..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.3/opam +++ /dev/null @@ -1,43 +0,0 @@ -opam-version: "2.0" -maintainer: "kazuhiko.sakaguchi@inria.fr" - -homepage: "https://github.com/math-comp/algebra-tactics" -dev-repo: "git+https://github.com/math-comp/algebra-tactics.git" -bug-reports: "https://github.com/math-comp/algebra-tactics/issues" -license: "CECILL-B" - -synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components" -description: """ -This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for -the Mathematical Components library. These tactics use the algebraic -structures defined in the MathComp library and their canonical instances for -the instance resolution, and do not require any special instance declaration, -like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics -works with any instance of the respective structure, including concrete -instances declared through Hierarchy Builder, abstract instances, and mixed -concrete and abstract instances, e.g., `int * R` where `R` is an abstract -commutative ring. Another key feature of Algebra Tactics is that they -automatically push down ring morphisms and additive functions to leaves of -ring/field expressions before applying the proof procedures.""" - -build: [make "-j%{jobs}%"] -install: [make "install"] -depends: [ - "coq" {>= "8.16" & < "8.21~"} - "coq-mathcomp-ssreflect" {>= "2.0" & < "2.4~"} - "coq-mathcomp-algebra" - "coq-mathcomp-zify" {>= "1.5.0"} - "coq-elpi" {>= "1.15.0" & != "1.17.0"} -] - -tags: [ - "logpath:mathcomp.algebra_tactics" -] -authors: [ - "Kazuhiko Sakaguchi" - "Pierre Roux" -] -url { - src: "https://github.com/math-comp/algebra-tactics/archive/refs/tags/1.2.3.tar.gz" - checksum: "sha256=a556875e9ed8db1f77474de77c6ae56142c4477a9f11438d70e1f346c90001e4" -} diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-word/coq-mathcomp-word.3.2/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-word/coq-mathcomp-word.3.2/opam deleted file mode 100644 index cb75cc7b69..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-mathcomp-word/coq-mathcomp-word.3.2/opam +++ /dev/null @@ -1,29 +0,0 @@ -opam-version: "2.0" -maintainer: "pierre-yves@strub.nu" - -homepage: "https://github.com/jasmin-lang/coqword" -bug-reports: "https://github.com/jasmin-lang/coqword/issues" -dev-repo: "git+https://github.com/jasmin-lang/coqword.git" -license: "MIT" - -synopsis: "Yet Another Coq Library on Machine Words" - -build: [ "dune" "build" "-p" name "-j" jobs ] -depends: [ - "dune" {>= "2.8"} - "coq" {>= "8.16"} - "coq-mathcomp-ssreflect" {>= "2.0" & < "2.4~"} - "coq-mathcomp-algebra" -] -tags: [ - "category:Computer Science/Data Types and Data Structures" - "keyword:machine words" - "logpath:mathcomp.word" - "date:2024-03-21" -] -authors: ["Pierre-Yves Strub"] - -url { - src: "https://github.com/jasmin-lang/coqword/releases/download/v3.2/coq-mathcomp-word-v3.2.tbz" - checksum: "sha512=503c252b6dc7cec12348c7224d4cd1fbd2ce5c2674c8e295238f18d7aefa2bdd97d19a7ff184701455c70d3755868c3c996bf600652cb12315bdee95d750b470" -} diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch deleted file mode 100755 index a420880d66..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/files/0001-Fix-line-ending-issues-with-generated-code-on-Window.patch +++ /dev/null @@ -1,29 +0,0 @@ -From 838930ef5983c0e19bd9e12ddb5b12cf5b367c8e Mon Sep 17 00:00:00 2001 -From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> -Date: Fri, 30 Sep 2022 09:15:08 +0200 -Subject: [PATCH] Fix line ending issues with generated code on Windows - ---- - template-coq/update_plugin.sh | 6 ++++++ - 1 file changed, 6 insertions(+) - -diff --git a/template-coq/update_plugin.sh b/template-coq/update_plugin.sh -index 9b3d2a5f..1842cfde 100755 ---- a/template-coq/update_plugin.sh -+++ b/template-coq/update_plugin.sh -@@ -12,6 +12,12 @@ then - echo "Renaming files to camelCase" - (cd gen-src; ./to-lower.sh) - rm -f gen-src/*.d gen-src/*.cm* -+ echo "Prepare line endings for patching (for Windows)" -+ for f in gen-src/*.ml* -+ do -+ tr -d '\r' < "$f" > tmp -+ mv -f tmp $f -+ done - # Fix an extraction bug: wrong type annotation on eq_equivalence - patch -N -p0 < extraction.patch - patch -N -p0 < specFloat.patch --- -2.37.3 - diff --git a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam b/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam deleted file mode 100755 index 42449eb9b6..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam +++ /dev/null @@ -1,60 +0,0 @@ -opam-version: "2.0" -maintainer: "matthieu.sozeau@inria.fr" -homepage: "https://metacoq.github.io/metacoq" -dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" -bug-reports: "https://github.com/MetaCoq/metacoq/issues" -authors: ["Abhishek Anand " - "Danil Annenkov " - "Simon Boulier " - "Cyril Cohen " - "Yannick Forster " - "Fabian Kunze " - "Meven Lennon-Bertrand " - "Kenji Maillard " - "Gregory Malecha " - "Jakob Botsch Nielsen " - "Matthieu Sozeau " - "Nicolas Tabareau " - "Théo Winterhalter " -] -license: "MIT" -patches: [ - "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch" -] -build: [ - ["bash" "./configure.sh"] - [make "-j" "%{jobs}%" "template-coq"] -] -install: [ - [make "-C" "template-coq" "install"] -] -depends: [ - "stdlib-shims" - "coq" { >= "8.16" & < "8.17~" } - "coq-equations" { >= "1.3" } -] -synopsis: "A quoting and unquoting library for Coq in Coq" -description: """ -MetaCoq is a meta-programming framework for Coq. - -Template Coq is a quoting library for Coq. It takes Coq terms and -constructs a representation of their syntax tree as a Coq inductive data -type. The representation is based on the kernel's term representation. - -In addition to a complete reification and denotation of CIC terms, -Template Coq includes: - -- Reification of the environment structures, for constant and inductive declarations. -- Denotation of terms and global declarations -- A monad for manipulating global declarations, calling the type - checker, and inserting them in the global environment, in the style of - MetaCoq/MTac. -""" -url { - src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.16.tar.gz" - checksum: "sha512=abd34042fc2804954abc8b1fba4c2b3d1d1c0c780874ad0cbe698a19756e26985c77bb231b2e9b40ea01261f3fbbb36fbdd2b7095931e947bf933359cb0154f7" -} -extra-files: [ - "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch" - "sha512=6b626b68ea3376ee3e532c8cbd024bd083be4b37e7fc933c4445c8fe7bc22022bc06a63b4f49e610381ee8a0218b0b42950ca417ca9404e84cbd16068191294e" -] diff --git a/opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20240923/opam b/opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20240923/opam deleted file mode 100644 index aa7043a3dd..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20240923/opam +++ /dev/null @@ -1,18 +0,0 @@ -opam-version: "2.0" -maintainer: "The UniMath Development Team" -homepage: "https://github.com/UniMath/UniMath" -dev-repo: "git+https://github.com/UniMath/UniMath.git" -bug-reports: "https://github.com/UniMath/UniMath/issues" -license: "Similar to MIT license" -authors: ["The UniMath Development Team"] -build: [make "BUILD_COQ=no" "-j%{jobs}%"] -install: [make "BUILD_COQ=no" "install"] -depends: [ - "ocaml" - "coq" {>= "8.18"} -] -synopsis: "Library of Univalent Mathematics" -url { - src: "https://github.com/UniMath/UniMath/archive/refs/tags/v20240923.tar.gz" - checksum: "sha512=ffb905217bc6426d6ad00168959961f560a05c040b10de0145ef27e1d93e9ab9ef60f7f5127fc8b9e0b04ad99608b452dbf261bc34072ee4f47ef6b6951bbc47" -} From 6e2b7755e5ba958525d14ed777777605b696c367 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 13:47:32 +0100 Subject: [PATCH 6/9] Opam: removed local dev packages from opam-coq-archive which are available upstream --- .../0001-Allow-dev-version-of-Menhir.patch | 44 ----------- .../coq-compcert-32/coq-compcert-32.dev/opam | 74 ------------------- .../0001-Allow-dev-version-of-Menhir.patch | 44 ----------- .../coq-compcert/coq-compcert.dev/opam | 61 --------------- .../packages/coq-serapi/coq-serapi.dev/opam | 47 ------------ .../packages/coq-vst-32/coq-vst-32.dev/opam | 42 ----------- .../packages/coq-vst/coq-vst.dev/opam | 43 ----------- .../extra-dev/packages/ott/ott.dev/opam | 41 ---------- 8 files changed, 396 deletions(-) delete mode 100755 opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch delete mode 100755 opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam delete mode 100755 opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch delete mode 100755 opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/opam delete mode 100644 opam/opam-coq-archive/extra-dev/packages/coq-serapi/coq-serapi.dev/opam delete mode 100755 opam/opam-coq-archive/extra-dev/packages/coq-vst-32/coq-vst-32.dev/opam delete mode 100755 opam/opam-coq-archive/extra-dev/packages/coq-vst/coq-vst.dev/opam delete mode 100644 opam/opam-coq-archive/extra-dev/packages/ott/ott.dev/opam diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch b/opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch deleted file mode 100755 index 52c92775f1..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/files/0001-Allow-dev-version-of-Menhir.patch +++ /dev/null @@ -1,44 +0,0 @@ -From b2f8e4d0fdea4611b56f8e2c2feade3e8fb632b7 Mon Sep 17 00:00:00 2001 -From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> -Date: Sun, 27 Dec 2020 15:18:54 +0100 -Subject: [PATCH] Allow dev version of Menhir - ---- - configure | 14 +++++++++++++- - 1 file changed, 13 insertions(+), 1 deletion(-) - -diff --git a/configure b/configure -index 7cbb9d7d..4c494379 100755 ---- a/configure -+++ b/configure -@@ -556,7 +556,7 @@ fi - - MENHIR_REQUIRED=20190626 - echo "Testing Menhir... " | tr -d '\n' --menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` -+menhir_ver=$(menhir --version 2>/dev/null | sed -n -E -e 's/^.*version (unreleased|[0-9]*).*$/\1/p') - case "$menhir_ver" in - 20[0-9][0-9][0-9][0-9][0-9][0-9]) - if test "$menhir_ver" -ge $MENHIR_REQUIRED; then -@@ -576,6 +576,18 @@ case "$menhir_ver" in - echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." - missingtools=true - fi;; -+ unreleased) -+ echo "version $menhir_ver -- acceptable!" -+ menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ -+ menhir_dir=$(menhir --suggest-menhirLib) || \ -+ menhir_dir="" -+ menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') -+ if test ! -d "$menhir_dir"; then -+ echo "Error: cannot determine the location of the Menhir API library." -+ echo "This can be due to an incorrect Menhir package." -+ echo "Consider using the OPAM package for Menhir." -+ missingtools=true -+ fi;; - *) - echo "NOT FOUND" - echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed." --- -2.29.2 - diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam b/opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam deleted file mode 100755 index f0aa5288c3..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-compcert-32/coq-compcert-32.dev/opam +++ /dev/null @@ -1,74 +0,0 @@ -opam-version: "2.0" -authors: "Xavier Leroy " -maintainer: "Jacques-Henri Jourdan " -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" -available: os != "macos" -patches: [ - "0001-Allow-dev-version-of-Menhir.patch" - "0001-Rename-Flocq-to-Flocq3.patch" {coq-flocq3:installed} -] -build: [ - ["./configure" - "ia32-linux" {os = "linux"} - "ia32-cygwin" {os = "cygwin"} - # This is for building a MinGW CompCert with cygwin host and cygwin target - "ia32-cygwin" {os = "win32" & os-distribution = "cygwinports"} - # This is for building a 32 bit CompCert on 64 bit MinGW with cygwin build host - "-toolprefix" {os = "win32" & os-distribution = "cygwinports" & arch = "x86_64"} - "i686-pc-cygwin-" {os = "win32" & os-distribution = "cygwinports" & arch = "x86_64"} - # The 32 bit CompCert is a variant which is installed in a non standard folder - "-prefix" "%{prefix}%/variants/compcert32" - "-install-coqdev" - "-clightgen" - "-use-external-Flocq" - "-use-external-MenhirLib" - "-coqdevdir" "%{lib}%/coq-variant/compcert32/compcert" - "-ignore-coq-version"] - [make "-j%{jobs}%" {ocaml:version >= "4.06"}] -] -install: [ - [make "install"] -] -depends: [ - "coq" {>= "8.8" | = "dev"} - "menhir" {>= "20190626" | = "dev"} - "ocaml" {>= "4.05.0"} - ("coq-flocq" {>= "3.1.0"} | "coq-flocq3" {>= "3.4.3"}) - "coq-menhirlib" {>= "20190626" | = "dev"} -] -synopsis: "The CompCert C compiler (32 bit)" -description: "This package installs the 32 bit version of CompCert. -For coexistence with the 64 bit version, the files are installed in: -%{prefix}%/variants/compcert32/bin (ccomp and clightgen binaries) -%{prefix}%/variants/compcert32/lib/compcert (C library) -%{lib}%/coq-variant/compcert32/compcert (Coq library) -Please note that the coq module path is compcert and not compcert32, -so the files cannot be directly Required as compcert32. -Instead -Q or -R options must be used to bind the compcert32 folder -to the module path compcert. This is more convenient if one development -supports both 32 and 64 bit versions. Otherwise all files would have to -be duplicated with module paths compcert and compcert32. -Please also note that the binary folder is usually not in the path." -tags: [ - "category:CS/Semantics and Compilation/Compilation" - "category:CS/Semantics and Compilation/Semantics" - "keyword:C" - "keyword:compiler" - "logpath:compcert32" -] -url { - src: "git+https://github.com/AbsInt/CompCert.git" -} -extra-files: [ - [ - "0001-Allow-dev-version-of-Menhir.patch" - "sha512=76f4222174fe2ff396ccef236b249a5094f4258459c3d74a074e714ddab7da6ea22d66a264386202988e16e6e5713c7ef06c043751890369e0c35c5915e2c832" - ] - [ - "0001-Rename-Flocq-to-Flocq3.patch" - "sha512=37d8d026e6762fad178b91c340bb5e26ba616ae26e077f2613776bdecf75b65fe43ba558f0d093a10cd9d45a016384450b966776abf5d154fee8b706135465a8" - ] -] diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch b/opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch deleted file mode 100755 index 52c92775f1..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/files/0001-Allow-dev-version-of-Menhir.patch +++ /dev/null @@ -1,44 +0,0 @@ -From b2f8e4d0fdea4611b56f8e2c2feade3e8fb632b7 Mon Sep 17 00:00:00 2001 -From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> -Date: Sun, 27 Dec 2020 15:18:54 +0100 -Subject: [PATCH] Allow dev version of Menhir - ---- - configure | 14 +++++++++++++- - 1 file changed, 13 insertions(+), 1 deletion(-) - -diff --git a/configure b/configure -index 7cbb9d7d..4c494379 100755 ---- a/configure -+++ b/configure -@@ -556,7 +556,7 @@ fi - - MENHIR_REQUIRED=20190626 - echo "Testing Menhir... " | tr -d '\n' --menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` -+menhir_ver=$(menhir --version 2>/dev/null | sed -n -E -e 's/^.*version (unreleased|[0-9]*).*$/\1/p') - case "$menhir_ver" in - 20[0-9][0-9][0-9][0-9][0-9][0-9]) - if test "$menhir_ver" -ge $MENHIR_REQUIRED; then -@@ -576,6 +576,18 @@ case "$menhir_ver" in - echo "Error: CompCert requires a version greater or equal to $MENHIR_REQUIRED." - missingtools=true - fi;; -+ unreleased) -+ echo "version $menhir_ver -- acceptable!" -+ menhir_dir=$(ocamlfind query menhirLib 2>/dev/null) || \ -+ menhir_dir=$(menhir --suggest-menhirLib) || \ -+ menhir_dir="" -+ menhir_dir=$(echo "$menhir_dir" | tr -d '\r' | tr '\\' '/') -+ if test ! -d "$menhir_dir"; then -+ echo "Error: cannot determine the location of the Menhir API library." -+ echo "This can be due to an incorrect Menhir package." -+ echo "Consider using the OPAM package for Menhir." -+ missingtools=true -+ fi;; - *) - echo "NOT FOUND" - echo "Error: make sure Menhir version $MENHIR_REQUIRED or later is installed." --- -2.29.2 - diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/opam b/opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/opam deleted file mode 100755 index d46949f319..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-compcert/coq-compcert.dev/opam +++ /dev/null @@ -1,61 +0,0 @@ -opam-version: "2.0" -authors: "Xavier Leroy " -maintainer: "Jacques-Henri Jourdan " -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" -patches: [ - "0001-Allow-dev-version-of-Menhir.patch" - "0001-Rename-Flocq-to-Flocq3.patch" {coq-flocq3:installed} -] -build: [ - ["./configure" - "amd64-linux" {os = "linux"} - "amd64-macosx" {os = "macos"} - "amd64-cygwin" {os = "cygwin"} - # This is for building a MinGW CompCert with cygwin host and cygwin target - "amd64-cygwin" {os = "win32" & os-distribution = "cygwinports"} - # This is for building a 64 bit CompCert on 32 bit MinGW with cygwin build host - "-toolprefix" {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} - "x86_64-pc-cygwin-" {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} - "-prefix" "%{prefix}%" - "-install-coqdev" - "-clightgen" - "-use-external-Flocq" - "-use-external-MenhirLib" - "-coqdevdir" "%{lib}%/coq/user-contrib/compcert" - "-ignore-coq-version"] - [make "-j%{jobs}%" {ocaml:version >= "4.06"}] -] -install: [ - [make "install"] -] -depends: [ - "coq" {>= "8.8.0" | = "dev"} - "menhir" {>= "20190626" | = "dev"} - "ocaml" {>= "4.05.0"} - ("coq-flocq" {>= "3.1.0"} | "coq-flocq3" {>= "3.4.3"}) - "coq-menhirlib" {>= "20190626" | = "dev"} -] -synopsis: "The CompCert C compiler (64 bit)" -tags: [ - "category:CS/Semantics and Compilation/Compilation" - "category:CS/Semantics and Compilation/Semantics" - "keyword:C" - "keyword:compiler" - "logpath:compcert" -] -url { - src: "git+https://github.com/AbsInt/CompCert.git" -} -extra-files: [ - [ - "0001-Allow-dev-version-of-Menhir.patch" - "sha512=76f4222174fe2ff396ccef236b249a5094f4258459c3d74a074e714ddab7da6ea22d66a264386202988e16e6e5713c7ef06c043751890369e0c35c5915e2c832" - ] - [ - "0001-Rename-Flocq-to-Flocq3.patch" - "sha512=37d8d026e6762fad178b91c340bb5e26ba616ae26e077f2613776bdecf75b65fe43ba558f0d093a10cd9d45a016384450b966776abf5d154fee8b706135465a8" - ] -] diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-serapi/coq-serapi.dev/opam b/opam/opam-coq-archive/extra-dev/packages/coq-serapi/coq-serapi.dev/opam deleted file mode 100644 index 1d1ad39dd2..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-serapi/coq-serapi.dev/opam +++ /dev/null @@ -1,47 +0,0 @@ -opam-version: "2.0" -maintainer: "e@x80.org" -homepage: "https://github.com/ejgallego/coq-serapi" -bug-reports: "https://github.com/ejgallego/coq-serapi/issues" -dev-repo: "git+https://github.com/ejgallego/coq-serapi.git" -license: "GPL-3.0-or-later" -doc: "https://ejgallego.github.io/coq-serapi/" - -synopsis: "Serialization library and protocol for machine interaction with the Coq proof assistant" -description: """ -SerAPI is a library for machine-to-machine interaction with the -Coq proof assistant, with particular emphasis on applications in IDEs, -code analysis tools, and machine learning. SerAPI provides automatic -serialization of Coq's internal OCaml datatypes from/to JSON or -S-expressions (sexps). -""" - -authors: [ - "Emilio Jesús Gallego Arias" - "Karl Palmskog" - "Clément Pit-Claudel" - "Kaiyu Yang" -] - -depends: [ - "ocaml" { >= "4.09.0" } - "coq" { >= "8.16" } - "cmdliner" { >= "1.1.0" } - "ocamlfind" { >= "1.8.0" } - "sexplib" { >= "v0.13.0" } - "dune" { >= "2.0.1" } - "ppx_import" { build & >= "1.5-3" } - "ppx_deriving" { >= "4.2.1" } - "ppx_sexp_conv" { >= "v0.13.0" } - "ppx_compare" { >= "v0.13.0" } - "ppx_hash" { >= "v0.13.0" } - "yojson" { >= "1.7.0" } - "ppx_deriving_yojson" { >= "3.4" } -] -conflicts: [ - "result" {< "1.5"} -] - -build: [ "dune" "build" "-p" name "-j" jobs ] -url { - src: "git+https://github.com/ejgallego/coq-serapi.git" -} diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-vst-32/coq-vst-32.dev/opam b/opam/opam-coq-archive/extra-dev/packages/coq-vst-32/coq-vst-32.dev/opam deleted file mode 100755 index f17248d249..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-vst-32/coq-vst-32.dev/opam +++ /dev/null @@ -1,42 +0,0 @@ -opam-version: "2.0" -synopsis: "Verified Software Toolchain" -description: "The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context." -authors: [ - "Andrew W. Appel" - "Lennart Beringer" - "Sandrine Blazy" - "Qinxiang Cao" - "Santiago Cuellar" - "Robert Dockins" - "Josiah Dodds" - "Nick Giannarakis" - "Samuel Gruetter" - "Aquinas Hobor" - "Jean-Marie Madiot" - "William Mansky" -] -maintainer: "VST team" -homepage: "http://vst.cs.princeton.edu/" -dev-repo: "git+https://github.com/PrincetonUniversity/VST.git" -bug-reports: "https://github.com/PrincetonUniversity/VST/issues" -license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE" -build: [ - [make "-j%{jobs}%" "IGNORECOQVERSION=true" "BITSIZE=32"] -] -install: [ - [make "install" "IGNORECOQVERSION=true" "BITSIZE=32"] -] -depends: [ - "ocaml" - "coq" {>= "8.11" | = "dev"} - "coq-compcert-32" {= "3.10" | = "3.10~flocq3" | = "dev" | = "dev~flocq3"} -] -tags: [ - "category:CS/Semantics and Compilation/Semantics" - "keyword:C" - "logpath:VST" - "date:2020-12-20" -] -url { - src: "git+https://github.com/PrincetonUniversity/VST.git#master" -} diff --git a/opam/opam-coq-archive/extra-dev/packages/coq-vst/coq-vst.dev/opam b/opam/opam-coq-archive/extra-dev/packages/coq-vst/coq-vst.dev/opam deleted file mode 100755 index ef638c953c..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/coq-vst/coq-vst.dev/opam +++ /dev/null @@ -1,43 +0,0 @@ -opam-version: "2.0" -synopsis: "Verified Software Toolchain" -description: "The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context." -authors: [ - "Andrew W. Appel" - "Lennart Beringer" - "Sandrine Blazy" - "Qinxiang Cao" - "Santiago Cuellar" - "Robert Dockins" - "Josiah Dodds" - "Nick Giannarakis" - "Samuel Gruetter" - "Aquinas Hobor" - "Jean-Marie Madiot" - "William Mansky" -] -maintainer: "VST team" -homepage: "http://vst.cs.princeton.edu/" -dev-repo: "git+https://github.com/PrincetonUniversity/VST.git" -bug-reports: "https://github.com/PrincetonUniversity/VST/issues" -license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE" -build: [ - [make "-j%{jobs}%" "IGNORECOQVERSION=true" "BITSIZE=64"] -] -install: [ - [make "install" "IGNORECOQVERSION=true" "BITSIZE=64"] -] -depends: [ - "ocaml" - "coq" {>= "8.11" | = "dev"} - # Note: the dev version of VST requires clightgen, so no open source - "coq-compcert" {= "3.10" | = "3.10~flocq3" | = "dev" | = "dev~flocq3"} -] -tags: [ - "category:CS/Semantics and Compilation/Semantics" - "keyword:C" - "logpath:VST" - "date:2020-12-20" -] -url { - src: "git+https://github.com/PrincetonUniversity/VST.git#master" -} diff --git a/opam/opam-coq-archive/extra-dev/packages/ott/ott.dev/opam b/opam/opam-coq-archive/extra-dev/packages/ott/ott.dev/opam deleted file mode 100644 index 555d118e87..0000000000 --- a/opam/opam-coq-archive/extra-dev/packages/ott/ott.dev/opam +++ /dev/null @@ -1,41 +0,0 @@ -opam-version: "2.0" -maintainer: "Hannes Mehnert " -authors: ["Peter Sewell" "Francesco Zappa Nardelli" "Scott Owens"] -license: "part BSD3, part LGPL 2.1" -homepage: "http://www.cl.cam.ac.uk/~pes20/ott/" -bug-reports: "https://github.com/ott-lang/ott/issues" -depends: [ - "ocaml" {>= "4.02.0"} - "pprint" {with-test} - "menhir" {>= "20151112" & with-test} -] -build: [ - [make "world"] - [make "ott.install"] -] -run-test: [ - [make "-C" "tests/menhir_tests/test_if"] - [make "-C" "tests/menhir_tests/test10menhir"] - [make "-C" "tests/menhir_tests/test10menhir_with_aux_args"] - [make "-C" "tests/menhir_tests/test10menhir_with_aux_rules"] -] -dev-repo: "git+https://github.com/ott-lang/ott.git" -synopsis: "A tool for writing definitions of programming languages and calculi" -description: """ -Ott takes as input a definition of a language syntax and semantics, in a -concise and readable ASCII notation that is close to what one would write in -informal mathematics. It generates output: -- a LaTeX source file that defines commands to build a typeset version of the definition; -- a Coq version of the definition; -- a HOL version of the definition; -- an Isabelle/HOL version of the definition; -- a Lem version of the definition; -- an OCaml version of the syntax of the definition. -Additionally, it can be run as a filter, taking a -LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file -with embedded (symbolic) terms of the defined language, parsing them and -replacing them by typeset terms. -""" -url { - src: "git+https://github.com/ott-lang/ott.git" -} From ff3d14074bf2d89e0527ceb2580c430693382af0 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 13:58:17 +0100 Subject: [PATCH 7/9] Pick 8.20~2025.01: fix typo in script introduced by version update --- package_picks/package-pick-8.20~2025.01.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index bb88b4da04..4c3c344613 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -158,7 +158,7 @@ then PACKAGES="${PACKAGES} coq-mathcomp-word.3.2" # Works with version relaxation case "$COQ_PLATFORM_COMPCERT" in - [yY]) PACKAGES="${PACKAGES} coq-compcert.3.15" + [yY]) PACKAGES="${PACKAGES} coq-compcert.3.15" ;; [nN]) true ;; *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;; esac From 3ea490fb2d41e5b8798cb34c02fd3e34b09cfe09 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Mon, 27 Jan 2025 14:15:50 +0100 Subject: [PATCH 8/9] Pick 8.20~2025.01: reverted coq-coqprime-generator to version 1.1.1 - 1.1.2 requires OCaml 5.0 --- package_picks/package-pick-8.20~2025.01.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh index 4c3c344613..b6ae3ca32e 100644 --- a/package_picks/package-pick-8.20~2025.01.sh +++ b/package_picks/package-pick-8.20~2025.01.sh @@ -94,7 +94,7 @@ then # Number theory PACKAGES="${PACKAGES} coq-coqprime.1.6.0" - PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.2" + PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" # Note: there is a newer version 1.1.2, but it requires Ocaml 5.X # Numerical mathematics PACKAGES="${PACKAGES} coq-flocq.4.2.0" From a030c3b89d19f8cd654b3eeb25b4ac99abaea8b8 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Date: Tue, 28 Jan 2025 09:34:18 +0100 Subject: [PATCH 9/9] Opam: adjust opam patch package for elpi.1.16.9 to upstream changes --- opam/opam-repository/packages/elpi/elpi.1.16.9/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opam/opam-repository/packages/elpi/elpi.1.16.9/opam b/opam/opam-repository/packages/elpi/elpi.1.16.9/opam index cc1df5a8d0..5045fc3c5e 100644 --- a/opam/opam-repository/packages/elpi/elpi.1.16.9/opam +++ b/opam/opam-repository/packages/elpi/elpi.1.16.9/opam @@ -25,7 +25,7 @@ depends: [ "cmdliner" {with-test} "dune" {>= "2.8.0"} "conf-time" {with-test} - "atdgen" {>= "2.10.0"} + "atdgen" {>= "2.10.0" & < "2.16.0"} "atdts" {>= "2.10.0"} "odoc" {with-doc} ]