Skip to content

Commit 8f76b3c

Browse files
garesgares
committed
Merge branch 'master' into coq-master+1.1.0
2 parents 5e9a0bd + 6c58bab commit 8f76b3c

File tree

106 files changed

+5505
-2816
lines changed

Some content is hidden

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

106 files changed

+5505
-2816
lines changed

‎.github/workflows/main.yml‎

Lines changed: 36 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# This is a basic workflow to help you get started with Actions
22

3-
name: CI
3+
name: docker CI
44

55
# Controls when the action will run. Triggers the workflow on push or pull request
66
# events but only for the master branch
@@ -11,21 +11,15 @@ on:
1111
branches: [ master ]
1212

1313
jobs:
14-
nix:
15-
runs-on: ubuntu-latest
16-
17-
steps:
18-
- uses: actions/checkout@v2
19-
- uses: cachix/install-nix-action@v10
20-
- run: nix-build
21-
2214
opam:
2315
runs-on: ubuntu-latest
2416
strategy:
17+
fail-fast: false
2518
matrix:
2619
coq_version:
2720
- '8.11'
2821
- '8.12'
22+
- '8.13'
2923
ocaml_version:
3024
- 'minimal'
3125
steps:
@@ -35,3 +29,36 @@ jobs:
3529
opam_file: './coq-hierarchy-builder.opam'
3630
coq_version: ${{ matrix.coq_version }}
3731
ocaml_version: ${{ matrix.ocaml_version }}
32+
33+
plan-B:
34+
runs-on: ubuntu-latest
35+
steps:
36+
- uses: actions/checkout@v2
37+
- uses: coq-community/docker-coq-action@v1
38+
with:
39+
opam_file: './coq-hierarchy-builder.opam'
40+
coq_version: '8.13'
41+
ocaml_version: 'minimal'
42+
script: |
43+
mkdir /home/coq/workspace
44+
cp -ra . /home/coq/workspace
45+
cd /home/coq/workspace
46+
opam install ./coq-hierarchy-builder.opam
47+
sed -i.bak "s/-Q . HB//" _CoqProject.test-suite
48+
# This is what a user does to cut HB loose
49+
export COQ_ELPI_ATTRIBUTES="hb(log(raw))"
50+
make test-suite -j2
51+
wc -l `find . -name \*.v`
52+
coq.hb patch `find . -name \*.v`
53+
wc -l `find . -name \*.v`
54+
if git diff --quiet; then echo "No patch!"; exit 1; fi
55+
make clean
56+
opam remove coq-hierarchy-builder
57+
opam install ./coq-hierarchy-builder-shim.opam
58+
# Does it work?
59+
make test-suite -j2
60+
# We also test the reset facility works (we rebuild hb locally)
61+
make coq.hb
62+
./coq.hb reset `find . -name \*.v`
63+
mv _CoqProject.test-suite.bak _CoqProject.test-suite
64+
git diff --exit-code

‎.github/workflows/nix.yml‎

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
# This is a basic workflow to help you get started with Actions
2+
3+
name: nix CI
4+
5+
# Controls when the action will run. Triggers the workflow on push or pull request
6+
# events but only for the master branch
7+
on:
8+
push:
9+
branches: [ master ]
10+
pull_request:
11+
branches: [ master ]
12+
13+
jobs:
14+
hb:
15+
runs-on: ubuntu-latest
16+
strategy:
17+
fail-fast: false
18+
matrix:
19+
bundle: [ "coq-8.13", "coq-8.12", "coq-8.11" ]
20+
steps:
21+
- name: Cachix install
22+
uses: cachix/install-nix-action@v12
23+
- name: Cachix setup
24+
uses: cachix/cachix-action@v8
25+
with:
26+
name: math-comp
27+
extraPullNames: coq
28+
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
29+
- name: Git checkout
30+
uses: actions/checkout@v2
31+
with:
32+
fetch-depth: 0
33+
- name: Dependencies
34+
run: nix-build --argstr job "_deps" --argstr bundle ${{ matrix.bundle }}
35+
- name: Build HB
36+
run: nix-build --argstr job "hierarchy-builder" --argstr bundle ${{ matrix.bundle }}
37+
38+
hb-shim:
39+
runs-on: ubuntu-latest
40+
strategy:
41+
matrix:
42+
bundle: [ "coq-8.13" ]
43+
steps:
44+
- name: Cachix install
45+
uses: cachix/install-nix-action@v12
46+
- name: Cachix setup
47+
uses: cachix/cachix-action@v8
48+
with:
49+
name: math-comp
50+
extraPullNames: coq
51+
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
52+
- name: Git checkout
53+
uses: actions/checkout@v2
54+
with:
55+
fetch-depth: 0
56+
- name: Dependencies
57+
run: nix-build --argstr job "_deps" --argstr bundle ${{ matrix.bundle }}
58+
- name: Build HB shim
59+
run: nix-build --argstr job "hierarchy-builder-shim" --argstr bundle ${{ matrix.bundle }}
60+
61+
mathcomp:
62+
runs-on: ubuntu-latest
63+
needs: hb
64+
if: always()
65+
strategy:
66+
fail-fast: false
67+
matrix:
68+
bundle: [ "coq-8.13", "coq-8.12", "coq-8.11" ]
69+
steps:
70+
- name: Cachix install
71+
uses: cachix/install-nix-action@v12
72+
- name: Cachix setup
73+
uses: cachix/cachix-action@v8
74+
with:
75+
name: math-comp
76+
extraPullNames: coq
77+
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
78+
- name: Git checkout
79+
uses: actions/checkout@v2
80+
with:
81+
fetch-depth: 0
82+
- name: Dependencies
83+
run: nix-build --argstr job "_deps" --argstr bundle ${{ matrix.bundle }}
84+
- name: Hiearchy builder
85+
run: nix-build --argstr job "hierarchy-builder" --argstr bundle ${{ matrix.bundle }}
86+
- name: Build mathcomp on HB
87+
run: nix-build --argstr job "mathcomp-single" --argstr bundle ${{ matrix.bundle }}
88+
89+
mathcomp-planB-src:
90+
runs-on: ubuntu-latest
91+
needs: hb
92+
if: always()
93+
strategy:
94+
matrix:
95+
bundle: [ "coq-8.13" ]
96+
steps:
97+
- name: Cachix install
98+
uses: cachix/install-nix-action@v12
99+
- name: Cachix setup
100+
uses: cachix/cachix-action@v8
101+
with:
102+
name: math-comp
103+
extraPullNames: coq
104+
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
105+
- name: Git checkout
106+
uses: actions/checkout@v2
107+
with:
108+
fetch-depth: 0
109+
- name: Dependencies
110+
run: nix-build --argstr job "_deps" --argstr bundle ${{ matrix.bundle }}
111+
- name: Hiearchy builder
112+
run: nix-build --argstr job "hierarchy-builder" --argstr bundle ${{ matrix.bundle }}
113+
- name: Build planB sources
114+
run: nix-build --argstr job "mathcomp-single-planB-src" --argstr bundle ${{ matrix.bundle }}
115+
- name: Save planB sources as a GH artifact
116+
uses: actions/upload-artifact@v2
117+
with:
118+
name: planB-sources
119+
path: |
120+
result/mathcomp
121+
! result/**/*.vo
122+
123+
mathcomp-planB:
124+
runs-on: ubuntu-latest
125+
if: always()
126+
strategy:
127+
matrix:
128+
bundle: [ "coq-8.13" ]
129+
needs:
130+
- hb-shim
131+
- mathcomp-planB-src
132+
steps:
133+
- name: Cachix install
134+
uses: cachix/install-nix-action@v12
135+
- name: Cachix setup
136+
uses: cachix/cachix-action@v8
137+
with:
138+
name: math-comp
139+
extraPullNames: coq
140+
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
141+
- name: Git checkout
142+
uses: actions/checkout@v2
143+
with:
144+
fetch-depth: 0
145+
- name: Dependencies
146+
run: nix-build --argstr job "_deps" --argstr bundle ${{ matrix.bundle }}
147+
- name: Hiearchy builder
148+
run: nix-build --argstr job "hierarchy-builder-shim" --argstr bundle ${{ matrix.bundle }}
149+
- name: Build plan B sources
150+
run: nix-build --argstr job "mathcomp-single-planB-src" --argstr bundle ${{ matrix.bundle }}
151+
- name: Build plan B
152+
run: nix-build --argstr job "mathcomp-single-planB" --argstr bundle ${{ matrix.bundle }}

‎.gitignore‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,13 @@ nra.cache
3434
Makefile.coq
3535
Makefile.coq.conf
3636
.coqdeps.d
37+
Makefile.test-suite.coq
38+
Makefile.test-suite.coq.conf
39+
.coqdeps.test-suite
40+
*.v.hb
41+
*.v.hb.old
42+
coq.hb
43+
HB/common/log.compat.elpi
3744

3845
_minted-*
3946
*.aux
@@ -48,3 +55,5 @@ _minted-*
4855
*.blg
4956
*.fdb_latexmk
5057
*.vtc
58+
59+
*.dot

‎.nix/config.nix‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
{
2+
format = "1.0.0";
3+
attribute = "hierarchy-builder";
4+
default-bundle = "coq-8.13";
5+
bundles = let common = {
6+
mathcomp.override.version = "hierarchy-builder";
7+
mathcomp.job = false;
8+
mathcomp-single.job = true;
9+
}; in {
10+
"coq-8.13".coqPackages = {
11+
coq.override.version = "8.13";
12+
hierarchy-builder-shim.job = true;
13+
mathcomp-single-planB-src.job = true;
14+
mathcomp-single-planB.job = true;
15+
} // common;
16+
"coq-8.12".coqPackages = {
17+
coq.override.version = "8.12";
18+
coq-elpi.override.version = "v1.8";
19+
20+
} // common;
21+
"coq-8.11".coqPackages = {
22+
coq.override.version = "8.11";
23+
coq-elpi.override.version = "v1.6";
24+
25+
} // common;
26+
};
27+
}

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
"751410ed320b348e8d066b1b939db0eab40f3a93"

‎.nix/coq-overlays/coq-elpi/default.nix‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
{ lib, mkCoqDerivation, which, coq, version ? null }:
2+
3+
with builtins; with lib; let
4+
elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
5+
{ case = "8.11"; out = { version = "1.11.4"; };}
6+
{ case = "8.12"; out = { version = "1.12.0"; };}
7+
{ case = "8.13"; out = { version = "1.13.0"; };}
8+
] {});
9+
in mkCoqDerivation {
10+
pname = "elpi";
11+
repo = "coq-elpi";
12+
owner = "LPCIC";
13+
inherit version;
14+
defaultVersion = lib.switch coq.coq-version [
15+
{ case = "8.13"; out = "1.9.5"; }
16+
{ case = "8.12"; out = "1.8.2_8.12"; }
17+
{ case = "8.11"; out = "1.6.2_8.11"; }
18+
] null;
19+
release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
20+
release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
21+
release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
22+
release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
23+
release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
24+
release."1.8.2_8.12".version = "1.8.2";
25+
release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
26+
release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
27+
release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
28+
release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
29+
release."1.6.2_8.11".version = "1.6.2";
30+
release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
31+
release."1.6.1_8.11".version = "1.6.1";
32+
release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
33+
release."1.6.0_8.11".version = "1.6.0";
34+
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
35+
releaseRev = v: "v${v}";
36+
37+
nativeBuildInputs = [ which ];
38+
mlPlugin = true;
39+
extraBuildInputs = [ elpi ];
40+
41+
meta = {
42+
description = "Coq plugin embedding ELPI.";
43+
maintainers = [ maintainers.cohencyril ];
44+
license = licenses.lgpl21;
45+
};
46+
}

‎.nix/coq-overlays/hierarchy-builder-shim/default.nix‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{ hierarchy-builder }: hierarchy-builder.override { shim = true; }

‎.nix/coq-overlays/hierarchy-builder/default.nix‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
{ lib, mkCoqDerivation, which, coq, coq-elpi,
2+
version ? null, shim ? false }:
3+
4+
let installFlags =
5+
[ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ];
6+
in
7+
with lib; mkCoqDerivation ({
8+
pname = "hierarchy-builder" + optionalString shim "-shim";
9+
repo = "hierarchy-builder";
10+
owner = "math-comp";
11+
inherit version;
12+
defaultVersion = with versions; switch coq.coq-version [
13+
{ case = isGe "8.12"; out = "1.0.0"; }
14+
{ case = range "8.11" "8.12"; out = "0.10.0"; }
15+
] null;
16+
release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
17+
release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
18+
releaseRev = v: "v${v}";
19+
20+
nativeBuildInputs = [ which ];
21+
propagatedBuildInputs = [ coq-elpi coq.ocaml ];
22+
inherit installFlags;
23+
24+
meta = {
25+
description = "Coq plugin embedding ELPI.";
26+
maintainers = [ maintainers.cohencyril ];
27+
license = licenses.lgpl21;
28+
};
29+
}
30+
// optionalAttrs shim {
31+
buildFlags = [ "-C shim" ];
32+
installFlags = installFlags ++ [ "-C shim" ];
33+
})

‎.nix/coq-overlays/mathcomp-single-planB-src/default.nix‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{ mathcomp, coq, coq-elpi, hierarchy-builder, version ? null }:
2+
(mathcomp.override {single = true;}).overrideAttrs (old: {
3+
name = "coq${coq.coq-version}-mathcomp-planB-src";
4+
buildPhase = ''
5+
COQ_ELPI_ATTRIBUTES='hb(log(raw))' \
6+
make -j$NIX_BUILD_CORES -C mathcomp
7+
coq.hb patch `find . -name \*.v`
8+
make -C mathcomp clean
9+
'';
10+
propagatedBuildInputs = old.propagatedBuildInputs ++
11+
[ coq-elpi hierarchy-builder ];
12+
installPhase = ''
13+
mkdir -p $out
14+
cp -r . $out
15+
'';
16+
})

‎.nix/coq-overlays/mathcomp-single-planB/default.nix‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{ mathcomp, coq, coq-elpi, hierarchy-builder-shim,
2+
mathcomp-single-planB-src }:
3+
(mathcomp.override {single = true;}).overrideAttrs (old: {
4+
src = mathcomp-single-planB-src;
5+
name = "coq${coq.coq-version}-mathcomp-planB";
6+
propagatedBuildInputs = old.propagatedBuildInputs ++
7+
[ coq-elpi hierarchy-builder-shim ];
8+
patchPhase = ''
9+
ulimit -s 81960
10+
'';
11+
})

0 commit comments

Comments
 (0)