diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-coq-master.yml index acb7b7b86d..e3f64cd989 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.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 diff --git a/.nix/config.nix b/.nix/config.nix index bf1623d0a8..3ddc4ad0ae 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -200,6 +200,7 @@ with builtins; with (import {}).lib; stdlib-html.job = true; stdlib-refman-html.job = true; stdlib-test.job = true; + stdlib-subcomponents.job = true; compcert.override.version = "proux01:stdlib_repo"; coq-elpi.override.version = "proux01:stdlib_repo"; coq-elpi-test.override.version = "proux01:stdlib_repo"; diff --git a/.nix/coq-overlays/stdlib-subcomponents/default.nix b/.nix/coq-overlays/stdlib-subcomponents/default.nix new file mode 100644 index 0000000000..53d89ab1f7 --- /dev/null +++ b/.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" diff --git a/doc/stdlib/depends b/doc/stdlib/depends index f6d0a63d1a..78bbad9910 100644 --- a/doc/stdlib/depends +++ b/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,