-
Notifications
You must be signed in to change notification settings - Fork 166
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
392 changed files
with
10,268 additions
and
296 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
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,68 @@ | ||
| 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: "https://github.com/coq/coq/releases/download/V8.20+rc1/coq-8.20-rc1.tar.gz" | ||
| checksum: [ | ||
| "md5=3a50a9d2768cf5dd0190afbd81f97051" | ||
| "sha512=895730028bb00a6b0c71d2b3fdff6d215f6bcc40a8223b20f7e1ce15a6cea0b3ca2243babeeac39653db887ae0147f98fb9e808d1b1b9b9e26baf2bc849c82ab" | ||
| ] | ||
| } |
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,55 @@ | ||
| 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/coq/coq/releases/download/V8.20+rc1/coq-8.20-rc1.tar.gz" | ||
| checksum: [ | ||
| "md5=3a50a9d2768cf5dd0190afbd81f97051" | ||
| "sha512=895730028bb00a6b0c71d2b3fdff6d215f6bcc40a8223b20f7e1ce15a6cea0b3ca2243babeeac39653db887ae0147f98fb9e808d1b1b9b9e26baf2bc849c82ab" | ||
| ] | ||
| } |
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
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,60 @@ | ||
| 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: | ||
| "https://github.com/coq/coq/releases/download/V8.20+rc1/coq-8.20-rc1.tar.gz" | ||
| checksum: [ | ||
| "md5=3a50a9d2768cf5dd0190afbd81f97051" | ||
| "sha512=895730028bb00a6b0c71d2b3fdff6d215f6bcc40a8223b20f7e1ce15a6cea0b3ca2243babeeac39653db887ae0147f98fb9e808d1b1b9b9e26baf2bc849c82ab" | ||
| ] | ||
| } |
Oops, something went wrong.