diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index ef27fb2835..de3414e5bd 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -3041,85 +3041,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "metarocq-template-rocq" - metarocq-translations: - needs: - - coq - - equations - - ExtLib - - stdlib - - metarocq-template-rocq - 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@v6 - 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@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (metarocq-translations) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"metarocq-translations\" \\\n --dry-run 2> err - > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: - getting derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "equations" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ExtLib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "ExtLib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "stdlib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: metarocq-template-rocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "metarocq-template-rocq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "metarocq-translations" metarocq-utils: needs: - coq diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 9147e1f25b..a626aa0f54 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -4363,7 +4363,6 @@ jobs: - stdlib - metarocq-safechecker-plugin - metarocq-erasure-plugin - - metarocq-translations - metarocq-quotation runs-on: ubuntu-latest steps: @@ -4437,10 +4436,6 @@ jobs: name: 'Building/fetching previous CI target: metarocq-erasure-plugin' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "metarocq-erasure-plugin" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: metarocq-translations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "metarocq-translations" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-quotation' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5254,85 +5249,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "metarocq-test" - metarocq-translations: - needs: - - coq - - equations - - ExtLib - - stdlib - - metarocq-template-rocq - 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@v6 - 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@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (metarocq-translations) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"metarocq-translations\" \\\n --dry-run 2> - err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\ - Error: getting derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "equations" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ExtLib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "ExtLib" - - if: steps.stepCheck.outputs.status != 'fetched' - 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 != 'fetched' - name: 'Building/fetching previous CI target: metarocq-template-rocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "metarocq-template-rocq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "metarocq-translations" metarocq-utils: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index 3f4ec53abd..04ad0084a8 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -219,6 +219,7 @@ with builtins; with (import {}).lib; "metarocq-safechecker" "metarocq-safechecker-plugin" "metarocq-template-pcuic" + "metarocq-translations" "metarocq-test" "rewriter" "riscvcoq" @@ -265,6 +266,7 @@ with builtins; with (import {}).lib; validsdp.job = false; # not in Rocq CI verified-extraction.job = false; # not in Rocq CI wasmcert.job = false; # not in Rocq CI + metarocq-translations.job = false; # not in Rocq CI hierarchy-builder.job = false; # not a reverse dependency of Stdlib mathcomp-order.job = false; # not a reverse dependency of Stdlib mathcomp-fingroup.job = false; # not a reverse dependency of Stdlib diff --git a/.nix/coq-overlays/metarocq/default.nix b/.nix/coq-overlays/metarocq/default.nix new file mode 100644 index 0000000000..3a9d783938 --- /dev/null +++ b/.nix/coq-overlays/metarocq/default.nix @@ -0,0 +1,153 @@ +{ + lib, + mkCoqDerivation, + single ? false, + coq, + equations, + ExtLib, + stdlib, + version ? null, +}@args: + +let + repo = "metarocq"; + owner = "MetaRocq"; + defaultVersion = + let + case = case: out: { inherit case out; }; + in + lib.switch coq.coq-version [ + (case "9.1" "1.5.1-9.1") + (case "9.0" "1.4-9.0.1") + ] null; + release = { + "1.4-9.0".sha256 = "sha256-5QecDAMkvgfDPZ7/jDfnOgcE+Eb1LTAozP7nz6nkuxg="; + "1.4-9.0.1".sha256 = "sha256-zMUd2A6EG0LYK3L9ABQvS/Et4MDpSmf3Pxd9+IPNYkI="; + "1.4-9.1".sha256 = "sha256-v6jFvUavIzyb/e6ytAaZjxQLFM9uW9TDUB77yRO74eE="; + "1.4.1-9.1".sha256 = "sha256-tzoAWX74lg7pArGVP11QBvDRKMvmGxXvrf3+1E3Y4DI="; + "1.5.1-9.1".sha256 = "sha256-0iFnSzfbufn2XhJ8EPyWu3KIiHYwxfMVQa2KT6GSR7s="; + }; + releaseRev = v: "v${v}"; + + # list of core metarocq packages and their dependencies + packages = { + "utils" = [ ]; + "common" = [ "utils" ]; + "template-rocq" = [ "common" ]; + "pcuic" = [ "common" ]; + "safechecker" = [ "pcuic" ]; + "template-pcuic" = [ + "template-rocq" + "pcuic" + ]; + "erasure" = [ + "safechecker" + "template-pcuic" + ]; + "quotation" = [ + "template-rocq" + "pcuic" + "template-pcuic" + ]; + "safechecker-plugin" = [ + "template-pcuic" + "safechecker" + ]; + "erasure-plugin" = [ + "template-pcuic" + "erasure" + ]; + "translations" = [ "template-rocq" ]; + "all" = [ + "safechecker-plugin" + "erasure-plugin" + # "translations" + "quotation" + ]; + }; + + template-rocq = metarocq_ "template-rocq"; + + metarocq_ = + package: + let + metarocq-deps = lib.optionals (package != "single") (map metarocq_ packages.${package}); + pkgpath = if package == "single" then "./" else "./${package}"; + pname = if package == "all" then "metarocq" else "metarocq-${package}"; + pkgallMake = '' + mkdir all + echo "all:" > all/Makefile + echo "install:" >> all/Makefile + ''; + derivation = mkCoqDerivation ( + { + inherit + version + pname + defaultVersion + release + releaseRev + repo + owner + ; + + mlPlugin = true; + propagatedBuildInputs = [ + equations + ExtLib + stdlib + coq.ocamlPackages.zarith + coq.ocamlPackages.stdlib-shims + ] + ++ metarocq-deps; + + patchPhase = '' + patchShebangs ./configure.sh + patchShebangs ./template-rocq/update_plugin.sh + patchShebangs ./template-rocq/gen-src/to-lower.sh + patchShebangs ./safechecker-plugin/clean_extraction.sh + patchShebangs ./erasure-plugin/clean_extraction.sh + echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local + sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-rocq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh + ''; + + configurePhase = + lib.optionalString (package == "all") pkgallMake + + '' + touch ${pkgpath}/metarocq-config + '' + + + lib.optionalString + (lib.elem package [ + "erasure" + "template-pcuic" + "quotation" + "safechecker-plugin" + "erasure-plugin" + "translations" + ]) + '' + echo "-I ${template-rocq}/lib/coq/${coq.coq-version}/user-contrib/MetaRocq/Template/" > ${pkgpath}/metarocq-config + '' + + lib.optionalString (package == "single") '' + ./configure.sh local + ''; + + preBuild = '' + cd ${pkgpath} + ''; + + meta = { + homepage = "https://metarocq.github.io/"; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ cohencyril ]; + }; + } + // lib.optionalAttrs (package != "single") { + passthru = lib.mapAttrs (package: deps: metarocq_ package) packages; + } + ); + in + derivation; +in +metarocq_ (if single then "single" else "all")