From 4b2e4a4f9ea351011d332df277ec6893886f5f59 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Fri, 11 Oct 2024 23:31:23 +0200 Subject: [PATCH 1/9] Update coq-nix-toolbox --- .nix/coq-nix-toolbox.nix | 2 +- .nix/nixpkgs.nix | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) delete mode 100644 .nix/nixpkgs.nix diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index ca847615b..5bf0b8bff 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"39243d0edb4cb0b872d299c4b128fe232f0d8101" +"e0247d8e45ffb7a62d9052f39cc342a95bbf232f" diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix deleted file mode 100644 index 142eb30ba..000000000 --- a/.nix/nixpkgs.nix +++ /dev/null @@ -1,4 +0,0 @@ -fetchTarball { - url = https://github.com/NixOS/nixpkgs/archive/61fcca66117a68f7189b93ff199c8147754be14c.tar.gz; - sha256 = "1byvy3g4wd6p283z5p6jp8j2fyk1rn7y5a2wis2ja0ws5bymbfv4"; - } From 4486ffdba7baf51dc51d79114e33d6ad9faeea03 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Fri, 11 Oct 2024 23:31:44 +0200 Subject: [PATCH 2/9] Update package definitions --- .nix/coq-overlays/equations/default.nix | 22 +++++-- .nix/coq-overlays/metacoq/default.nix | 79 ++++++++++++++++--------- 2 files changed, 68 insertions(+), 33 deletions(-) diff --git a/.nix/coq-overlays/equations/default.nix b/.nix/coq-overlays/equations/default.nix index ffe72ad33..b517d16ab 100644 --- a/.nix/coq-overlays/equations/default.nix +++ b/.nix/coq-overlays/equations/default.nix @@ -1,11 +1,15 @@ { lib, mkCoqDerivation, coq, version ? null }: -with lib; (mkCoqDerivation { +(mkCoqDerivation { pname = "equations"; owner = "mattam82"; repo = "Coq-Equations"; inherit version; - defaultVersion = switch coq.coq-version [ + defaultVersion = lib.switch coq.coq-version [ + { case = "8.20"; out = "1.3.1+8.20"; } + { case = "8.19"; out = "1.3+8.19"; } + { case = "8.18"; out = "1.3+8.18"; } + { case = "8.17"; out = "1.3+8.17"; } { case = "8.16"; out = "1.3+8.16"; } { case = "8.15"; out = "1.3+8.15"; } { case = "8.14"; out = "1.3+8.14"; } @@ -54,14 +58,22 @@ with lib; (mkCoqDerivation { release."1.3+8.15".sha256 = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k"; release."1.3+8.16".rev = "v1.3-8.16"; release."1.3+8.16".sha256 = "sha256-zyMGeRObtSGWh7n3WCqesBZL5EgLvKwmnTy09rYpxyE="; + release."1.3+8.17".rev = "v1.3-8.17"; + release."1.3+8.17".sha256 = "sha256-yNotSIxFkhTg3reZIchGQ7cV9WmTJ7p7hPfKGBiByDw="; + release."1.3+8.18".rev = "v1.3-8.18"; + release."1.3+8.18".sha256 = "sha256-8MZO9vWdr8wlAov0lBTYMnde0RuMyhaiM99zp7Zwfao="; + release."1.3+8.19".rev = "v1.3-8.19"; + release."1.3+8.19".sha256 = "sha256-roBCWfAHDww2Z2JbV5yMI3+EOfIsv3WvxEcUbBiZBsk="; + release."1.3.1+8.20".rev = "v1.3.1-8.20"; + release."1.3.1+8.20".sha256 = "sha256-u8LB1KiACM5zVaoL7dSdHYvZgX7pf30VuqtjLLGuTzc="; mlPlugin = true; - meta = { + meta = with lib; { homepage = "https://mattam82.github.io/Coq-Equations/"; - description = "A plugin for Coq to add dependent pattern-matching"; + description = "Plugin for Coq to add dependent pattern-matching"; maintainers = with maintainers; [ jwiegley ]; }; }).overrideAttrs (o: { - preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}"; + preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}"; }) diff --git a/.nix/coq-overlays/metacoq/default.nix b/.nix/coq-overlays/metacoq/default.nix index 06ab02870..c79261aa1 100644 --- a/.nix/coq-overlays/metacoq/default.nix +++ b/.nix/coq-overlays/metacoq/default.nix @@ -1,19 +1,22 @@ -{ lib, fetchzip, - mkCoqDerivation, recurseIntoAttrs, single ? false, - coqPackages, coq, equations, version ? null }@args: -with builtins // lib; +{ lib, + mkCoqDerivation, single ? false, + coq, equations, version ? null }@args: + let repo = "metacoq"; owner = "MetaCoq"; - defaultVersion = with versions; switch coq.coq-version [ + defaultVersion = lib.switch coq.coq-version [ { case = "8.11"; out = "1.0-beta2-8.11"; } { case = "8.12"; out = "1.0-beta2-8.12"; } # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3) # { case = "8.13"; out = "1.0-beta2-8.13"; } - { case = "8.14"; out = "1.0-8.14"; } - { case = "8.15"; out = "1.0-8.15"; } - { case = "8.16"; out = "1.0-8.16"; } - { case = "dev"; out = "dev"; } + { case = "8.14"; out = "1.1-8.14"; } + { case = "8.15"; out = "1.1-8.15"; } + { case = "8.16"; out = "1.1-8.16"; } + { case = "8.17"; out = "1.3.1-8.17"; } + { case = "8.18"; out = "1.3.1-8.18"; } + { case = "8.19"; out = "1.3.2-8.19"; } + { case = "8.20"; out = "1.3.2-8.20"; } ] null; release = { "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs="; @@ -22,17 +25,28 @@ let "1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0="; "1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k="; "1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o="; + "1.1-8.14".sha256 = "sha256-6vViCNQl6BnGgOHX3P/OLfFXN4aUfv4RbDokfz2BgQI="; + "1.1-8.15".sha256 = "sha256-qCD3wFW4E+8vSVk4XoZ0EU4PVya0al+JorzS9nzmR/0="; + "1.1-8.16".sha256 = "sha256-cTK4ptxpPPlqxAhasZFX3RpSlsoTZwhTqs2A3BZy9sA="; + "1.2.1-8.17".sha256 = "sha256-FP4upuRsG8B5Q5FIr76t+ecRirrOUX0D1QiLq0/zMyE="; + "1.2.1-8.18".sha256 = "sha256-49g5db2Bv8HpltptJdxA7zrmgNFGC6arx5h2mKHhrko="; + "1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc="; + "1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY="; + "1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64="; + "1.3.2-8.19".sha256 = "sha256-e5Pm1AhaQrO6JoZylSXYWmeXY033QflQuCBZhxGH8MA="; + "1.3.2-8.20".sha256 = "sha256-4J7Ly4Fc2E/I6YqvzTLntVVls5t94OUOjVMKJyyJdw8="; }; releaseRev = v: "v${v}"; # list of core metacoq packages sorted by dependency order - packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]; + packages = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" + then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ] + else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ]; template-coq = metacoq_ "template-coq"; metacoq_ = package: let - metacoq-deps = if package == "single" then [] - else map metacoq_ (head (splitList (pred.equal package) packages)); + metacoq-deps = lib.optionals (package != "single") (map metacoq_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "./" else "./${package}"; pname = if package == "all" then "metacoq" else "metacoq-${package}"; pkgallMake = '' @@ -46,7 +60,7 @@ let mlPlugin = true; propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps; - patchPhase = '' + patchPhase = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" then '' patchShebangs ./configure.sh patchShebangs ./template-coq/update_plugin.sh patchShebangs ./template-coq/gen-src/to-lower.sh @@ -54,13 +68,22 @@ let 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-coq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh + '' else '' + patchShebangs ./configure.sh + patchShebangs ./template-coq/update_plugin.sh + patchShebangs ./template-coq/gen-src/to-lower.sh + patchShebangs ./pcuic/clean_extraction.sh + patchShebangs ./safechecker/clean_extraction.sh + patchShebangs ./erasure/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-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh '' ; - configurePhase = optionalString (package == "all") pkgallMake + '' + configurePhase = lib.optionalString (package == "all") pkgallMake + '' touch ${pkgpath}/metacoq-config - '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' + '' + lib.optionalString (lib.elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config - '' + optionalString (package == "single") '' + '' + lib.optionalString (package == "single") '' ./configure.sh local ''; @@ -70,18 +93,18 @@ let meta = { homepage = "https://metacoq.github.io/"; - license = licenses.mit; - maintainers = with maintainers; [ cohencyril ]; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ cohencyril ]; }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages metacoq_; }) - ).overrideAttrs (o: - let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" || - (o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; - in - { - propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; - }); - in derivation; + } // lib.optionalAttrs (package != "single") + { passthru = lib.genAttrs packages metacoq_; }) + ).overrideAttrs (o: + let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" || + (o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; + in + { + propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; + }); + in derivation; in metacoq_ (if single then "single" else "all") From db2018e503580e8fec8ca8148a8aaf953bf0d1c0 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Fri, 11 Oct 2024 23:31:53 +0200 Subject: [PATCH 3/9] Update bundles --- .github/workflows/nix-action-coq-8.19.yml | 185 ++++++++++++++++++++++ .nix/config.nix | 48 +----- 2 files changed, 191 insertions(+), 42 deletions(-) create mode 100644 .github/workflows/nix-action-coq-8.19.yml diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml new file mode 100644 index 000000000..71d1e9948 --- /dev/null +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -0,0 +1,185 @@ +jobs: + coq: + 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 + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community + name: coq + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $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 current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "coq" + equations: + 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@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community + name: coq + - id: stepCheck + name: Checking presence of CI target equations + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.19\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $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-8.19" + --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-8.19" + --argstr job "equations" + metacoq: + needs: + - coq + - equations + 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 + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community + name: coq + - id: stepCheck + name: Checking presence of CI target metacoq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.19\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-pcuic" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-safechecker' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-safechecker" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-erasure' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-erasure" + - 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-8.19" + --argstr job "metacoq" +name: Nix CI for bundle coq-8.19 +'on': + pull_request: + paths: + - .github/workflows/nix-action-coq-8.19.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-coq-8.19.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index db37a6b43..63d53dc78 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,59 +31,23 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "coq-dev"; + default-bundle = "coq-8.19"; # MetaCoq is expected to be compatible with a single coq version # The name of the bundle should finish with the coq version to use # cachedMake.sh - bundles."coq-dev" = { + bundles."coq-8.19" = { + coqPackages.coq.override.version = "8.19"; + coqPackages.equations.override.version = "1.3+8.19"; - ## You can override Coq and other Coq coqPackages - ## through the following attribute - coqPackages.coq.override.version = "master"; - coqPackages.equations.override.version = "main"; - ## In some cases, light overrides are not available/enough - ## in which case you can use either - # coqPackages..overrideAttrs = o: ; - # coqPackages.equations.overrideAttrs = o: ; - ## or a "long" overlay to put in `.nix/coq-overlays - ## you may use `nix-shell --run fetchOverlay ` - ## to automatically retrieve the one from nixpkgs - ## if it exists and is correctly named/located - - ## You can override Coq and other coqPackages - ## through the following attribute - ## If does not support light overrides, - ## you may use `overrideAttrs` or long overlays - ## located in `.nix/ocaml-overlays` - ## (there is no automation for this one) - # ocamlPackages..override.version = "x.xx"; - - ## You can also override packages from the nixpkgs toplevel - # .override.overrideAttrs = o: ; - ## Or put an overlay in `.nix/overlays` - - ## you may mark a package as a main CI job (one to take deps and - ## rev deps from) as follows - # coqPackages..main-job = true; - ## by default the current package and its shell attributes are main jobs - - ## you may mark a package as a CI job as follows - # coqPackages..job = "test"; - ## It can then built through - ## nix-build --argstr bundle "default" --arg job "test"; - ## in the absence of such a directive, the job "another-pkg" will - ## is still available, but will be automatically included in the CI - ## via the command genNixActions only if it is a dependency or a - ## reverse dependency of a job flagged as "main-job" (see above). + push-branches = ["coq-8.19"]; }; ## Cachix caches to use in CI ## Below we list some standard ones cachix.coq = {}; - # cachix.math-comp = {}; cachix.coq-community = {}; ## If you have write access to one of these caches you can @@ -91,7 +55,7 @@ ## variable on GitHub. Then, you should give the variable ## name here. For instance, coq-community projects can use ## the following line instead of the one above: - cachix.metacoq.authToken = "CACHIX_AUTH_TOKEN"; + # cachix.metacoq.authToken = "CACHIX_AUTH_TOKEN"; ## Or if you have a signing key for a given Cachix cache: # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" From b59243b56636de99e69e695e395ee733a7dbfbba Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Sun, 13 Oct 2024 03:19:49 +0200 Subject: [PATCH 4/9] Fix missing MetaCoq sub-modules --- .github/workflows/nix-action-coq-8.19.yml | 26 ++++++++++++++++++++++- .nix/config.nix | 2 ++ .nix/coq-nix-toolbox.nix | 2 +- .nix/coq-overlays/metacoq/default.nix | 14 ++++++++---- default.nix | 2 +- 5 files changed, 39 insertions(+), 7 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml index 71d1e9948..7cbdc21a2 100644 --- a/.github/workflows/nix-action-coq-8.19.yml +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -148,6 +148,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-utils' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-utils" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-common' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-common" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: metacoq-template-coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" @@ -160,10 +168,26 @@ jobs: name: 'Building/fetching previous CI target: metacoq-safechecker' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "metacoq-safechecker" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-pcuic" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: metacoq-erasure' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "metacoq-erasure" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-quotation' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-quotation" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-safechecker-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-safechecker-plugin" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-erasure-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-erasure-plugin" - 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-8.19" @@ -182,4 +206,4 @@ name: Nix CI for bundle coq-8.19 - reopened push: branches: - - master + - coq-8.19 diff --git a/.nix/config.nix b/.nix/config.nix index 63d53dc78..06ca74735 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -40,6 +40,8 @@ coqPackages.coq.override.version = "8.19"; coqPackages.equations.override.version = "1.3+8.19"; + coqPackages.metacoq.main-job = true; + # coqPackages.metacoq-utils.main-job = true; push-branches = ["coq-8.19"]; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 5bf0b8bff..2160e31c4 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"e0247d8e45ffb7a62d9052f39cc342a95bbf232f" +"d483e863600a529f057641af41a10716a2aa06a4" diff --git a/.nix/coq-overlays/metacoq/default.nix b/.nix/coq-overlays/metacoq/default.nix index c79261aa1..bc87c7111 100644 --- a/.nix/coq-overlays/metacoq/default.nix +++ b/.nix/coq-overlays/metacoq/default.nix @@ -39,9 +39,7 @@ let releaseRev = v: "v${v}"; # list of core metacoq packages sorted by dependency order - packages = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" - then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ] - else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ]; + packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]; template-coq = metacoq_ "template-coq"; @@ -105,6 +103,14 @@ let { propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; }); - in derivation; + # utils, common, template-pcuic, quotation, safechecker-plugin, and erasure-plugin + # packages didn't exist before 1.2, so bulding nothing in that case + patched-derivation = derivation.overrideAttrs (o: + lib.optionalAttrs (o.pname != null && + lib.elem package [ "utils" "common" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" ] && + o.version != null && o.version != "dev" && lib.versions.isLt "1.2" o.version) + { patchPhase = ""; configurePhase = ""; preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; } + ); + in patched-derivation; in metacoq_ (if single then "single" else "all") diff --git a/default.nix b/default.nix index 6fda2e8b2..c5e7de9bf 100644 --- a/default.nix +++ b/default.nix @@ -4,7 +4,7 @@ bundle ? null, job ? null, inNixShell ? null, src ? ./., }@args: let auto = fetchGit { - url = "https://github.com/coq-community/coq-nix-toolbox.git"; + url = "https://github.com/4ever2/coq-nix-toolbox.git"; allRefs = true ; # ref = "master"; rev = import .nix/coq-nix-toolbox.nix; From 8154704984fbb8da439b47cadb26a76298c78a60 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Sun, 13 Oct 2024 03:21:20 +0200 Subject: [PATCH 5/9] Set up reverse dependencies --- .github/workflows/nix-action-coq-8.19.yml | 56 +++++++++++++++++++++++ .nix/config.nix | 2 + 2 files changed, 58 insertions(+) diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml index 7cbdc21a2..e1ad3cd55 100644 --- a/.github/workflows/nix-action-coq-8.19.yml +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -1,4 +1,60 @@ jobs: + ElmExtraction: + needs: + - coq + - metacoq + 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 + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community + name: coq + - id: stepCheck + name: Checking presence of CI target ElmExtraction + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.19\" --argstr job \"ElmExtraction\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq" + - 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-8.19" + --argstr job "ElmExtraction" coq: needs: [] runs-on: ubuntu-latest diff --git a/.nix/config.nix b/.nix/config.nix index 06ca74735..73ba74f7b 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -45,6 +45,8 @@ push-branches = ["coq-8.19"]; + # Reverse dependencies + coqPackages.ElmExtraction.override.version = "master"; }; ## Cachix caches to use in CI From 90a8ae6f16a798ce0b0bc63d7df80b7fbcf462a0 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Tue, 15 Oct 2024 12:04:24 +0200 Subject: [PATCH 6/9] Update Nix toolbox --- .nix/coq-nix-toolbox.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 2160e31c4..9f30d3b1a 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"d483e863600a529f057641af41a10716a2aa06a4" +"f8bc8e6b019071bbd4ce47fd87d1bbf49b04dbc8" From fecfdd1b5a33240693030486d7762efe52a1650a Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Tue, 15 Oct 2024 12:04:37 +0200 Subject: [PATCH 7/9] Add RustExtraction rev dep --- .github/workflows/nix-action-coq-8.19.yml | 56 +++++++++++++++++++++++ .nix/config.nix | 3 +- 2 files changed, 58 insertions(+), 1 deletion(-) diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml index e1ad3cd55..9cabec3f5 100644 --- a/.github/workflows/nix-action-coq-8.19.yml +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -55,6 +55,62 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "ElmExtraction" + RustExtraction: + needs: + - coq + - metacoq + 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 + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community + name: coq + - id: stepCheck + name: Checking presence of CI target RustExtraction + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.19\" --argstr job \"RustExtraction\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq" + - 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-8.19" + --argstr job "RustExtraction" coq: needs: [] runs-on: ubuntu-latest diff --git a/.nix/config.nix b/.nix/config.nix index 73ba74f7b..04fefd28a 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -46,7 +46,8 @@ push-branches = ["coq-8.19"]; # Reverse dependencies - coqPackages.ElmExtraction.override.version = "master"; + coqPackages.ElmExtraction.override.version = "coq-8.19"; + coqPackages.RustExtraction.override.version = "coq-8.19"; }; ## Cachix caches to use in CI From bb1ae7d486914980b933908558b73ae2a333b3f8 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Tue, 15 Oct 2024 13:33:50 +0200 Subject: [PATCH 8/9] Enable cache --- .github/workflows/nix-action-coq-8.19.yml | 35 +++++++++++++---------- .nix/config.nix | 2 +- 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml index 9cabec3f5..62414450a 100644 --- a/.github/workflows/nix-action-coq-8.19.yml +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -32,11 +32,12 @@ jobs: uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup metacoq uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq - id: stepCheck name: Checking presence of CI target ElmExtraction run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -88,11 +89,12 @@ jobs: uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup metacoq uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq - id: stepCheck name: Checking presence of CI target RustExtraction run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -142,11 +144,12 @@ jobs: uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup metacoq uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -189,11 +192,12 @@ jobs: uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup metacoq uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq - id: stepCheck name: Checking presence of CI target equations run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -241,11 +245,12 @@ jobs: uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup metacoq uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq - id: stepCheck name: Checking presence of CI target metacoq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ diff --git a/.nix/config.nix b/.nix/config.nix index 04fefd28a..97903af88 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -60,7 +60,7 @@ ## variable on GitHub. Then, you should give the variable ## name here. For instance, coq-community projects can use ## the following line instead of the one above: - # cachix.metacoq.authToken = "CACHIX_AUTH_TOKEN"; + cachix.metacoq.authToken = "CACHIX_AUTH_TOKEN"; ## Or if you have a signing key for a given Cachix cache: # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" From 87337324051c4b9384c0183a1adbf7b2368e530a Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Tue, 29 Oct 2024 22:59:49 +0100 Subject: [PATCH 9/9] Add metacoq-translations and fix dependency ordering --- .github/workflows/nix-action-coq-8.19.yml | 847 ++++++++++++++++++++-- .nix/config.nix | 4 +- .nix/coq-nix-toolbox.nix | 2 +- .nix/coq-overlays/metacoq/default.nix | 31 +- default.nix | 5 +- 5 files changed, 795 insertions(+), 94 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml index 62414450a..5abdf0b3e 100644 --- a/.github/workflows/nix-action-coq-8.19.yml +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -6,23 +6,23 @@ jobs: 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" + 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" + 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: @@ -40,10 +40,10 @@ jobs: name: metacoq - id: stepCheck name: Checking presence of CI target ElmExtraction - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"ElmExtraction\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"ElmExtraction\" \\\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-8.19" @@ -63,23 +63,23 @@ jobs: 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" + 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" + 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: @@ -97,10 +97,10 @@ jobs: name: metacoq - id: stepCheck name: Checking presence of CI target RustExtraction - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"RustExtraction\" \\\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" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"RustExtraction\" \\\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-8.19" @@ -118,23 +118,23 @@ jobs: 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" + 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" + 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: @@ -152,8 +152,8 @@ jobs: name: metacoq - id: stepCheck name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -166,23 +166,23 @@ jobs: 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" + 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" + 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: @@ -200,8 +200,8 @@ jobs: name: metacoq - id: stepCheck name: Checking presence of CI target equations - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -216,26 +216,30 @@ jobs: needs: - coq - equations + - metacoq-safechecker-plugin + - metacoq-erasure-plugin + - metacoq-translations + - metacoq-quotation 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" + 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" + 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: @@ -253,8 +257,8 @@ jobs: name: metacoq - id: stepCheck name: Checking presence of CI target metacoq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -265,22 +269,143 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-safechecker-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-safechecker-plugin" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-erasure-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-erasure-plugin" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-translations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-translations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-quotation' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-quotation" + - 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-8.19" + --argstr job "metacoq" + metacoq-common: + needs: + - coq + - equations + - metacoq-utils + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-common + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-common\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: metacoq-utils' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "metacoq-utils" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-common' + name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "metacoq-common" + metacoq-erasure: + needs: + - coq + - equations + - metacoq-safechecker + - metacoq-template-pcuic + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-erasure + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-erasure\" \\\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: metacoq-template-coq' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "metacoq-template-coq" + --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-pcuic' + name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "metacoq-pcuic" + --argstr job "equations" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: metacoq-safechecker' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" @@ -289,28 +414,590 @@ jobs: name: 'Building/fetching previous CI target: metacoq-template-pcuic' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "metacoq-template-pcuic" + - 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-8.19" + --argstr job "metacoq-erasure" + metacoq-erasure-plugin: + needs: + - coq + - equations + - metacoq-template-pcuic + - metacoq-erasure + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-erasure-plugin + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-erasure-plugin\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-pcuic" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: metacoq-erasure' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "metacoq-erasure" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-quotation' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-erasure-plugin" + metacoq-pcuic: + needs: + - coq + - equations + - metacoq-common + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-pcuic + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-pcuic\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-common' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-common" + - 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-8.19" + --argstr job "metacoq-pcuic" + metacoq-quotation: + needs: + - coq + - equations + - metacoq-template-coq + - metacoq-pcuic + - metacoq-template-pcuic + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-quotation + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-quotation\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-pcuic" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-pcuic" + - 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-8.19" --argstr job "metacoq-quotation" + metacoq-safechecker: + needs: + - coq + - equations + - metacoq-pcuic + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-safechecker + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-safechecker\" \\\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: metacoq-safechecker-plugin' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-pcuic" + - 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-8.19" + --argstr job "metacoq-safechecker" + metacoq-safechecker-plugin: + needs: + - coq + - equations + - metacoq-template-pcuic + - metacoq-safechecker + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-safechecker-plugin + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-safechecker-plugin\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-pcuic" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-safechecker' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-safechecker" + - 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-8.19" --argstr job "metacoq-safechecker-plugin" + metacoq-template-coq: + needs: + - coq + - equations + - metacoq-common + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-template-coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-template-coq\" \\\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: metacoq-erasure-plugin' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "metacoq-erasure-plugin" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-common' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-common" - 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-8.19" - --argstr job "metacoq" + --argstr job "metacoq-template-coq" + metacoq-template-pcuic: + needs: + - coq + - equations + - metacoq-template-coq + - metacoq-pcuic + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-template-pcuic + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-template-pcuic\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-pcuic' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-pcuic" + - 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-8.19" + --argstr job "metacoq-template-pcuic" + metacoq-translations: + needs: + - coq + - equations + - metacoq-template-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@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-translations + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-translations\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: metacoq-template-coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "metacoq-template-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-8.19" + --argstr job "metacoq-translations" + metacoq-utils: + needs: + - coq + - equations + 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 metacoq + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq-utils + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"coq-8.19\" --argstr job \"metacoq-utils\" \\\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-8.19" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" + --argstr job "equations" + - 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-8.19" + --argstr job "metacoq-utils" name: Nix CI for bundle coq-8.19 -'on': +on: pull_request: paths: - .github/workflows/nix-action-coq-8.19.yml diff --git a/.nix/config.nix b/.nix/config.nix index 97903af88..0272dd09d 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -40,8 +40,8 @@ coqPackages.coq.override.version = "8.19"; coqPackages.equations.override.version = "1.3+8.19"; - coqPackages.metacoq.main-job = true; - # coqPackages.metacoq-utils.main-job = true; + # coqPackages.metacoq.main-job = true; + coqPackages.metacoq-utils.main-job = true; push-branches = ["coq-8.19"]; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 9f30d3b1a..eeccddce5 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"f8bc8e6b019071bbd4ce47fd87d1bbf49b04dbc8" +"95ab8ac1ca273c4db485937e55b03ba48fb2accc" diff --git a/.nix/coq-overlays/metacoq/default.nix b/.nix/coq-overlays/metacoq/default.nix index bc87c7111..48691bba9 100644 --- a/.nix/coq-overlays/metacoq/default.nix +++ b/.nix/coq-overlays/metacoq/default.nix @@ -38,20 +38,35 @@ let }; releaseRev = v: "v${v}"; - # list of core metacoq packages sorted by dependency order - packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]; + # list of core metacoq packages and their dependencies + packages = { + "utils" = []; + "common" = [ "utils" ]; + "template-coq" = [ "common" ]; + "pcuic" = if (lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev") + then [ "common" ] + else [ "template-coq" ]; + "safechecker" = [ "pcuic" ]; + "template-pcuic" = [ "template-coq" "pcuic" ]; + "erasure" = [ "safechecker" "template-pcuic" ]; + "quotation" = [ "template-coq" "pcuic" "template-pcuic" ]; + "safechecker-plugin" = [ "template-pcuic" "safechecker" ]; + "erasure-plugin" = [ "template-pcuic" "erasure" ]; + "translations" = [ "template-coq" ]; + "all" = [ "safechecker-plugin" "erasure-plugin" "translations" "quotation" ]; + }; template-coq = metacoq_ "template-coq"; metacoq_ = package: let - metacoq-deps = lib.optionals (package != "single") (map metacoq_ (lib.head (lib.splitList (lib.pred.equal package) packages))); + metacoq-deps = lib.optionals (package != "single") (map metacoq_ packages.${package}); pkgpath = if package == "single" then "./" else "./${package}"; pname = if package == "all" then "metacoq" else "metacoq-${package}"; pkgallMake = '' mkdir all echo "all:" > all/Makefile echo "install:" >> all/Makefile - '' ; + ''; derivation = (mkCoqDerivation ({ inherit version pname defaultVersion release releaseRev repo owner; @@ -75,11 +90,11 @@ let patchShebangs ./erasure/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-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh - '' ; + ''; configurePhase = lib.optionalString (package == "all") pkgallMake + '' touch ${pkgpath}/metacoq-config - '' + lib.optionalString (lib.elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' + '' + lib.optionalString (lib.elem package ["erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" "translations"]) '' echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config '' + lib.optionalString (package == "single") '' ./configure.sh local @@ -87,7 +102,7 @@ let preBuild = '' cd ${pkgpath} - '' ; + ''; meta = { homepage = "https://metacoq.github.io/"; @@ -95,7 +110,7 @@ let maintainers = with lib.maintainers; [ cohencyril ]; }; } // lib.optionalAttrs (package != "single") - { passthru = lib.genAttrs packages metacoq_; }) + { passthru = lib.mapAttrs (package: deps: metacoq_ package) packages; }) ).overrideAttrs (o: let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" || (o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; diff --git a/default.nix b/default.nix index c5e7de9bf..1a24d7a18 100644 --- a/default.nix +++ b/default.nix @@ -4,9 +4,8 @@ bundle ? null, job ? null, inNixShell ? null, src ? ./., }@args: let auto = fetchGit { - url = "https://github.com/4ever2/coq-nix-toolbox.git"; - allRefs = true ; - # ref = "master"; + url = "https://github.com/coq-community/coq-nix-toolbox.git"; + ref = "master"; rev = import .nix/coq-nix-toolbox.nix; }; in