-
Notifications
You must be signed in to change notification settings - Fork 49
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add a pick for 8.19.2 with the Ltac2 debugger (preview)
- Loading branch information
Showing
6 changed files
with
523 additions
and
0 deletions.
There are no files selected for viewing
70 changes: 70 additions & 0 deletions
70
opam/opam-repository/packages/coq-core/coq-core.8.19.2.ltac2debug/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,70 @@ | ||
| 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 <[email protected]>"] | ||
| 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" | ||
| XXXpatches: [ "PR19247-ported-Fix-coqide-compilation-with-lablgtk-3.1.5-on-windows.patch" ] | ||
| 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_tag.tar.gz" | ||
| checksum: [ | ||
| "md5=8466fc9ec474a73376a48b0ec70f9f6f" | ||
| "sha512=bd67ad44fd1787e69b1d5a7e45189e0399ecf3ff52e7c76d45f43c4389a9491cde0643ba5a4093eae26c137eca05c394d34f8e0e3e2e5eace1bd53fc1a8ad944" | ||
| ] | ||
| } |
56 changes: 56 additions & 0 deletions
56
opam/opam-repository/packages/coq-stdlib/coq-stdlib.8.19.2.ltac2debug/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <[email protected]>"] | ||
| 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_tag.tar.gz" | ||
| checksum: [ | ||
| "md5=8466fc9ec474a73376a48b0ec70f9f6f" | ||
| "sha512=bd67ad44fd1787e69b1d5a7e45189e0399ecf3ff52e7c76d45f43c4389a9491cde0643ba5a4093eae26c137eca05c394d34f8e0e3e2e5eace1bd53fc1a8ad944" | ||
| ] | ||
| } |
59 changes: 59 additions & 0 deletions
59
opam/opam-repository/packages/coq/coq.8.19.2.ltac2debug/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <[email protected]>"] | ||
| 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/jfehrle/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_tag.tar.gz" | ||
| checksum: [ | ||
| "md5=8466fc9ec474a73376a48b0ec70f9f6f" | ||
| "sha512=bd67ad44fd1787e69b1d5a7e45189e0399ecf3ff52e7c76d45f43c4389a9491cde0643ba5a4093eae26c137eca05c394d34f8e0e3e2e5eace1bd53fc1a8ad944" | ||
| ] | ||
| } |
47 changes: 47 additions & 0 deletions
47
opam/opam-repository/packages/coqide-server/coqide-server.8.19.2.ltac2debug/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <[email protected]>"] | ||
| 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_tag.tar.gz" | ||
| checksum: [ | ||
| "md5=8466fc9ec474a73376a48b0ec70f9f6f" | ||
| "sha512=bd67ad44fd1787e69b1d5a7e45189e0399ecf3ff52e7c76d45f43c4389a9491cde0643ba5a4093eae26c137eca05c394d34f8e0e3e2e5eace1bd53fc1a8ad944" | ||
| ] | ||
| } |
59 changes: 59 additions & 0 deletions
59
opam/opam-repository/packages/coqide/coqide.8.19.2.ltac2debug/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <[email protected]>"] | ||
| 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/jfehrle/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_tag.tar.gz" | ||
| checksum: [ | ||
| "md5=8466fc9ec474a73376a48b0ec70f9f6f" | ||
| "sha512=bd67ad44fd1787e69b1d5a7e45189e0399ecf3ff52e7c76d45f43c4389a9491cde0643ba5a4093eae26c137eca05c394d34f8e0e3e2e5eace1bd53fc1a8ad944" | ||
| ] | ||
| } |
Oops, something went wrong.