forked from coq/opam
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into update-elpi-2
- Loading branch information
Showing
313 changed files
with
9,855 additions
and
95 deletions.
There are no files selected for viewing
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
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
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
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,65 @@ | ||
| 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" {>= "3.6.1" & < "3.14"} | ||
| "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" "memtrace"] | ||
| 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: "git+https://github.com/coq/coq.git#v8.20" | ||
| } |
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
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,51 @@ | ||
| 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: "git+https://github.com/coq/coq.git#v8.20" | ||
| } |
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 @@ | ||
| 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} | ||
| "conf-python-3" {with-test} | ||
| "conf-time" {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: "git+https://github.com/coq/coq.git#v8.20" | ||
| } |
44 changes: 44 additions & 0 deletions
44
core-dev/packages/coqide-server/coqide-server.8.20.dev/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,44 @@ | ||
| opam-version: "2.0" | ||
| 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 | ||
| "--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: "git+https://github.com/coq/coq.git#v8.20" | ||
| } |
46 changes: 46 additions & 0 deletions
46
extra-dev/packages/coq-bignums/coq-bignums.9.0.0+coq8.20/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,46 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
|
|
||
| homepage: "https://github.com/coq-community/bignums" | ||
| dev-repo: "git+https://github.com/coq-community/bignums.git" | ||
| bug-reports: "https://github.com/coq-community/bignums/issues" | ||
| license: "LGPL-2.1-only" | ||
|
|
||
| synopsis: "Bignums, the Coq library of arbitrarily large numbers" | ||
| description: """ | ||
| This Coq library provides BigN, BigZ, and BigQ that used to | ||
| be part of the standard library.""" | ||
|
|
||
| build: [make "-j%{jobs}%"] | ||
| install: [ | ||
| [make "install"] | ||
| [make "-C" "tests" "-j%{jobs}%"] {with-test} | ||
| ] | ||
| depends: [ | ||
| "ocaml" | ||
| "coq" {>= "8.20" & < "8.21~"} | ||
| ] | ||
|
|
||
| tags: [ | ||
| "category:Miscellaneous/Coq Extensions" | ||
| "category:Mathematics/Arithmetic and Number Theory/Number theory" | ||
| "category:Mathematics/Arithmetic and Number Theory/Rational numbers" | ||
| "keyword:integer numbers" | ||
| "keyword:rational numbers" | ||
| "keyword:arithmetic" | ||
| "keyword:arbitrary precision" | ||
| "logpath:Bignums" | ||
| "date:2024-06-20" | ||
| ] | ||
| authors: [ | ||
| "Laurent Théry" | ||
| "Benjamin Grégoire" | ||
| "Arnaud Spiwack" | ||
| "Evgeny Makarov" | ||
| "Pierre Letouzey" | ||
| ] | ||
|
|
||
| url { | ||
| src: "https://github.com/coq/bignums/archive/v9.0.0+coq8.20.tar.gz" | ||
| checksum: "sha512=2c83c5c4caf77b68280dd56ca658da176e4223794b1627e8ac86b9e310a6cc81082bd4e880449b1c330013f1540ff1f78ddfce7a8d4039c3b00ba59904273d61" | ||
| } |
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,45 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "The CertiCoq Team" | ||
| homepage: "https://certicoq.org/" | ||
| dev-repo: "git+https://github.com/CertiCoq/certicoq" | ||
| bug-reports: "https://github.com/CertiCoq/certicoq/issues" | ||
| authors: ["Andrew Appel" | ||
| "Yannick Forster" | ||
| "Anvay Grover" | ||
| "Joomy Korkut" | ||
| "John Li" | ||
| "Zoe Paraskevopoulou" | ||
| "Matthieu Sozeau" | ||
| "Matthew Weaver" | ||
| "Abhishek Anand" | ||
| "Greg Morrisett" | ||
| "Randy Pollack" | ||
| "Olivier Savary Belanger" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["bash" "./configure.sh"] | ||
| [make "all"] | ||
| [make "plugins"] | ||
| [make "bootstrap"] | ||
| [make "-C" "benchmarks" "all"] {with-test} | ||
| [make "-C" "bootstrap" "tests"] {with-test} | ||
| ] | ||
| install: [ | ||
| [make "install"] | ||
| ] | ||
| depends: [ | ||
| "ocaml" | ||
| "stdlib-shims" | ||
| "coq" {>= "8.17" & < "8.18~"} | ||
| "coq-compcert" {= "3.12"} | ||
| "coq-equations" {= "1.3+8.17"} | ||
| "coq-metacoq-erasure-plugin" {= "8.17.dev"} | ||
| "coq-metacoq-safechecker-plugin" {= "8.17.dev"} | ||
| "coq-ext-lib" {>= "0.11.8"} | ||
| ] | ||
|
|
||
| synopsis: "A Verified Compiler for Gallina, Written in Gallina " | ||
| url { | ||
| src: "git+https://github.com/CertiCoq/certicoq.git#master" | ||
| } |
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
Oops, something went wrong.