Skip to content

Commit

Permalink
Merge pull request #2880 from palmskog/8.19-supported
Browse files Browse the repository at this point in the history
compatibility for coq-community packages with 8.19
  • Loading branch information
palmskog authored Dec 28, 2023
2 parents fb22344 + 986df0d commit 5b7f7d3
Show file tree
Hide file tree
Showing 5 changed files with 42 additions and 4 deletions.
38 changes: 38 additions & 0 deletions released/packages/coq-almost-full/coq-almost-full.8.18.0/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
opam-version: "2.0"
maintainer: "[email protected]"

homepage: "https://github.com/coq-community/almost-full"
dev-repo: "git+https://github.com/coq-community/almost-full.git"
bug-reports: "https://github.com/coq-community/almost-full/issues"
license: "MIT"

synopsis: "Almost-full relations in Coq for proving termination"
description: """
Coq development of almost-full relations, including the Ramsey
Theorem, useful for proving termination."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.11" & < "8.20"}
]

tags: [
"category:Computer Science/Data Types and Data Structures"
"keyword:Ramsey theorem"
"keyword:termination"
"keyword:almost-full relations"
"keyword:well-founded relations"
"logpath:AlmostFull"
"date:2023-12-28"
]
authors: [
"Dimitrios Vytiniotis"
"Thierry Coquand"
"David Wahlstedt"
]

url {
src: "https://github.com/coq-community/almost-full/releases/download/v8.18.0/almost-full-8.18.0.tar.gz"
checksum: "sha512=c6871611ae19c34dfd6c27f86c29c9b38cff126cc2631684357a3cf04bb5d38e8aed0d4178f26f9c584e16cda7c6c6d1422996c0b057fe7fd8f5470662d284b3"
}
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ Includes a proof of Ptolemy's theorem."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.16" & < "8.19"}
"coq" {>= "8.16" & < "8.20"}
]

tags: [
Expand Down
2 changes: 1 addition & 1 deletion released/packages/coq-huffman/coq-huffman.8.16.0/opam
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Codes, Proc. IRE, pp. 1098-1101, September 1952."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.12" & < "8.19~"}
"coq" {>= "8.12" & < "8.20"}
]

tags: [
Expand Down
2 changes: 1 addition & 1 deletion released/packages/coq-jmlcoq/coq-jmlcoq.8.15.0/opam
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ verified runtime assertion checker for JML."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.10" & < "8.19~"}
"coq" {>= "8.10" & < "8.20"}
]

tags: [
Expand Down
2 changes: 1 addition & 1 deletion released/packages/coq-sudoku/coq-sudoku.8.16.0/opam
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Davis-Putnam procedure to solve Sudokus."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.12" & < "8.17~"}
"coq" {>= "8.12" & < "8.20"}
]

tags: [
Expand Down

0 comments on commit 5b7f7d3

Please sign in to comment.