Skip to content

Commit 2181112

Browse files
proux01proux01
committed
[CI] Add a job to check the subcomponent structure
Ensure that subcomponents build with the declared dependencies
1 parent 5c1cd56 commit 2181112

File tree

4 files changed

+125
-0
lines changed

4 files changed

+125
-0
lines changed

‎.github/workflows/nix-action-coq-master.yml‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5950,6 +5950,58 @@ jobs:
59505950
name: Building/fetching current CI target
59515951
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
59525952
--argstr job "stdlib-refman-html"
5953+
stdlib-subcomponents:
5954+
needs:
5955+
- coq
5956+
runs-on: ubuntu-latest
5957+
steps:
5958+
- name: Determine which commit to initially checkout
5959+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
5960+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
5961+
\ }}\" >> $GITHUB_ENV\nfi\n"
5962+
- name: Git checkout
5963+
uses: actions/checkout@v4
5964+
with:
5965+
fetch-depth: 0
5966+
ref: ${{ env.target_commit }}
5967+
- name: Determine which commit to test
5968+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
5969+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
5970+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
5971+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
5972+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
5973+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
5974+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
5975+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
5976+
- name: Git checkout
5977+
uses: actions/checkout@v4
5978+
with:
5979+
fetch-depth: 0
5980+
ref: ${{ env.tested_commit }}
5981+
- name: Cachix install
5982+
uses: cachix/install-nix-action@v27
5983+
with:
5984+
nix_path: nixpkgs=channel:nixpkgs-unstable
5985+
- name: Cachix setup coq-community
5986+
uses: cachix/cachix-action@v15
5987+
with:
5988+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
5989+
extraPullNames: coq, math-comp
5990+
name: coq-community
5991+
- id: stepCheck
5992+
name: Checking presence of CI target stdlib-subcomponents
5993+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
5994+
\ bundle \"coq-master\" --argstr job \"stdlib-subcomponents\" \\\n --dry-run\
5995+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
5996+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
5997+
- if: steps.stepCheck.outputs.status == 'built'
5998+
name: 'Building/fetching previous CI target: coq'
5999+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
6000+
--argstr job "coq"
6001+
- if: steps.stepCheck.outputs.status == 'built'
6002+
name: Building/fetching current CI target
6003+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
6004+
--argstr job "stdlib-subcomponents"
59536005
stdlib-test:
59546006
needs:
59556007
- coq

‎.nix/config.nix‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -200,6 +200,7 @@ with builtins; with (import <nixpkgs> {}).lib;
200200
stdlib-html.job = true;
201201
stdlib-refman-html.job = true;
202202
stdlib-test.job = true;
203+
stdlib-subcomponents.job = true;
203204
coq-elpi.override.version = "proux01:stdlib_repo";
204205
coq-elpi-test.override.version = "proux01:stdlib_repo";
205206
coq-tools.override.version = "proux01:stdlib_repo";

‎.nix/coq-overlays/stdlib-subcomponents/default.nix‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
# CI job to test that we don't break the subcomponent structure of the stdlib,
2+
# as described in the graph doc/stdlib/depends
3+
4+
{ stdlib, coqPackages }:
5+
6+
let
7+
# stdlib subcomponents with their dependencies
8+
# when editing this, ensure to keep doc/stdlib/depends in sync
9+
components = {
10+
"logic" = [ ];
11+
"relations" = [ ];
12+
"program" = [ "logic" ];
13+
"classes" = [ "program" "relations" ];
14+
"bool" = [ "classes" ];
15+
"structures" = [ "bool" ];
16+
"arith-base" = [ "structures" ];
17+
"positive" = [ "arith-base" ];
18+
"narith" = [ "positive" ];
19+
"zarith-base" = [ "narith" ];
20+
"list" = [ "arith-base" ];
21+
"ring" = [ "zarith-base" "list" ];
22+
"arith" = [ "ring" ];
23+
"string" = [ "arith" ];
24+
"lia" = [ "arith" ];
25+
"zarith" = [ "lia" ];
26+
"qarith-base" = [ "ring" ];
27+
"field" = [ "qarith-base" "zarith" ];
28+
"lqa" = [ "field" ];
29+
"qarith" = [ "field" ];
30+
"nsatz" = [ "zarith" "qarith-base" ];
31+
"classical-logic" = [ "arith" ];
32+
"sets" = [ "classical-logic" ];
33+
"vectors" = [ "list" ];
34+
"sorting" = [ "lia" "sets" "vectors" ];
35+
"orders-ex" = [ "string" "sorting" ];
36+
"unicode" = [ ];
37+
"primitive-int" = [ "unicode" "zarith" ];
38+
"primitive-floats" = [ "primitive-int" ];
39+
"primitive-array" = [ "primitive-int" ];
40+
"primitive-string" = [ "primitive-int" "orders-ex" ];
41+
"reals" = [ "nsatz" "lqa" "qarith" "classical-logic" "vectors" ];
42+
"fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
43+
"extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
44+
"funind" = [ "arith-base" ];
45+
"wellfounded" = [ "list" ];
46+
"streams" = [ "logic" ];
47+
"rtauto" = [ "positive" "list" ];
48+
"compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "wellfounded" "streams" ];
49+
"all" = [ "compat" ];
50+
};
51+
52+
stdlib_ = component: let
53+
pname = "stdlib-${component}";
54+
stdlib-deps = map stdlib_ components.${component};
55+
in coqPackages.lib.overrideCoqDerivation ({
56+
inherit pname;
57+
propagatedBuildInputs = stdlib-deps;
58+
useDune = false;
59+
} // (if component != "all" then {
60+
buildFlags = [ "build-${component}" ];
61+
installTargets = [ "install-${component}" ];
62+
} else {
63+
buildPhase = ''
64+
echo "nothing left to build"
65+
'';
66+
installPhase = ''
67+
echo "nothing left to install"
68+
'';
69+
})) stdlib;
70+
in stdlib_ "all"

‎doc/stdlib/depends‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
# this has been mostly automatically generated by dev/tools/make-depends.sh
2+
# when editing this, ensure to keep .nix/coq-overlays/stdlib-subcomponents
3+
# in sync
24
digraph stdlib_deps {
35
node [color=lightblue,
46
shape=ellipse,

0 commit comments

Comments
 (0)