Skip to content

Commit 858ab2d

Browse files
proux01proux01
authored
Merge pull request #3309 from proux01/nix-backport
Backport from coq-nix-toolbox
2 parents 5974d3c + b6100f9 commit 858ab2d

File tree

21 files changed

+137
-21
lines changed
  • released/packages
    • coq-autosubst/coq-autosubst.1.9
    • coq-color/coq-color.1.8.5
    • coq-deriving/coq-deriving.0.2.1
    • coq-elpi/coq-elpi.2.4.0
    • coq-extructures/coq-extructures.0.5.0
    • coq-fourcolor/coq-fourcolor.1.4.0
    • coq-hierarchy-builder/coq-hierarchy-builder.1.8.1
    • coq-iris/coq-iris.4.3.0
    • coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.4
    • coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.2
    • coq-mathcomp-classical/coq-mathcomp-classical.1.8.0
    • coq-mathcomp-finmap/coq-mathcomp-finmap.2.1.0
    • coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.8.0
    • coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0
    • coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.2
    • coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16
    • coq-paco/coq-paco.4.2.2
    • coq-record-update/coq-record-update.0.3.4
    • coq-reglang/coq-reglang.1.2.1
    • coq-simple-io/coq-simple-io.1.10.0
    • coq-stdpp/coq-stdpp.1.11.0

21 files changed

+137
-21
lines changed

‎released/packages/coq-autosubst/coq-autosubst.1.9/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ substitutions."""
1919
build: [make "-j%{jobs}%"]
2020
install: [make "install"]
2121
depends: [
22-
"coq" {>= "8.14" & < "8.21~"}
22+
"coq" {>= "8.14" & < "9.1~"}
2323
]
2424

2525
tags: [

‎released/packages/coq-color/coq-color.1.8.5/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ install: [make "-f" "Makefile.coq" "install"]
2424
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/CoLoR"]
2525
depends: [
2626
"ocaml"
27-
"coq" {>= "8.14" & < "8.21~"}
27+
"coq" {>= "8.14" & < "9.1~"}
2828
"coq-bignums"
2929
]
3030
tags: [

‎released/packages/coq-deriving/coq-deriving.0.2.1/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ license: "MIT"
99
build: [ make "-j" "%{jobs}%" "test" {with-test} ]
1010
install: [ make "install" ]
1111
depends: [
12-
"coq" { (>= "8.17" & < "8.21~") | (= "dev") }
12+
"coq" { (>= "8.17" & < "9.1~") | (= "dev") }
1313
"coq-mathcomp-ssreflect" {>= "2.0"}
1414
]
1515

‎released/packages/coq-elpi/coq-elpi.2.4.0/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ depends: [
1818
"dune" {>= "3.13"}
1919
"ocaml" {>= "4.10.0"}
2020
"elpi" {>= "2.0.7" & < "2.1.0~"}
21-
"coq" {>= "8.20+rc1" & < "8.21~"}
21+
"coq" {>= "8.20+rc1" & < "9.1~"}
2222
"ppx_optcomp"
2323
"ocaml-lsp-server" {with-dev-setup}
2424
"odoc" {with-doc}
@@ -45,4 +45,4 @@ url {
4545
checksum: [
4646
"sha512=327cf88912571884f5d5598c658b47c73694cf8fbc74cf7a2c65eb2577c3adc6b767c49c18216e19cf59c1661e315265e82e9b7a2226305ae56bee6bc9895b9d"
4747
]
48-
}
48+
}

‎released/packages/coq-extructures/coq-extructures.0.5.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ install: [
1313
[make "install"]
1414
]
1515
depends: [
16-
"coq" {(>= "8.17" & < "8.21~")}
16+
"coq" {(>= "8.17" & < "9.1~")}
1717
"coq-mathcomp-ssreflect" {(>= "2.0.0")}
1818
"coq-deriving" {(>= "0.2.0")}
1919
]

‎released/packages/coq-fourcolor/coq-fourcolor.1.4.0/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ basic plane topology definitions, and a theory of combinatorial hypermaps."""
1616
build: [make "-C" "theories/proof" "-j%{jobs}%"]
1717
install: [make "-C" "theories/proof" "install"]
1818
depends: [
19-
"coq" {(>= "8.16" & < "8.21~") | (= "dev")}
19+
"coq" {(>= "8.16" & < "9.1~") | (= "dev")}
2020
"coq-mathcomp-ssreflect" {(>= "2.1.0" & < "2.4~") | (= "dev")}
21-
"coq-mathcomp-algebra"
21+
"coq-mathcomp-algebra"
2222
"coq-hierarchy-builder" {>= "1.5.0"}
2323
"coq-fourcolor-reals" {= version}
2424
]

‎released/packages/coq-hierarchy-builder/coq-hierarchy-builder.1.8.1/opam

+33
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
opam-version: "2.0"
2+
synopsis:
3+
"High level commands to declare and evolve a hierarchy based on packed classes"
4+
description: """\
5+
Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these
6+
hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder
7+
and abbreviation that let the hierarchy developer describe an actual interface for their library.
8+
Behind that interface the developer can provide appropriate code to ensure retro compatibility."""
9+
maintainer: "Enrico Tassi <[email protected]>"
10+
authors: ["Cyril Cohen" "Kazuhiko Sakaguchi" "Enrico Tassi"]
11+
license: "MIT"
12+
tags: "logpath:HB"
13+
homepage: "https://github.com/math-comp/hierarchy-builder"
14+
bug-reports: "https://github.com/math-comp/hierarchy-builder/issues"
15+
depends: [
16+
("coq" {>= "8.18" & < "8.20~"} & "coq-elpi" {>= "2.0"}
17+
| "coq" {>= "8.20" | = "dev"} & "coq-elpi" {(>= "2.4" < "2.5") | = "dev"})
18+
]
19+
conflicts: ["coq-hierarchy-builder-shim"]
20+
build: [
21+
[make "build"]
22+
[make "test-suite"] {with-test}
23+
]
24+
install: [make "install"]
25+
dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
26+
url {
27+
src:
28+
"https://github.com/math-comp/hierarchy-builder/releases/download/v1.8.1/hierarchy-builder-1.8.1.tar.gz"
29+
checksum: [
30+
"md5=faa5a113d28f52b680b7f7b44a090fb9"
31+
"sha512=244dab5c4a8f62f4c2fd506ebe7822d68405d1a2c1bae35664028f27ca7776b60bff7446ef232b841335357a24c4d502815c01e8d11ced3318f0d271990f77e6"
32+
]
33+
}

‎released/packages/coq-iris/coq-iris.4.3.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ tags: [
2727
]
2828

2929
depends: [
30-
"coq" { (>= "8.19" & < "8.21~") | (= "dev") }
30+
"coq" { (>= "8.19" & < "9.1~") | (= "dev") }
3131
"coq-stdpp" { (= "1.11.0") | (= "dev") }
3232
]
3333

‎released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.4/opam

+43
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
4+
homepage: "https://github.com/math-comp/algebra-tactics"
5+
dev-repo: "git+https://github.com/math-comp/algebra-tactics.git"
6+
bug-reports: "https://github.com/math-comp/algebra-tactics/issues"
7+
license: "CECILL-B"
8+
9+
synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components"
10+
description: """
11+
This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
12+
the Mathematical Components library. These tactics use the algebraic
13+
structures defined in the MathComp library and their canonical instances for
14+
the instance resolution, and do not require any special instance declaration,
15+
like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics
16+
works with any instance of the respective structure, including concrete
17+
instances declared through Hierarchy Builder, abstract instances, and mixed
18+
concrete and abstract instances, e.g., `int * R` where `R` is an abstract
19+
commutative ring. Another key feature of Algebra Tactics is that they
20+
automatically push down ring morphisms and additive functions to leaves of
21+
ring/field expressions before applying the proof procedures."""
22+
23+
build: [make "-j%{jobs}%"]
24+
install: [make "install"]
25+
depends: [
26+
"coq" {>= "8.16" & < "9.1~"}
27+
"coq-mathcomp-ssreflect" {>= "2.0" & < "2.4~"}
28+
"coq-mathcomp-algebra"
29+
"coq-mathcomp-zify" {>= "1.5.0"}
30+
"coq-elpi" {>= "1.15.0" & != "1.17.0"}
31+
]
32+
33+
tags: [
34+
"logpath:mathcomp.algebra_tactics"
35+
]
36+
authors: [
37+
"Kazuhiko Sakaguchi"
38+
"Pierre Roux"
39+
]
40+
url {
41+
src: "https://github.com/math-comp/algebra-tactics/archive/refs/tags/1.2.3.tar.gz"
42+
checksum: "sha256=a556875e9ed8db1f77474de77c6ae56142c4477a9f11438d70e1f346c90001e4"
43+
}

‎released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.2/opam

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
2+
opam-version: "2.0"
3+
maintainer: "Cyril Cohen <[email protected]>"
4+
5+
homepage: "https://github.com/math-comp/bigenough"
6+
dev-repo: "git+https://github.com/math-comp/bigenough.git"
7+
bug-reports: "https://github.com/math-comp/bigenough/issues"
8+
license: "CeCILL-B"
9+
10+
synopsis: "A small library to do epsilon - N reasoning"
11+
description: """
12+
The package contains a package to reasoning with big enough objects
13+
(mostly natural numbers). This package is essentially for backward
14+
compatibility purposes as `bigenough` will be subsumed by the near
15+
tactics. The formalization is based on the Mathematical Components
16+
library."""
17+
18+
build: [make "-j%{jobs}%"]
19+
install: [make "install"]
20+
depends: [
21+
"coq" {(>= "8.10" & < "9.1~") | (= "dev")}
22+
"coq-mathcomp-ssreflect" {>= "1.6"}
23+
]
24+
25+
tags: [
26+
"keyword:bigenough"
27+
"keyword:asymptotic reasonning"
28+
"keyword:small scale reflection"
29+
"keyword:mathematical components"
30+
"logpath:mathcomp.bigenough"
31+
]
32+
authors: [
33+
"Cyril Cohen"
34+
]
35+
36+
url {
37+
src: "https://github.com/math-comp/bigenough/archive/1.0.2.tar.gz"
38+
checksum: "sha512=faaa56c7db5b00a3e3b1a60dc0b3623d8ef5bcf7d08a228df2184e79a124f9dbd4917b2c24cef0bd9ad98b3dd7aae331d5fbe6dd2d154b80fdc108d8dc828b29"
39+
}

‎released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.8.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
1414
build: [make "-C" "classical" "-j%{jobs}%"]
1515
install: [make "-C" "classical" "install"]
1616
depends: [
17-
"coq" { (>= "8.19" & < "8.21~") | (= "dev") }
17+
"coq" { (>= "8.19" & < "9.1~") | (= "dev") }
1818
"coq-mathcomp-ssreflect" { (>= "2.1.0") }
1919
"coq-mathcomp-fingroup"
2020
"coq-mathcomp-algebra"

‎released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.2.1.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ which will be used to subsume notations for finite sets, eventually."""
1717
build: [make "-j%{jobs}%"]
1818
install: [make "install"]
1919
depends: [
20-
"coq" { (>= "8.16" & < "8.21~") | (= "dev") }
20+
"coq" { (>= "8.16" & < "9.1~") | (= "dev") }
2121
"coq-mathcomp-ssreflect" { (>= "2.0.0" & < "2.4~") | (= "dev") }
2222
]
2323

‎released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.8.0/opam

+1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ the Coq proof-assistant using the Mathematical Components library and Stdlib."""
1414
build: [make "-C" "reals_stdlib" "-j%{jobs}%"]
1515
install: [make "-C" "reals_stdlib" "install"]
1616
depends: [
17+
"coq" {< "8.21~"}
1718
"coq-mathcomp-reals" { = version}
1819
]
1920

‎released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ license: "CECILL-B"
99
build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
1010
install: [ make "-C" "mathcomp/ssreflect" "install" ]
1111
depends: [
12-
"coq" {(>= "8.18" & < "8.21~") | (= "dev")}
12+
"coq" {(>= "8.18" & < "9.1~") | (= "dev")}
1313
# Please keep the "dev" above as it is required for the coq-dev Docker images
1414
"elpi" {>= "1.17.0"}
1515
"coq-hierarchy-builder" { >= "1.7.0"}

‎released/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.1.0.2/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ sorting with extended guarantees for acyclic graphs."""
1616
build: [make "-j%{jobs}%"]
1717
install: [make "install"]
1818
depends: [
19-
"coq" {>= "8.16" & < "8.21~"}
19+
"coq" {>= "8.16" & < "9.1~"}
2020
"coq-mathcomp-ssreflect" {>= "2.0"}
21-
"coq-mathcomp-fingroup"
21+
"coq-mathcomp-fingroup"
2222
"coq-hierarchy-builder" {>= "1.4.0"}
2323
]
2424

‎released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.5.0+2.0+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,9 @@ by extending the zify tactic."""
1515
build: [make "-j%{jobs}%"]
1616
install: [make "install"]
1717
depends: [
18-
"coq" {(>= "8.16" & < "8.21~")}
18+
"coq" {(>= "8.16" & < "9.1~")}
1919
"coq-mathcomp-ssreflect" {(>= "2.0" & < "2.4~")}
20-
"coq-mathcomp-algebra"
20+
"coq-mathcomp-algebra"
2121
]
2222

2323
tags: [

‎released/packages/coq-paco/coq-paco.4.2.2/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ license: "BSD-3-Clause"
1515
build: [make "-C" "src" "all" "-j%{jobs}%"]
1616
install: [make "-C" "src" "-f" "Makefile.coq" "install"]
1717
depends: [
18-
"coq" {>= "8.13" & < "8.21~"}
18+
"coq" {>= "8.13" & < "9.1~"}
1919
]
2020
tags: [
2121
"date:2024-12-31"

‎released/packages/coq-record-update/coq-record-update.0.3.4/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ simple typeclass that lists out the record fields."""
1616
build: [make "-j%{jobs}%" "NO_TEST=1"]
1717
install: [make "install"]
1818
depends: [
19-
"coq" {(>= "8.14" & < "8.21~") | (= "dev")}
19+
"coq" {(>= "8.14" & < "9.1~") | (= "dev")}
2020
]
2121

2222
tags: [

‎released/packages/coq-reglang/coq-reglang.1.2.1/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ decidability results and closure properties of regular languages."""
1818
build: [make "-j%{jobs}%"]
1919
install: [make "install"]
2020
depends: [
21-
"coq" {>= "8.16" & < "8.21"}
21+
"coq" {>= "8.16" & < "9.1~"}
2222
"coq-mathcomp-ssreflect" {>= "2.0" & < "2.4"}
2323
"coq-hierarchy-builder" {>= "1.4.0"}
2424
]

‎released/packages/coq-simple-io/coq-simple-io.1.10.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ depends: [
1313
"dune" {>= "3.7"}
1414
"ocaml" {>= "4.08.0"}
1515
"ocamlfind"
16-
"coq" {>= "8.12~" & < "8.21~"}
16+
"coq" {>= "8.12~" & < "9.1~"}
1717
"coq-ext-lib" {>= "0.10.0"}
1818
"ocamlbuild" {with-test & >= "0.9.0"}
1919
"cppo" {build & >= "1.6.8"}

‎released/packages/coq-stdpp/coq-stdpp.1.11.0/opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ tags: [
3333
]
3434

3535
depends: [
36-
"coq" { (>= "8.18" & < "8.21~") | (= "dev") }
36+
"coq" { (>= "8.18" & < "9.1~") | (= "dev") }
3737
]
3838

3939
build: ["./make-package" "stdpp" "-j%{jobs}%"]

0 commit comments

Comments
 (0)