Skip to content

Commit 61303be

Browse files
therythery
authored
Merge pull request #9 from coq-community/split-packages
split into several packages
2 parents 2005430 + 1fa12fc commit 61303be

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+394
-233
lines changed

‎.github/workflows/docker-action.yml

Lines changed: 54 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
# This file was generated from `meta.yml`, please do not edit manually.
2-
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
31
name: Docker CI
42

53
on:
@@ -37,8 +35,61 @@ jobs:
3735
- uses: actions/checkout@v2
3836
- uses: coq-community/docker-coq-action@v1
3937
with:
40-
opam_file: 'coq-gaia.opam'
4138
custom_image: ${{ matrix.image }}
39+
custom_script: |
40+
{{before_install}}
41+
startGroup "Build gaia-theory-of-sets dependencies"
42+
opam pin add -n -y -k path coq-gaia-theory-of-sets .
43+
opam update -y
44+
opam install -y -j 2 coq-gaia-theory-of-sets --deps-only
45+
endGroup
46+
startGroup "Build gaia-theory-of-sets"
47+
opam install -y -v -j 2 coq-gaia-theory-of-sets
48+
opam list
49+
endGroup
50+
startGroup "Build gaia-schutte dependencies"
51+
opam pin add -n -y -k path coq-gaia-schutte .
52+
opam update -y
53+
opam install -y -j 2 coq-gaia-schutte --deps-only
54+
endGroup
55+
startGroup "Build gaia-schutte"
56+
opam install -y -v -j 2 coq-gaia-schutte
57+
opam list
58+
endGroup
59+
startGroup "Build gaia-ordinals dependencies"
60+
opam pin add -n -y -k path coq-gaia-ordinals .
61+
opam update -y
62+
opam install -y -j 2 coq-gaia-ordinals --deps-only
63+
endGroup
64+
startGroup "Build gaia-ordinals"
65+
opam install -y -v -j 2 coq-gaia-ordinals
66+
opam list
67+
endGroup
68+
startGroup "Build gaia-numbers dependencies"
69+
opam pin add -n -y -k path coq-gaia-numbers .
70+
opam update -y
71+
opam install -y -j 2 coq-gaia-numbers --deps-only
72+
endGroup
73+
startGroup "Build gaia-numbers"
74+
opam install -y -v -j 2 coq-gaia-numbers
75+
opam list
76+
endGroup
77+
startGroup "Build gaia-stern dependencies"
78+
opam pin add -n -y -k path coq-gaia-stern .
79+
opam update -y
80+
opam install -y -j 2 coq-gaia-stern --deps-only
81+
endGroup
82+
startGroup "Build gaia-stern"
83+
opam install -y -v -j 2 coq-gaia-stern
84+
opam list
85+
endGroup
86+
startGroup "Uninstallation test"
87+
opam remove -y coq-gaia-stern
88+
opam remove -y coq-gaia-numbers
89+
opam remove -y coq-gaia-ordinals
90+
opam remove -y coq-gaia-schutte
91+
opam remove -y coq-gaia-theory-of-sets
92+
endGroup
4293
4394
# See also:
4495
# https://github.com/coq-community/docker-coq-action#readme

‎README.md

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -50,17 +50,9 @@ and number theory.
5050
- [Fibonacci numbers and the Stern-Brocot tree in Coq](https://hal.inria.fr/hal-01093589)
5151
- [Implementation of three types of ordinals in Coq](https://hal.inria.fr/hal-00911710)
5252

53-
## Building and installation instructions
53+
## Building and installation
5454

55-
The easiest way to install the latest released version of Gaia
56-
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
57-
58-
```shell
59-
opam repo add coq-released https://coq.inria.fr/opam/released
60-
opam install coq-gaia
61-
```
62-
63-
To instead build and install manually, do:
55+
To build and install manually, do:
6456

6557
``` shell
6658
git clone https://github.com/coq-community/gaia.git
@@ -69,7 +61,6 @@ make # or make -j <number-of-cores-on-your-machine>
6961
make install
7062
```
7163

72-
7364
## Documentation
7465

7566
Gaia stands for: Geometry, Algebra, Informatics and Applications.

‎_CoqProject

Lines changed: 45 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -1,49 +1,51 @@
1-
-R theories gaia
1+
-Q theories gaia
2+
23
-arg -w -arg -notation-overridden
34
-arg -w -arg -notation-incompatible-format
45
-arg -w -arg -ambiguous-paths
56
-arg -w -arg -deprecated-hint-without-locality
67
-arg -w -arg -deprecated-ident-entry
78
-arg -w -arg -deprecated-hint-rewrite-without-locality
8-
theories/fibm.v
9-
theories/sset1.v
10-
theories/sset10.v
11-
theories/sset11.v
12-
theories/sset12.v
13-
theories/sset13a.v
14-
theories/sset13b.v
15-
theories/sset13c.v
16-
theories/sset14.v
17-
theories/sset15.v
18-
theories/sset16a.v
19-
theories/sset16b.v
20-
theories/sset16c.v
21-
theories/sset17.v
22-
theories/sset18.v
23-
theories/sset19.v
24-
theories/sset2.v
25-
theories/sset2_aux.v
26-
theories/sset3.v
27-
theories/sset4.v
28-
theories/sset5.v
29-
theories/sset6.v
30-
theories/sset7.v
31-
theories/sset8.v
32-
theories/sset9.v
33-
theories/ssetc.v
34-
theories/ssete1.v
35-
theories/ssete10.v
36-
theories/ssete11.v
37-
theories/ssete2.v
38-
theories/ssete3.v
39-
theories/ssete4.v
40-
theories/ssete5.v
41-
theories/ssete6.v
42-
theories/ssete7.v
43-
theories/ssete8.v
44-
theories/ssete9.v
45-
theories/ssetq1.v
46-
theories/ssetq2.v
47-
theories/ssetr.v
48-
theories/ssetz.v
49-
theories/stern.v
9+
10+
theories/sets/sset1.v
11+
theories/sets/sset2_aux.v
12+
theories/sets/sset2.v
13+
theories/sets/sset3.v
14+
theories/sets/sset4.v
15+
theories/sets/sset5.v
16+
theories/sets/sset6.v
17+
theories/sets/sset7.v
18+
theories/sets/sset8.v
19+
theories/sets/sset9.v
20+
theories/sets/sset10.v
21+
theories/sets/sset18.v
22+
theories/sets/sset19.v
23+
theories/sets/ssete1.v
24+
theories/schutte/ssete9.v
25+
theories/ordinals/sset11.v
26+
theories/ordinals/sset12.v
27+
theories/ordinals/sset13a.v
28+
theories/ordinals/sset13b.v
29+
theories/ordinals/sset13c.v
30+
theories/ordinals/sset14.v
31+
theories/ordinals/sset15.v
32+
theories/ordinals/sset16a.v
33+
theories/ordinals/sset16b.v
34+
theories/ordinals/sset16c.v
35+
theories/ordinals/sset17.v
36+
theories/ordinals/ssete10.v
37+
theories/ordinals/ssete2.v
38+
theories/ordinals/ssete3.v
39+
theories/ordinals/ssete4.v
40+
theories/ordinals/ssete5.v
41+
theories/numbers/ssetc.v
42+
theories/numbers/ssetr.v
43+
theories/numbers/ssetz.v
44+
theories/numbers/ssetq1.v
45+
theories/numbers/ssetq2.v
46+
theories/numbers/ssete6.v
47+
theories/numbers/ssete7.v
48+
theories/numbers/ssete8.v
49+
theories/numbers/ssete11.v
50+
theories/stern/fibm.v
51+
theories/stern/stern.v

‎coq-gaia-numbers.opam

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
opam-version: "2.0"
2+
maintainer: "palmskog@gmail.com"
3+
version: "dev"
4+
5+
homepage: "https://github.com/coq-community/gaia"
6+
dev-repo: "git+https://github.com/coq-community/gaia.git"
7+
bug-reports: "https://github.com/coq-community/gaia/issues"
8+
license: "MIT"
9+
10+
synopsis: "Implementation of the sets of numbers Z, Q, and R following Bourbaki's Elements of Mathematics in Coq"
11+
description: """
12+
Implementation of the sets of numbers Z, Q, and R following N. Bourbaki's book series
13+
Elements of Mathematics in Coq using the Mathematical Components library."""
14+
15+
build: ["dune" "build" "-p" name "-j" jobs]
16+
depends: [
17+
"dune" {>= "2.5"}
18+
"coq" {(>= "8.10" & < "8.16~") | (= "dev")}
19+
"coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
20+
"coq-mathcomp-algebra"
21+
"coq-gaia-theory-of-sets" {= version}
22+
"coq-gaia-ordinals" {= version}
23+
]
24+
25+
tags: [
26+
"category:Mathematics/Arithmetic and Number Theory/Number theory"
27+
"keyword:integers"
28+
"keyword:rational numbers"
29+
"keyword:real numbers"
30+
"logpath:gaia.numbers"
31+
]
32+
authors: [
33+
"José Grimm"
34+
"Alban Quadrat"
35+
]

‎coq-gaia-ordinals.opam

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
opam-version: "2.0"
2+
maintainer: "palmskog@gmail.com"
3+
version: "dev"
4+
5+
homepage: "https://github.com/coq-community/gaia"
6+
dev-repo: "git+https://github.com/coq-community/gaia.git"
7+
bug-reports: "https://github.com/coq-community/gaia/issues"
8+
license: "MIT"
9+
10+
synopsis: "Implementation and properties of ordinals in Coq using Mathematical Components"
11+
description: """
12+
Implementation and properties of ordinals and cardinals in Coq using
13+
the Mathematical Components library."""
14+
15+
build: ["dune" "build" "-p" name "-j" jobs]
16+
depends: [
17+
"dune" {>= "2.5"}
18+
"coq" {(>= "8.10" & < "8.16~") | (= "dev")}
19+
"coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
20+
"coq-gaia-theory-of-sets" {= version}
21+
"coq-gaia-schutte" {= version}
22+
]
23+
24+
tags: [
25+
"category:Mathematics/Logic/Set theory"
26+
"category:Mathematics/Arithmetic and Number Theory/Number theory"
27+
"keyword:ordered sets"
28+
"keyword:ordinal arithmetic"
29+
"keyword:ordinals"
30+
"keyword:cardinal numbers"
31+
"logpath:gaia.ordinals"
32+
]
33+
authors: [
34+
"José Grimm"
35+
"Alban Quadrat"
36+
]

‎coq-gaia-schutte.opam

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
opam-version: "2.0"
2+
maintainer: "palmskog@gmail.com"
3+
version: "dev"
4+
5+
homepage: "https://github.com/coq-community/gaia"
6+
dev-repo: "git+https://github.com/coq-community/gaia.git"
7+
bug-reports: "https://github.com/coq-community/gaia/issues"
8+
license: "MIT"
9+
10+
synopsis: "Implementation of ordinals in Coq following Schütte and Ackermann"
11+
description: """
12+
Types for ordinal numbers in Coq using the Mathematical Components library,
13+
following the approaches of Schütte and Ackermann."""
14+
15+
build: ["dune" "build" "-p" name "-j" jobs]
16+
depends: [
17+
"dune" {>= "2.5"}
18+
"coq" {(>= "8.10" & < "8.16~") | (= "dev")}
19+
"coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
20+
]
21+
22+
tags: [
23+
"category:Mathematics/Arithmetic and Number Theory/Number theory"
24+
"keyword:ordinal arithmetic"
25+
"keyword:ordinals"
26+
"logpath:gaia.schutte"
27+
]
28+
authors: [
29+
"José Grimm"
30+
"Alban Quadrat"
31+
]

‎coq-gaia-stern.opam

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
opam-version: "2.0"
2+
maintainer: "palmskog@gmail.com"
3+
version: "dev"
4+
5+
homepage: "https://github.com/coq-community/gaia"
6+
dev-repo: "git+https://github.com/coq-community/gaia.git"
7+
bug-reports: "https://github.com/coq-community/gaia/issues"
8+
license: "MIT"
9+
10+
synopsis: "Properties of Fibonacci numbers and the Stern diatomic sequence in Coq"
11+
description: """
12+
Properties of Fibonacci numbers and the Stern diatomic sequence in Coq using the
13+
Mathematical Components library."""
14+
15+
build: ["dune" "build" "-p" name "-j" jobs]
16+
depends: [
17+
"dune" {>= "2.5"}
18+
"coq" {(>= "8.10" & < "8.16~") | (= "dev")}
19+
"coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
20+
"coq-mathcomp-algebra"
21+
]
22+
23+
tags: [
24+
"category:Mathematics/Arithmetic and Number Theory/Number theory"
25+
"keyword:stern-brocot"
26+
"keyword:fibonacci numbers"
27+
"logpath:gaia.stern"
28+
]
29+
authors: [
30+
"José Grimm"
31+
"Alban Quadrat"
32+
]

‎coq-gaia.opam renamed to ‎coq-gaia-theory-of-sets.opam

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,3 @@
1-
# This file was generated from `meta.yml`, please do not edit manually.
2-
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
3-
41
opam-version: "2.0"
52
maintainer: "palmskog@gmail.com"
63
version: "dev"
@@ -10,25 +7,23 @@ dev-repo: "git+https://github.com/coq-community/gaia.git"
107
bug-reports: "https://github.com/coq-community/gaia/issues"
118
license: "MIT"
129

13-
synopsis: "Implementation of books from Bourbaki's Elements of Mathematics in Coq"
10+
synopsis: "Implementation of the Theory of Sets from Bourbaki's Elements of Mathematics in Coq"
1411
description: """
15-
Implementation of books from N. Bourbaki's Elements of Mathematics
16-
in Coq using the Mathematical Components library, including set theory
17-
and number theory."""
12+
Implementation of the Theory of Sets following N. Bourbaki's book series
13+
Elements of Mathematics in Coq using the Mathematical Components library."""
1814

1915
build: ["dune" "build" "-p" name "-j" jobs]
2016
depends: [
2117
"dune" {>= "2.5"}
2218
"coq" {(>= "8.10" & < "8.16~") | (= "dev")}
2319
"coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
24-
"coq-mathcomp-algebra"
2520
]
2621

2722
tags: [
2823
"category:Mathematics/Logic/Set theory"
2924
"keyword:Bourbaki"
3025
"keyword:set theory"
31-
"logpath:gaia"
26+
"logpath:gaia.sets"
3227
]
3328
authors: [
3429
"José Grimm"

0 commit comments

Comments
 (0)