diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml new file mode 100644 index 0000000..25ddf58 --- /dev/null +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -0,0 +1,190 @@ +jobs: + bignums: + needs: + - rocq-core + - stdlib + 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@v30 + 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: stepGetDerivation + name: Getting derivation for current job (bignums) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "bignums" + rocq-core: + needs: [] + 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@v30 + 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: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "rocq-core" + stdlib: + needs: + - rocq-core + 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@v30 + 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: stepGetDerivation + name: Getting derivation for current job (stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"stdlib\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "stdlib" +name: Nix CI for bundle rocq-9.0 +on: + pull_request: + paths: + - .github/workflows/nix-action-rocq-9.0.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-rocq-9.0.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml new file mode 100644 index 0000000..0733231 --- /dev/null +++ b/.github/workflows/nix-action-rocq-master.yml @@ -0,0 +1,190 @@ +jobs: + bignums: + needs: + - rocq-core + - stdlib + 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@v30 + 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: stepGetDerivation + name: Getting derivation for current job (bignums) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || + (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" + --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" + --argstr job "bignums" + rocq-core: + needs: [] + 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@v30 + 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: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || + (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" + --argstr job "rocq-core" + stdlib: + needs: + - rocq-core + 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@v30 + 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: stepGetDerivation + name: Getting derivation for current job (stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"stdlib\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" + --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" + --argstr job "stdlib" +name: Nix CI for bundle rocq-master +on: + pull_request: + paths: + - .github/workflows/nix-action-rocq-master.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-rocq-master.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/fallback-config.nix b/.nix/fallback-config.nix index 346c174..5fe0a2e 100644 --- a/.nix/fallback-config.nix +++ b/.nix/fallback-config.nix @@ -25,6 +25,15 @@ with (import (import ./nixpkgs.nix) {}).lib; master = { coqPackages.coq.override.version = "master"; coqPackages.heq.job = false; + coqPackages.stdlib.job = false; + }; + "rocq-9.0" = { + isRocq = true; + rocqPackages.rocq-core.override.version = "9.0"; + }; + "rocq-master" = { + isRocq = true; + rocqPackages.rocq-core.override.version = "master"; }; }; diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix index 4668352..3dbeed3 100644 --- a/.nix/nixpkgs.nix +++ b/.nix/nixpkgs.nix @@ -1,4 +1,4 @@ fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/230646000795257116a112c24c06056210896333.tar.gz"; - sha256 = "15l41nbbrcrrjkn8ibgchavkjnmq3mzhcim1bbbg87v43dkyqm8d"; + url = "https://github.com/NixOS/nixpkgs/archive/15fdb273b8f523e0742dd2a898713833ac549296.tar.gz"; + sha256 = "12xaf75356yxm079jszb1mfw2b20z37v20mwawfsl757hirvjwf0"; } diff --git a/config-parser-1.0.0/ci.nix b/config-parser-1.0.0/ci.nix index eea5d3f..7d9fc1c 100644 --- a/config-parser-1.0.0/ci.nix +++ b/config-parser-1.0.0/ci.nix @@ -6,20 +6,25 @@ with builtins; with lib; (this-shell-pkg.propagatedBuildInputs or []); collect-job = v: if v?job && v.job != "_excluded" then [ v.job ] else []; collect-jobs = p: flatten (map collect-job (attrValues p)); - jobs = collect-jobs (bundle.coqPackages or {}); + bundle-packages = + if bundle ? isRocq then (bundle.rocqPackages or {}) + else (bundle.coqPackages or {}); + jobs = collect-jobs bundle-packages; excluded-pkg = n: v: if v?job && v.job == "_excluded" then [ n ] else []; - excluded = flatten (mapAttrsToList excluded-pkg - (bundle.coqPackages or {})); + excluded = flatten (mapAttrsToList excluded-pkg bundle-packages); main-job = v: if (v.main-job or false) && (v.job or "" != "_excluded") then [ v.job ] else []; main-jobs = p: flatten (map main-job (attrValues p)); - mains = main-jobs (bundle.coqPackages or {}); + mains = main-jobs bundle-packages; keep_ = tgt: job: (job != "_excluded") && (tgt == "_all" || tgt == job || (tgt == "_allJobs" && elem job jobs)); + pkgs-packages = + if bundle ? isRocq then pkgs.rocqPackages + else pkgs.coqPackages; subpkgs = job: let keep = n: v: keep_ job (bundle.coqPackages.${n}.job or n); in - attrValues (filterAttrs keep pkgs.coqPackages) + attrValues (filterAttrs keep pkgs-packages) ++ optionals (job == "_deps") dependencies; in { diff --git a/config-parser-1.0.0/default.nix b/config-parser-1.0.0/default.nix index 3125f2a..68ce887 100644 --- a/config-parser-1.0.0/default.nix +++ b/config-parser-1.0.0/default.nix @@ -18,28 +18,51 @@ let config = import ./normalize.nix { inherit (initial) src lib config nixpkgs; }; in with config; let + bundle-ppath = bundle: + let + rocq-coq-packages = + if bundle ? isRocq then "rocqPackages" else "coqPackages"; + path-to-attribute = config.path-to-attribute or [ rocq-coq-packages ]; + path-to-shell-attribute = + config.path-to-shell-attribute + or (config.path-to-attribute or [ "coqPackages" ]); + attribute = + if bundle ? isRocq && config.attribute == "coq" then "rocq-core" + else config.attribute; + shell-attribute = + if bundle ? isRocq && config.shell-attribute == "coq-shell" then "rocq-shell" + else config.shell-attribute; + in { + inherit rocq-coq-packages attribute shell-attribute; + # not configurable from config.nix: + ppath = path-to-attribute ++ [ attribute ]; + shell-ppath = path-to-shell-attribute ++ [ shell-attribute ]; + }; + # preparing bundles bundles = let mk-bundles = pre: x: setAttrByPath pre (mapAttrs (n: v: {override.version = v;}) x); in mapAttrs - (_: i: foldl recursiveUpdate {} [ - (setAttrByPath config.shell-ppath + (_: i: + let config-ppath = bundle-ppath i; in + foldl recursiveUpdate {} [ + (setAttrByPath config-ppath.shell-ppath { override.version = "${config.src}"; - job = config.shell-attribute; + job = config-ppath.shell-attribute; main-job = true; }) - (setAttrByPath config.ppath + (setAttrByPath config-ppath.ppath { override.version = "${config.src}"; - job = config.attribute; + job = config-ppath.attribute; main-job = true; }) i - (mk-bundles [ "coqPackages" ] override) + (mk-bundles [ config-ppath.rocq-coq-packages ] override) (mk-bundles [ "ocamlPackages" ] ocaml-override) (mk-bundles [ ] global-override) ]) config.bundles; buildInputFrom = pkgs: str: - pkgs.coqPackages.${str} or pkgs.ocamlPackages.${str} or pkgs.${str}; + pkgs.rocqPackages.${str} or pkgs.coqPackages.${str} or pkgs.ocamlPackages.${str} or pkgs.${str}; mk-instance = bundleName: bundle: let overlays = import ./overlays.nix @@ -51,7 +74,8 @@ in with config; let ci = import ./ci.nix { inherit lib this-shell-pkg pkgs bundle; }; genCI = import ../deps.nix - { inherit lib; inherit (pkgs) coqPackages; }; + { inherit lib; coqPackages = + if bundle ? isRocq then pkgs.rocqPackages else pkgs.coqPackages; }; jsonPkgsDeps = toJSON genCI.pkgsDeps; jsonPkgsRevDeps = toJSON genCI.pkgsRevDeps; jsonPkgsSorted = toJSON genCI.pkgsSorted; @@ -82,10 +106,11 @@ in with config; let if bi == [] then pkg else pkg.overrideAttrs (o: { buildInputs = o.buildInputs ++ bi;}); - notfound-ppath = throw "config-parser-1.0.0: not found: ${toString config.ppath}"; - notfound-shell-ppath = throw "config-parser-1.0.0: not found: ${toString config.shell-ppath}"; - this-pkg = patchBIPkg (attrByPath config.ppath notfound-ppath pkgs); - this-shell-pkg = patchBIPkg (attrByPath config.shell-ppath notfound-shell-ppath pkgs); + config-ppath = bundle-ppath bundle; + notfound-ppath = throw "config-parser-1.0.0: not found: ${toString config-ppath.ppath}"; + notfound-shell-ppath = throw "config-parser-1.0.0: not found: ${toString config-ppath.shell-ppath}"; + this-pkg = patchBIPkg (attrByPath config-ppath.ppath notfound-ppath pkgs); + this-shell-pkg = patchBIPkg (attrByPath config-ppath.shell-ppath notfound-shell-ppath pkgs); in rec { inherit bundle pkgs this-pkg this-shell-pkg ci genCI; diff --git a/config-parser-1.0.0/normalize.nix b/config-parser-1.0.0/normalize.nix index dd56bf5..8342a88 100644 --- a/config-parser-1.0.0/normalize.nix +++ b/config-parser-1.0.0/normalize.nix @@ -26,9 +26,6 @@ in rec { format = "1.0.0"; attribute = config.attribute or "template"; shell-attribute = config.shell-attribute or attribute; - path-to-attribute = config.path-to-attribute or [ "coqPackages" ]; - path-to-shell-attribute = - config.path-to-shell-attribute or path-to-attribute; nixpkgs = config.nixpkgs or initial.nixpkgs; pname = config.pname or attribute; shell-pname = config.shell-pname or pname; @@ -46,7 +43,4 @@ in rec { # cf https://github.com/NixOS/nix/issues/1837 then { url = initial.src; shallow = true; } else initial.src) else /. + initial.src); - # not configurable from config.nix: - ppath = path-to-attribute ++ [ attribute ]; - shell-ppath = path-to-shell-attribute ++ [ shell-attribute ]; } diff --git a/template-config.nix b/template-config.nix index 091d7c0..67742c1 100644 --- a/template-config.nix +++ b/template-config.nix @@ -38,6 +38,10 @@ ## When generating GitHub Action CI, one workflow file ## will be created per bundle bundles.default = { + ## Uncomment the following to mark the current bundle as a rocq bundle. + ## By default, the bundle is a coq bundle, + ## i.e., Coq <= 8.20 or using Coq shim for Rocq >= 9.0. + # isRocq = true; ## You can override Coq and other Coq coqPackages ## through the following attribute