[CI] Add a job to check the subcomponent structure

Ensure that subcomponents build with the declared dependencies

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

@@ -5950,6 +5950,58 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
         --argstr job "stdlib-refman-html"
+  stdlib-subcomponents:
+    needs:
+    - coq
+    runs-on: ubuntu-latest
+    steps:
+    - name: Determine which commit to initially checkout
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha\
+        \ }}\" >> $GITHUB_ENV\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.target_commit }}
+    - name: Determine which commit to test
+      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
+        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
+        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
+        \ | cut -f1)\n  mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
+        \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
+        \  if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n    echo\
+        \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
+        \  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
+    - name: Git checkout
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+        ref: ${{ env.tested_commit }}
+    - name: Cachix install
+      uses: cachix/install-nix-action@v27
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq-community
+      uses: cachix/cachix-action@v15
+      with:
+        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
+        extraPullNames: coq, math-comp
+        name: coq-community
+    - id: stepCheck
+      name: Checking presence of CI target stdlib-subcomponents
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-master\" --argstr job \"stdlib-subcomponents\" \\\n   --dry-run\
+        \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
+        \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
+        --argstr job "coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: Building/fetching current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
+        --argstr job "stdlib-subcomponents"
   stdlib-test:
     needs:
     - coq

.nix/config.nix

@@ -200,6 +200,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       stdlib-html.job = true;
       stdlib-refman-html.job = true;
       stdlib-test.job = true;
+      stdlib-subcomponents.job = true;
       coq-elpi.override.version = "proux01:stdlib_repo";
       coq-elpi-test.override.version = "proux01:stdlib_repo";
       metacoq.override.version = "proux01:stdlib_repo";

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

@@ -0,0 +1,70 @@
+# CI job to test that we don't break the subcomponent structure of the stdlib,
+# as described in the graph doc/stdlib/depends
+
+{ stdlib, coqPackages }:
+
+let
+  # stdlib subcomponents with their dependencies
+  # when editing this, ensure to keep doc/stdlib/depends in sync
+  components = {
+    "logic" = [ ];
+    "relations" = [ ];
+    "program" = [ "logic" ];
+    "classes" = [ "program" "relations" ];
+    "bool" = [ "classes" ];
+    "structures" = [ "bool" ];
+    "arith-base" = [ "structures" ];
+    "positive" = [ "arith-base" ];
+    "narith" = [ "positive" ];
+    "zarith-base" = [ "narith" ];
+    "list" = [ "arith-base" ];
+    "ring" = [ "zarith-base" "list" ];
+    "arith" = [ "ring" ];
+    "string" = [ "arith" ];
+    "lia" = [ "arith" ];
+    "zarith" = [ "lia" ];
+    "qarith-base" = [ "ring" ];
+    "field" = [ "qarith-base" "zarith" ];
+    "lqa" = [ "field" ];
+    "qarith" = [ "field" ];
+    "nsatz" = [ "zarith" "qarith-base" ];
+    "classical-logic" = [ "arith" ];
+    "sets" = [ "classical-logic" ];
+    "vectors" = [ "list" ];
+    "sorting" = [ "lia" "sets" "vectors" ];
+    "orders-ex" = [ "string" "sorting" ];
+    "unicode" = [ ];
+    "primitive-int" = [ "unicode" "zarith" ];
+    "primitive-floats" = [ "primitive-int" ];
+    "primitive-array" = [ "primitive-int" ];
+    "primitive-string" = [ "primitive-int" "orders-ex" ];
+    "reals" = [ "nsatz" "lqa" "qarith" "classical-logic" "vectors" ];
+    "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
+    "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
+    "funind" = [ "arith-base" ];
+    "wellfounded" = [ "list" ];
+    "streams" = [ "logic" ];
+    "rtauto" = [ "positive" "list" ];
+    "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "wellfounded" "streams" ];
+    "all" = [ "compat" ];
+  };
+
+  stdlib_ = component: let
+    pname = "stdlib-${component}";
+    stdlib-deps = map stdlib_ components.${component};
+    in coqPackages.lib.overrideCoqDerivation ({
+      inherit pname;
+      propagatedBuildInputs = stdlib-deps;
+      useDune = false;
+    } // (if component != "all" then {
+      buildFlags = [ "build-${component}" ];
+      installTargets = [ "install-${component}" ];
+    } else {
+      buildPhase = ''
+        echo "nothing left to build"
+      '';
+      installPhase = ''
+        echo "nothing left to install"
+      '';
+    })) stdlib;
+in stdlib_ "all"

doc/stdlib/depends

@@ -1,4 +1,6 @@
 # this has been mostly automatically generated by dev/tools/make-depends.sh
+# when editing this, ensure to keep .nix/coq-overlays/stdlib-subcomponents
+# in sync
 digraph stdlib_deps {
 	node [color=lightblue,
 		shape=ellipse,