From cf00cd482d8ac65563c7801f09159dd94931b35e Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Tue, 10 Sep 2024 23:22:09 -0700 Subject: [PATCH] Add a pick for 8.19.2 with the Ltac2 debugger (preview) --- .../coq-core/coq-core.8.19.2.ltac2debug/opam | 69 ++++++ .../coq-stdlib.8.19.2.ltac2debug/opam | 56 +++++ .../packages/coq/coq.8.19.2.ltac2debug/opam | 59 +++++ .../coqide-server.8.19.2.ltac2debug/opam | 47 ++++ .../coqide/coqide.8.19.2.ltac2debug/opam | 52 ++++ ...ackage-pick-8.19-2024.01+ltac2-debugger.sh | 232 ++++++++++++++++++ 6 files changed, 515 insertions(+) create mode 100644 opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam create mode 100644 opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam create mode 100644 opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam create mode 100644 opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam create mode 100644 opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam create mode 100644 package_picks/package-pick-8.19-2024.01+ltac2-debugger.sh diff --git a/opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam new file mode 100644 index 0000000000..82c6ae653d --- /dev/null +++ b/opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam @@ -0,0 +1,69 @@ +opam-version: "2.0" +synopsis: "The Coq Proof Assistant -- Core Binaries and Tools" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq core binaries, plugins, and tools, but +not the vernacular standard library. + +Note that in this setup, Coq needs to be started with the -boot and +-noinit options, as will otherwise fail to find the regular Coq +prelude, now living in the coq-stdlib package.""" +maintainer: ["The Coq development team "] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "2.9"} + "ocaml" {>= "4.09.0"} + "ocamlfind" {>= "1.8.1"} + "zarith" {>= "1.11"} + "conf-linux-libc-dev" {os = "linux"} + "odoc" {with-doc} +] +conflicts: [ + "coq" { < "8.17" } +] +depopts: ["coq-native" "memprof-limits"] +dev-repo: "git+https://github.com/coq/coq.git" +build: [ + ["dune" "subst"] {dev} + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] + +url { + src: "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz" + checksum: [ + "md5=8540549341f6425174165edec2bc5c29" + "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f" + ] +} diff --git a/opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam new file mode 100644 index 0000000000..a9b4d78fe1 --- /dev/null +++ b/opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam @@ -0,0 +1,56 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "The Coq Proof Assistant -- Standard Library" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching. + +This package includes the Coq Standard Library, that is to say, the +set of modules usually bound to the Coq.* namespace.""" +maintainer: ["The Coq development team "] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "3.6"} + "coq-core" {= version} + "odoc" {with-doc} +] +depopts: ["coq-native"] +dev-repo: "git+https://github.com/coq/coq.git" +build: [ + ["dune" "subst"] {dev} + # We tell dunestrap to use coq-config from coq-core + [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +url { + src: + "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz" + checksum: [ + "md5=8540549341f6425174165edec2bc5c29" + "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f" + ] +} \ No newline at end of file diff --git a/opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam new file mode 100644 index 0000000000..e0c6854d0d --- /dev/null +++ b/opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam @@ -0,0 +1,59 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +Typical applications include the certification of properties of +programming languages (e.g. the CompCert compiler certification +project, or the Bedrock verified low-level programming library), the +formalization of mathematics (e.g. the full formalization of the +Feit-Thompson theorem or homotopy type theory) and teaching.""" +maintainer: ["The Coq development team "] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "3.6"} + "coq-core" {= version} + "coq-stdlib" {= version} + "coqide-server" {= version} + "ounit2" {with-test} + "odoc" {with-doc} +] +dev-repo: "git+https://github.com/coq/coq.git" +build: [ + ["dune" "subst"] {dev} + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] {with-test} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +url { + src: + "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz" + checksum: [ + "md5=8540549341f6425174165edec2bc5c29" + "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f" + ] +} \ No newline at end of file diff --git a/opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam new file mode 100644 index 0000000000..639148d39a --- /dev/null +++ b/opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam @@ -0,0 +1,47 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +synopsis: "The Coq Proof Assistant, XML protocol server" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the `coqidetop` language server, an +implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md) +which allows clients, such as CoqIDE, to interact with Coq in a +structured way.""" +maintainer: ["The Coq development team "] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "3.6"} + "coq-core" {= version} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" +url { + src: "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz" + checksum: [ + "md5=8540549341f6425174165edec2bc5c29" + "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f" + ] +} \ No newline at end of file diff --git a/opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam b/opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam new file mode 100644 index 0000000000..eec6de9cdb --- /dev/null +++ b/opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam @@ -0,0 +1,52 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "The Coq Proof Assistant --- GTK3 IDE" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the CoqIDE, a graphical user interface for the +development of interactive proofs.""" +maintainer: ["The Coq development team "] +authors: ["The Coq development team, INRIA, CNRS, and contributors"] +license: "LGPL-2.1-only" +homepage: "https://coq.inria.fr/" +doc: "https://coq.github.io/doc/" +bug-reports: "https://github.com/coq/coq/issues" +depends: [ + "dune" {>= "2.9"} + "ocamlfind" {build} + "conf-findutils" {build} + "conf-adwaita-icon-theme" + "coqide-server" {= version} + "cairo2" {>= "0.6.4"} + "lablgtk3-sourceview3" {>= "3.1.5"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/coq/coq.git" + +url { + src: "https://github.com/jfehrle/coq/archive/refs/tags/debug_pl_8_19_tag2.tar.gz" + checksum: [ + "md5=8540549341f6425174165edec2bc5c29" + "sha512=00833a93914d485e6ca695b6cec220da47957d7e3358bfe8e68300c48935255e95436be751826d837dfbd5f784116df86c1b57a8fe7e3301b45b4b19bffe958f" + ] +} diff --git a/package_picks/package-pick-8.19-2024.01+ltac2-debugger.sh b/package_picks/package-pick-8.19-2024.01+ltac2-debugger.sh new file mode 100644 index 0000000000..e880d03422 --- /dev/null +++ b/package_picks/package-pick-8.19-2024.01+ltac2-debugger.sh @@ -0,0 +1,232 @@ +#!/usr/bin/env bash + +###################### COPYRIGHT/COPYLEFT ###################### + +# (C) 2020..2022 Michael Soegtrop + +# Released to the public under the +# Creative Commons CC0 1.0 Universal License +# See https://creativecommons.org/publicdomain/zero/1.0/legalcode.txt + +###################### CONTROL VARIABLES ##################### + +# The two lines below are used by the package selection script +COQ_PLATFORM_VERSION_TITLE="Coq 8.19.2+ltac2-debugger (released Sept 2024)" +COQ_PLATFORM_VERSION_SORTORDER=97 + +# The package list name is the final part of the opam switch name. +# It is usually either empty ot starts with ~. +# It might also be used for installer package names, but with ~ replaced by _ +# It is also used for version specific file selections in the smoke test kit. +COQ_PLATFORM_PACKAGE_PICK_POSTFIX='~8.19~2024.01+ltac2-debugger' + +# The corresponding Coq development branch and tag +COQ_PLATFORM_COQ_BRANCH='v8.19' +COQ_PLATFORM_COQ_TAG='debug_pl_8_19_tag' + +# This controls if opam repositories for development packages are selected +COQ_PLATFORM_USE_DEV_REPOSITORY='N' + +# This extended descriptions is used for readme files +COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2024.01.0 includes the Ltac2 debugger from July 2024. ' + +# The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way) +COQ_PLATFORM_OCAML_VERSION='4.14.2' + +###################### PACKAGE SELECTION ##################### + +PACKAGES="" + +# - Comment out packages you do not want. +# - Packages which take a long time to build should be given last. +# There is some evidence that they are built early then. +# - Versions ending with ~flex are identical to the opam package without the +# ~flex extension, except that version restrictions have been relaxed. +# - The picking tracker issue is https://github.com/coq/platform/issues/193 + +########## BASE PACKAGES ########## + +# Coq needs a patched ocamlfind to be relocatable by installers +PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.5~relocatable" # TODO port patch to 1.9.6 +# Since dune does support Coq, it is explicitly selected +PACKAGES="${PACKAGES} PIN.dune.3.15.3" +PACKAGES="${PACKAGES} PIN.dune-configurator.3.15.3" +# The Coq compiler coqc and the Coq standard library +PACKAGES="${PACKAGES} PIN.coq.8.19.2.ltac2debug PIN.coq-core.8.19.2.ltac2debug" + +########## IDE PACKAGES ########## + +# GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[iIfFxX] ]] +then +PACKAGES="${PACKAGES} coqide.8.19.2.ltac2debug" +fi + +########## "FULL" COQ PLATFORM PACKAGES ########## + +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[fFxX] ]] +then + # Standard library extensions + PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.19" + PACKAGES="${PACKAGES} coq-ext-lib.0.12.1" + PACKAGES="${PACKAGES} coq-stdpp.1.10.0" + + # General mathematics + PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.2.0" + PACKAGES="${PACKAGES} coq-mathcomp-fingroup.2.2.0" + PACKAGES="${PACKAGES} coq-mathcomp-algebra.2.2.0" + PACKAGES="${PACKAGES} coq-mathcomp-solvable.2.2.0" + PACKAGES="${PACKAGES} coq-mathcomp-field.2.2.0" + PACKAGES="${PACKAGES} coq-mathcomp-character.2.2.0" + PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.1" + PACKAGES="${PACKAGES} coq-mathcomp-finmap.2.1.0" + PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.0" + PACKAGES="${PACKAGES} coq-mathcomp-zify.1.5.0+2.0+8.16" + PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.2.0" + PACKAGES="${PACKAGES} coq-coquelicot.3.4.1" + + # Number theory + PACKAGES="${PACKAGES} coq-coqprime.1.5.0" + PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" #NOTE:THIS IS STILL TAGGED TO v8.14.1, SHOULD SOMETHING BE DONE? + + # Numerical mathematics + PACKAGES="${PACKAGES} coq-flocq.4.1.4" + PACKAGES="${PACKAGES} coq-interval.4.10.0" + PACKAGES="${PACKAGES} coq-gappa.1.5.5" + PACKAGES="${PACKAGES} gappa.1.4.1" + + # Constructive mathematics + PACKAGES="${PACKAGES} coq-math-classes.8.19.0" + PACKAGES="${PACKAGES} coq-corn.8.19.0" + + # Homotopy Type Theory (HoTT) + PACKAGES="${PACKAGES} coq-hott.8.19" + + # Univalent Mathematics (UniMath) + # Note: coq-unimath requires too much memory for 32 bit architectures + if [ "${BITSIZE}" == "64" ] + then + case "$COQ_PLATFORM_UNIMATH" in + [yY]) PACKAGES="${PACKAGES} coq-unimath.20240331" ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_UNIMATH - aborting"; false ;; + esac + fi + + # Code extraction + PACKAGES="${PACKAGES} coq-simple-io.1.8.0" + + # Proof automation / generation / helpers + PACKAGES="${PACKAGES} coq-menhirlib.20231231 menhir.20231231" + PACKAGES="${PACKAGES} coq-equations.1.3+8.19" + PACKAGES="${PACKAGES} coq-aac-tactics.8.19.0" + PACKAGES="${PACKAGES} coq-unicoq.1.6+8.19" + if [[ "$OSTYPE" != cygwin ]] + then + PACKAGES="${PACKAGES} coq-mtac2.1.4+8.19" # build issues on Windows + fi + PACKAGES="${PACKAGES} elpi.1.18.2 coq-elpi.2.1.0" + PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0" + if [[ "$OSTYPE" != cygwin ]] + then + PACKAGES="${PACKAGES} coq-quickchick.2.0.3" # build issues on Windows + fi + PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.19" + if [[ "$OSTYPE" != cygwin ]] + then + # coq-hammer does not work on Windows because it heavily relies on fork + PACKAGES="${PACKAGES} coq-hammer.1.3.2+8.19" + PACKAGES="${PACKAGES} eprover.3.1" + PACKAGES="${PACKAGES} z3_tptp.4.13.0" + fi + PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.19" + PACKAGES="${PACKAGES} coq-coqeal.2.0.2" + PACKAGES="${PACKAGES} coq-libhyps.2.0.8" + PACKAGES="${PACKAGES} coq-itauto.8.19.0" #DOES NOT BUILD ON WINDOWS + + # General mathematics (which requires one of the above tools) + PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.1.0" + PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.2.3" + PACKAGES="${PACKAGES} coq-relation-algebra.1.7.10" + + # Formal languages, compilers and code verification + PACKAGES="${PACKAGES} coq-reglang.1.2.1" + PACKAGES="${PACKAGES} coq-iris.4.2.0" + PACKAGES="${PACKAGES} coq-iris-heap-lang.4.2.0" + if [[ "$OSTYPE" != cygwin ]] + then + # Windows: some issues with executable extensions (ott.opt instead of ott.exe) + # Note: 0.32 does work on Windows! + PACKAGES="${PACKAGES} coq-ott.0.33" + PACKAGES="${PACKAGES} ott.0.33" + fi + PACKAGES="${PACKAGES} coq-mathcomp-word.3.0" + + case "$COQ_PLATFORM_COMPCERT" in + [yY]) PACKAGES="${PACKAGES} coq-compcert.3.13.1" ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_COMPCERT - aborting"; false ;; + esac + + case "$COQ_PLATFORM_VST" in + [yY]) + PACKAGES="${PACKAGES} coq-vst.2.14" + true ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_VST - aborting"; false ;; + esac + + # # Proof analysis and other tools + PACKAGES="${PACKAGES} coq-dpdgraph.1.0+8.19" +fi + +########## EXTENDED" COQ PLATFORM PACKAGES ########## + +if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[xX] ]] +then + + # Proof automation / generation / helpers + PACKAGES="${PACKAGES} coq-deriving.0.2.0" + if [ "${BITSIZE}" == "64" ] + then + PACKAGES="${PACKAGES} coq-metacoq.1.3.1+8.19" + fi + + # General mathematics + PACKAGES="${PACKAGES} coq-extructures.0.4.0" + + # Gallina extensions + PACKAGES="${PACKAGES} coq-reduction-effects.0.1.5" + PACKAGES="${PACKAGES} coq-record-update.0.3.4" + + # Communication with coqtop + if [[ "$OSTYPE" != cygwin ]] + then + # Windows: path length issues + PACKAGES="${PACKAGES} coq-serapi.8.19.0+0.19.2" + + fi + + # fiat crypto, bedrock2, rupicola and dependencies + if [ "${BITSIZE}" == "64" ] + then + case "$COQ_PLATFORM_FIATCRYPTO" in + [yY]) + PACKAGES="${PACKAGES} coq-coqutil.0.0.5" + PACKAGES="${PACKAGES} coq-rewriter.0.0.11" + PACKAGES="${PACKAGES} coq-riscv.0.0.5" + PACKAGES="${PACKAGES} coq-bedrock2.0.0.7" + PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.7" + PACKAGES="${PACKAGES} coq-rupicola.0.0.9" + if [ "$OSTYPE" != cygwin ] + then + # Windows: stack overflow + PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.2" + true + fi + ;; + [nN]) true ;; + *) echo "Illegal value for COQ_PLATFORM_FIATCRYPTO - aborting"; false ;; + esac + fi +fi \ No newline at end of file