package Coq 8.12.0 #16876
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| bin: [ | ||
| "bin/coqwc" | ||
| "bin/coqtop" | ||
| "bin/coqtop.byte" | ||
| "bin/coqdoc" | ||
| "bin/coqdep" | ||
| "bin/coqchk" | ||
| "bin/coqc" | ||
| "bin/coq_makefile" | ||
| "bin/coq-tex" | ||
| "bin/coqworkmgr" | ||
| ] |
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,52 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "coqdev@inria.fr" | ||
| authors: "The Coq development team, INRIA, CNRS, and contributors." | ||
| homepage: "https://coq.inria.fr/" | ||
| bug-reports: "https://github.com/coq/coq/issues" | ||
| dev-repo: "git+https://github.com/coq/coq.git" | ||
| license: "LGPL-2.1-only" | ||
| synopsis: "Formal proof management system" | ||
| description: """ | ||
| The Coq proof assistant 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 and the | ||
| Bedrock verified low-level programming library), the formalization of | ||
| mathematics (e.g., the full formalization of the Feit-Thompson theorem | ||
| and homotopy type theory) and teaching. | ||
| """ | ||
|
|
||
| depends: [ | ||
| "ocaml" {>= "4.05.0" & < "4.12"} | ||
| "ocamlfind" {build} | ||
| "num" | ||
| "conf-findutils" {build} | ||
| ] | ||
| build: [ | ||
| [ | ||
| "./configure" | ||
| "-configdir" "%{lib}%/coq/config" | ||
| "-prefix" prefix | ||
| "-mandir" man | ||
| "-docdir" doc | ||
| "-libdir" "%{lib}%/coq" | ||
| "-datadir" "%{share}%/coq" | ||
| "-coqide" "no" | ||
| ] | ||
| [make "-j%{jobs}%"] | ||
| [make "-j%{jobs}%" "byte"] | ||
| ] | ||
| install: [ | ||
| [make "install"] | ||
| [make "install-byte"] | ||
| ] | ||
|
|
||
| extra-files: [ | ||
| ["coq.install" "sha512=b501737b4dbd22adc1c0377d744448056fb1dc493caf72c05f57c8463cf23f758373605ab3a50b9f505e4c856c41039d0bd7f81f96ed62adc6a674179523e7d2"] | ||
| ] | ||
|
|
||
| url { | ||
| src: "https://github.com/coq/coq/archive/V8.12.0.tar.gz" | ||
| checksum: "sha512=8a64624c578ce0ab781fb3b1f162bd8b095735ad891fdad2fb7c40849afbdc7c1360187c6b62a5ef2982566f4c6c78029240c611ae769943a5250af300eb1240" | ||
| } |
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,9 @@ | ||
| bin: [ | ||
| "bin/coqide" | ||
| ] | ||
| share_root: [ | ||
| "ide/coq.lang" {"coq/coq.lang"} | ||
| "ide/coq-ssreflect.lang" {"coq/coq-ssreflect.lang"} | ||
| "ide/coq.png" {"coq/coq.png"} | ||
| "ide/coq_style.xml" {"coq/coq_style.xml"} | ||
| ] |
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,49 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "coqdev@inria.fr" | ||
| authors: "The Coq development team, INRIA, CNRS, and contributors." | ||
| homepage: "https://coq.inria.fr/" | ||
| bug-reports: "https://github.com/coq/coq/issues" | ||
| dev-repo: "git+https://github.com/coq/coq.git" | ||
| license: "LGPL-2.1-only" | ||
| synopsis: "IDE of the Coq formal proof management system" | ||
| description: """ | ||
| CoqIDE is a graphical user interface for interactive development | ||
| of mathematical definitions, executable algorithms, and proofs of theorems | ||
| using the Coq proof assistant. | ||
| """ | ||
|
|
||
| depends: [ | ||
| "coq" {= version} | ||
| "lablgtk3-sourceview3" {>= "3.1.0"} | ||
|
There was a problem hiding this comment. @RalfJung @ejgallego : Is there a good reason for the restriction to lablgtk 3.1.0? For a reason yet to be investigated this version does not build on windows, but 3.0.beta5 does and it seems to work fine. There was a problem hiding this comment. Summing up: no, beta7 had to be banned only for coqide 8.10.*. No comment on potential other problems. === Below the former comments which I dropped.
There was a problem hiding this comment. Okay, I opened #16881 to relax the version bound. |
||
| "conf-findutils" {build} | ||
| "conf-gnome-icon-theme3" | ||
| ] | ||
| build: [ | ||
| [ | ||
| "./configure" | ||
| "-configdir" "%{lib}%/coq/config" | ||
| "-prefix" prefix | ||
| "-mandir" man | ||
| "-docdir" doc | ||
| "-libdir" "%{lib}%/coq" | ||
| "-datadir" "%{share}%/coq" | ||
| ] | ||
| [make "-j%{jobs}%" "coqide-files"] | ||
| [make "-j%{jobs}%" "coqide-opt"] | ||
| ] | ||
| install: [ | ||
| make | ||
| "install-ide-bin" | ||
| "install-ide-files" | ||
| "install-ide-info" | ||
| "install-ide-devfiles" | ||
| ] | ||
|
|
||
| extra-files: [ | ||
| ["coqide.install" "sha512=0c59f0c3cf3453e92c02b29aceb31090020410d2b0dd2856172cd19b1b2b58b2a1d46047fb08a9c1d4767d87934c73ae6adfcb4204b1ea6a55a85ba75b2b812d"] | ||
| ] | ||
|
|
||
| url { | ||
| src: "https://github.com/coq/coq/archive/V8.12.0.tar.gz" | ||
| checksum: "sha512=8a64624c578ce0ab781fb3b1f162bd8b095735ad891fdad2fb7c40849afbdc7c1360187c6b62a5ef2982566f4c6c78029240c611ae769943a5250af300eb1240" | ||
| } | ||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let's remember to split CoqIDE out if there are problems in CI.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't follow... we want a CoqIDE package, no?
I consider creating two PRs and tracking their mutual dependencies to be just unnecessary work.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Your call; I was just mentioning @palmskog's suggestion to avoid holding up Coq packages (IIRC because coqide held up some 8.11.* version for a long while). No strong opinion myself.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
But again, no action needed if there are no problems in CI 🙂