From 7eb34e59313a322da809bd75ab6d48db81876700 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Wed, 10 Jul 2024 01:06:33 +0200 Subject: [PATCH 01/10] Nix setup --- .github/workflows/nix-action-8.17.yml | 325 ++++++++++++++++++++++++++ .github/workflows/nix-action-8.18.yml | 325 ++++++++++++++++++++++++++ .github/workflows/nix-action-8.19.yml | 325 ++++++++++++++++++++++++++ .nix/config.nix | 78 +++++++ .nix/coq-nix-toolbox.nix | 1 + .nix/coq-overlays/ConCert/default.nix | 40 ++++ default.nix | 12 + 7 files changed, 1106 insertions(+) create mode 100644 .github/workflows/nix-action-8.17.yml create mode 100644 .github/workflows/nix-action-8.18.yml create mode 100644 .github/workflows/nix-action-8.19.yml create mode 100644 .nix/config.nix create mode 100644 .nix/coq-nix-toolbox.nix create mode 100644 .nix/coq-overlays/ConCert/default.nix create mode 100644 default.nix diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml new file mode 100644 index 00000000..9ce97ba9 --- /dev/null +++ b/.github/workflows/nix-action-8.17.yml @@ -0,0 +1,325 @@ +jobs: + ConCert: + needs: + - coq + - metacoq + - QuickChick + - stdpp + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target ConCert + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"ConCert\" \\\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 "8.17" --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 "8.17" --argstr + job "metacoq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: QuickChick' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "QuickChick" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdpp' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "stdpp" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: RustExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "RustExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: ElmExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "ElmExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "ConCert" + QuickChick: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target QuickChick + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"QuickChick\" \\\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 "8.17" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-ext-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "coq-ext-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: simple-io' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "simple-io" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "QuickChick" + 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@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + 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 \"8.17\" --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 "8.17" --argstr + job "coq" + metacoq: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + 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 \"8.17\" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --argstr + job "metacoq" + stdpp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target stdpp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"stdpp\" \\\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 "8.17" --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 "8.17" --argstr + job "stdpp" +name: Nix CI for bundle 8.17 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.17.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.17.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml new file mode 100644 index 00000000..3abfb0d1 --- /dev/null +++ b/.github/workflows/nix-action-8.18.yml @@ -0,0 +1,325 @@ +jobs: + ConCert: + needs: + - coq + - metacoq + - QuickChick + - stdpp + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target ConCert + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"ConCert\" \\\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 "8.18" --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 "8.18" --argstr + job "metacoq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: QuickChick' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "QuickChick" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdpp' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "stdpp" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: RustExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "RustExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: ElmExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "ElmExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "ConCert" + QuickChick: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target QuickChick + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"QuickChick\" \\\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 "8.18" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-ext-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq-ext-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: simple-io' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "simple-io" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "QuickChick" + 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@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + 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 \"8.18\" --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 "8.18" --argstr + job "coq" + metacoq: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + 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 \"8.18\" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --argstr + job "metacoq" + stdpp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target stdpp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.18\" --argstr job \"stdpp\" \\\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 "8.18" --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 "8.18" --argstr + job "stdpp" +name: Nix CI for bundle 8.18 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.18.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.18.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml new file mode 100644 index 00000000..6e5e3dab --- /dev/null +++ b/.github/workflows/nix-action-8.19.yml @@ -0,0 +1,325 @@ +jobs: + ConCert: + needs: + - coq + - metacoq + - QuickChick + - stdpp + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target ConCert + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"ConCert\" \\\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 "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 "8.19" --argstr + job "metacoq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: QuickChick' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "QuickChick" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdpp' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "stdpp" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: RustExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "RustExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: ElmExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "ElmExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "ConCert" + QuickChick: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target QuickChick + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"QuickChick\" \\\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 "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-ext-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq-ext-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: simple-io' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "simple-io" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "QuickChick" + 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@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + 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 \"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 "8.19" --argstr + job "coq" + metacoq: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + 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 \"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 "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 "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 "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 "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 "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 "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 "8.19" --argstr + job "metacoq" + stdpp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v15 + with: + extraPullNames: coq-community, metacoq + name: coq + - id: stepCheck + name: Checking presence of CI target stdpp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"stdpp\" \\\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 "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 "8.19" --argstr + job "stdpp" +name: Nix CI for bundle 8.19 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.19.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.19.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix new file mode 100644 index 00000000..f4cb7aa0 --- /dev/null +++ b/.nix/config.nix @@ -0,0 +1,78 @@ +{ + ## DO NOT CHANGE THIS + format = "1.0.0"; + ## unless you made an automated or manual update + ## to another supported format. + + ## The attribute to build from the local sources, + ## either using nixpkgs data or the overlays located in `.nix/coq-overlays` + ## Will determine the default main-job of the bundles defined below + attribute = "ConCert"; + + ## If you want to select a different attribute (to build from the local sources as well) + ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument + # shell-attribute = "{{nix_name}}"; + + ## Maybe the shortname of the library is different from + ## the name of the nixpkgs attribute, if so, set it here: + # pname = "ConCert"; + + ## Lists the dependencies, phrased in terms of nix attributes. + ## No need to list Coq, it is already included. + ## These dependencies will systematically be added to the currently + ## known dependencies, if any more than Coq. + ## /!\ Remove this field as soon as the package is available on nixpkgs. + ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. + # buildInputs = [ ]; + + ## Indicate the relative location of your _CoqProject + ## If not specified, it defaults to "_CoqProject" + # coqproject = "_CoqProject"; + + ## select an entry to build in the following `bundles` set + ## defaults to "default" + default-bundle = "8.17"; + + ## write one `bundles.name` attribute set per + ## alternative configuration + ## When generating GitHub Action CI, one workflow file + ## will be created per bundle + bundles."8.17" = { + coqPackages.coq.override.version = "8.17"; + coqPackages.metacoq.override.version = "1.3.1-8.17"; + coqPackages.stdpp.override.version = "1.10.0"; + coqPackages.QuickChick.override.version = "2.0.4"; + }; + bundles."8.18" = { + coqPackages.coq.override.version = "8.18"; + coqPackages.metacoq.override.version = "1.3.1-8.18"; + coqPackages.stdpp.override.version = "1.10.0"; + coqPackages.QuickChick.override.version = "2.0.4"; + }; + bundles."8.19" = { + coqPackages.coq.override.version = "8.19"; + coqPackages.metacoq.override.version = "1.3.1-8.19"; + coqPackages.stdpp.override.version = "1.10.0"; + coqPackages.QuickChick.override.version = "2.0.4"; + }; + + ## Cachix caches to use in CI + ## Below we list some standard ones + cachix.coq = {}; + cachix.coq-community = {}; + cachix.metacoq = {}; + + ## If you have write access to one of these caches you can + ## provide the auth token or signing key through a secret + ## 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.coq-community.authToken = "CACHIX_AUTH_TOKEN"; + + ## Or if you have a signing key for a given Cachix cache: + # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" + + ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY + ## are the names of secret variables. They are set in + ## GitHub's web interface. +} diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix new file mode 100644 index 00000000..58de04d0 --- /dev/null +++ b/.nix/coq-nix-toolbox.nix @@ -0,0 +1 @@ +"6325dec49c36d36c17b8cbfc80efe1e4cef972b5" diff --git a/.nix/coq-overlays/ConCert/default.nix b/.nix/coq-overlays/ConCert/default.nix new file mode 100644 index 00000000..d857104c --- /dev/null +++ b/.nix/coq-overlays/ConCert/default.nix @@ -0,0 +1,40 @@ +{ lib, mkCoqDerivation, which, coq + , metacoq, bignums, QuickChick, stdpp, RustExtraction, ElmExtraction + , version ? null }: + +with lib; mkCoqDerivation { + pname = "ConCert"; + repo = "ConCert"; + owner = "AU-COBRA"; + domain = "github.com"; + + inherit version; + ## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged + ## for local usage since it will be ignored locally if + ## - this derivation corresponds to the main attribute, + ## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`. + defaultVersion = with versions; switch coq.coq-version [ + ## Example of possible dependencies + # { case = range "8.13" "8.14"; out = "1.2.0"; } + ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc + ] null; + + ## Declare existing releases + ## leave sha256 empty at first and then copy paste + ## the resulting sha given by the error message + # release."1.1.1".sha256 = ""; + ## if the tag is not exactly the version number you can amend like this + # release."1.1.1".rev = "v1.1.1"; + ## if a consistent scheme gives the tag from the release number, you can do like this: + # releaseRev = v: "v${v}"; + + propagatedBuildInputs = [ coq.ocamlPackages.findlib metacoq bignums QuickChick stdpp RustExtraction ElmExtraction ]; + + postPatch = ''patchShebangs ./extraction/process-extraction-examples.sh''; + + meta = { + description = "A framework for smart contract verification in Coq"; + maintainers = with maintainers; [ _4ever2 ]; + license = licenses.mit; + }; +} diff --git a/default.nix b/default.nix new file mode 100644 index 00000000..1a24d7a1 --- /dev/null +++ b/default.nix @@ -0,0 +1,12 @@ +{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, + update-nixpkgs ? false, ci-matrix ? false, + override ? {}, ocaml-override ? {}, global-override ? {}, + bundle ? null, job ? null, inNixShell ? null, src ? ./., +}@args: +let auto = fetchGit { + url = "https://github.com/coq-community/coq-nix-toolbox.git"; + ref = "master"; + rev = import .nix/coq-nix-toolbox.nix; +}; +in +import auto ({inherit src;} // args) From 3e7c00851e7e028cc41581b7f12958d23754f1de Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Wed, 10 Jul 2024 02:17:08 +0200 Subject: [PATCH 02/10] Include examples in all make target --- .github/coq-concert.opam.locked | 2 +- Makefile | 5 ++++- coq-concert.opam | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/.github/coq-concert.opam.locked b/.github/coq-concert.opam.locked index 1eb968bc..e59c9536 100644 --- a/.github/coq-concert.opam.locked +++ b/.github/coq-concert.opam.locked @@ -34,7 +34,7 @@ pin-depends: [ ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"] ] build: [ - [make] + [make "core"] [make "examples"] {with-test} [make "html"] {with-doc} ] diff --git a/Makefile b/Makefile index 7fe981cc..747da0bd 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,9 @@ -all: utils execution embedding extraction +all: utils execution embedding extraction examples .PHONY: all +core: utils execution embedding extraction +.PHONY: core + utils: +make -C utils .PHONY: utils diff --git a/coq-concert.opam b/coq-concert.opam index 5ba4bd18..546b7fc8 100644 --- a/coq-concert.opam +++ b/coq-concert.opam @@ -40,7 +40,7 @@ pin-depends: [ ] build: [ - [make] + [make "core"] [make "examples"] {with-test} [make "html"] {with-doc} ] From 604251f3912465a766b64551dd8b9f292c53d848 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Wed, 10 Jul 2024 15:33:33 +0200 Subject: [PATCH 03/10] Update gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index 8b63802c..6cb138e6 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,9 @@ *.tmp .DS_Store +# Nix outputs +result + # dpd-graph outputs *.dpd *.dot From 31ed24d512fec7d73cb65eeefdb38d574c61e057 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Mon, 14 Oct 2024 15:59:37 +0200 Subject: [PATCH 04/10] Add cachix token --- .github/workflows/nix-action-8.17.yml | 35 ++++++++++++--------- .github/workflows/nix-action-8.18.yml | 35 ++++++++++++--------- .github/workflows/nix-action-8.19.yml | 35 ++++++++++++--------- .nix/config.nix | 45 +-------------------------- 4 files changed, 61 insertions(+), 89 deletions(-) diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml index 9ce97ba9..d2ddb30d 100644 --- a/.github/workflows/nix-action-8.17.yml +++ b/.github/workflows/nix-action-8.17.yml @@ -34,11 +34,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target ConCert run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -109,11 +110,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target QuickChick run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -171,11 +173,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -218,11 +221,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target metacoq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -289,11 +293,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target stdpp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 3abfb0d1..6979d588 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -34,11 +34,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target ConCert run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -109,11 +110,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target QuickChick run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -171,11 +173,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -218,11 +221,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target metacoq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -289,11 +293,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target stdpp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 6e5e3dab..01f4521e 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -34,11 +34,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target ConCert run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -109,11 +110,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target QuickChick run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -171,11 +173,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -218,11 +221,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target metacoq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ @@ -289,11 +293,12 @@ jobs: uses: cachix/install-nix-action@v27 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq + - name: Cachix setup au-cobra uses: cachix/cachix-action@v15 with: - extraPullNames: coq-community, metacoq - name: coq + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra - id: stepCheck name: Checking presence of CI target stdpp 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 f4cb7aa0..d0c220b4 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -4,39 +4,10 @@ ## unless you made an automated or manual update ## to another supported format. - ## The attribute to build from the local sources, - ## either using nixpkgs data or the overlays located in `.nix/coq-overlays` - ## Will determine the default main-job of the bundles defined below attribute = "ConCert"; - ## If you want to select a different attribute (to build from the local sources as well) - ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument - # shell-attribute = "{{nix_name}}"; - - ## Maybe the shortname of the library is different from - ## the name of the nixpkgs attribute, if so, set it here: - # pname = "ConCert"; - - ## Lists the dependencies, phrased in terms of nix attributes. - ## No need to list Coq, it is already included. - ## These dependencies will systematically be added to the currently - ## known dependencies, if any more than Coq. - ## /!\ Remove this field as soon as the package is available on nixpkgs. - ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. - # buildInputs = [ ]; - - ## Indicate the relative location of your _CoqProject - ## If not specified, it defaults to "_CoqProject" - # coqproject = "_CoqProject"; - - ## select an entry to build in the following `bundles` set - ## defaults to "default" default-bundle = "8.17"; - ## write one `bundles.name` attribute set per - ## alternative configuration - ## When generating GitHub Action CI, one workflow file - ## will be created per bundle bundles."8.17" = { coqPackages.coq.override.version = "8.17"; coqPackages.metacoq.override.version = "1.3.1-8.17"; @@ -56,23 +27,9 @@ coqPackages.QuickChick.override.version = "2.0.4"; }; - ## Cachix caches to use in CI - ## Below we list some standard ones cachix.coq = {}; cachix.coq-community = {}; cachix.metacoq = {}; - ## If you have write access to one of these caches you can - ## provide the auth token or signing key through a secret - ## 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.coq-community.authToken = "CACHIX_AUTH_TOKEN"; - - ## Or if you have a signing key for a given Cachix cache: - # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" - - ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY - ## are the names of secret variables. They are set in - ## GitHub's web interface. + cachix.au-cobra.authToken = "CACHIX_AUTH_TOKEN"; } From 48b140380c0b3a19e2cc6ad4b56ffab49f7764ae Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Mon, 14 Oct 2024 16:01:46 +0200 Subject: [PATCH 05/10] Don't run build job on nix changes --- .github/workflows/build.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a5add0f4..7c973de2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,6 +8,7 @@ on: - '**.md' - '**.gitignore' - '**.opam' + - '**.nix' - '**.editorconfig' - 'LICENSE' - 'papers/**' @@ -17,6 +18,7 @@ on: - '**.md' - '**.gitignore' - '**.opam' + - '**.nix' - '**.editorconfig' - 'LICENSE' - 'papers/**' From b2c55df5df766af19a610f4c950680dd21c85e17 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Tue, 15 Oct 2024 12:27:09 +0200 Subject: [PATCH 06/10] Add concurrency groups --- .github/workflows/nix-action-8.17.yml | 22 +++++++++++++++++----- .github/workflows/nix-action-8.18.yml | 22 +++++++++++++++++----- .github/workflows/nix-action-8.19.yml | 22 +++++++++++++++++----- 3 files changed, 51 insertions(+), 15 deletions(-) diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml index d2ddb30d..f5e6adb9 100644 --- a/.github/workflows/nix-action-8.17.yml +++ b/.github/workflows/nix-action-8.17.yml @@ -31,7 +31,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -107,7 +107,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -170,7 +170,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -218,7 +218,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -290,7 +290,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -321,6 +321,13 @@ name: Nix CI for bundle 8.17 pull_request_target: paths-ignore: - .github/workflows/nix-action-8.17.yml + - '**.md' + - '**.gitignore' + - '**.opam' + - '**.editorconfig' + - 'LICENSE' + - 'papers/**' + - 'extra/docker/**' types: - opened - synchronize @@ -328,3 +335,8 @@ name: Nix CI for bundle 8.17 push: branches: - master +concurrency: + group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}" + cancel-in-progress: true +permissions: + contents: read diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml index 6979d588..71df3a65 100644 --- a/.github/workflows/nix-action-8.18.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -31,7 +31,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -107,7 +107,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -170,7 +170,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -218,7 +218,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -290,7 +290,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -321,6 +321,13 @@ name: Nix CI for bundle 8.18 pull_request_target: paths-ignore: - .github/workflows/nix-action-8.18.yml + - '**.md' + - '**.gitignore' + - '**.opam' + - '**.editorconfig' + - 'LICENSE' + - 'papers/**' + - 'extra/docker/**' types: - opened - synchronize @@ -328,3 +335,8 @@ name: Nix CI for bundle 8.18 push: branches: - master +concurrency: + group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}" + cancel-in-progress: true +permissions: + contents: read diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 01f4521e..fc71390a 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -31,7 +31,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -107,7 +107,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -170,7 +170,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -218,7 +218,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -290,7 +290,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v27 + uses: cachix/install-nix-action@v30 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup au-cobra @@ -321,6 +321,13 @@ name: Nix CI for bundle 8.19 pull_request_target: paths-ignore: - .github/workflows/nix-action-8.19.yml + - '**.md' + - '**.gitignore' + - '**.opam' + - '**.editorconfig' + - 'LICENSE' + - 'papers/**' + - 'extra/docker/**' types: - opened - synchronize @@ -328,3 +335,8 @@ name: Nix CI for bundle 8.19 push: branches: - master +concurrency: + group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}" + cancel-in-progress: true +permissions: + contents: read From bcebb2319b466a8ae156a74d8cb973b603d474ee Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Thu, 16 Jan 2025 21:21:02 +0100 Subject: [PATCH 07/10] Use MetaCoq 8.19 branch rather than Nix release --- .nix/config.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/config.nix b/.nix/config.nix index d0c220b4..acd0f0f9 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -22,7 +22,7 @@ }; bundles."8.19" = { coqPackages.coq.override.version = "8.19"; - coqPackages.metacoq.override.version = "1.3.1-8.19"; + coqPackages.metacoq.override.version = "coq-8.19"; coqPackages.stdpp.override.version = "1.10.0"; coqPackages.QuickChick.override.version = "2.0.4"; }; From 1a4e3e4833263684881d35db68a02dd8f81a54ba Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Thu, 16 Jan 2025 21:24:29 +0100 Subject: [PATCH 08/10] Remove Coq 8.17 and 8.18 Nix workflows --- .github/workflows/nix-action-8.17.yml | 342 -------------------------- .github/workflows/nix-action-8.18.yml | 342 -------------------------- .nix/config.nix | 14 +- 3 files changed, 1 insertion(+), 697 deletions(-) delete mode 100644 .github/workflows/nix-action-8.17.yml delete mode 100644 .github/workflows/nix-action-8.18.yml diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml deleted file mode 100644 index f5e6adb9..00000000 --- a/.github/workflows/nix-action-8.17.yml +++ /dev/null @@ -1,342 +0,0 @@ -jobs: - ConCert: - needs: - - coq - - metacoq - - QuickChick - - stdpp - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - id: stepCheck - name: Checking presence of CI target ConCert - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"ConCert\" \\\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 "8.17" --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 "8.17" --argstr - job "metacoq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: QuickChick' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "QuickChick" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdpp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "stdpp" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: RustExtraction' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "RustExtraction" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: ElmExtraction' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "ElmExtraction" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "ConCert" - QuickChick: - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - id: stepCheck - name: Checking presence of CI target QuickChick - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"QuickChick\" \\\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 "8.17" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-ext-lib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "coq-ext-lib" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: simple-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "simple-io" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "QuickChick" - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - 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 \"8.17\" --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 "8.17" --argstr - job "coq" - metacoq: - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - 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 \"8.17\" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --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 "8.17" --argstr - job "metacoq" - stdpp: - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - id: stepCheck - name: Checking presence of CI target stdpp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"stdpp\" \\\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 "8.17" --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 "8.17" --argstr - job "stdpp" -name: Nix CI for bundle 8.17 -'on': - pull_request: - paths: - - .github/workflows/nix-action-8.17.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.17.yml - - '**.md' - - '**.gitignore' - - '**.opam' - - '**.editorconfig' - - 'LICENSE' - - 'papers/**' - - 'extra/docker/**' - types: - - opened - - synchronize - - reopened - push: - branches: - - master -concurrency: - group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}" - cancel-in-progress: true -permissions: - contents: read diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml deleted file mode 100644 index 71df3a65..00000000 --- a/.github/workflows/nix-action-8.18.yml +++ /dev/null @@ -1,342 +0,0 @@ -jobs: - ConCert: - needs: - - coq - - metacoq - - QuickChick - - stdpp - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - id: stepCheck - name: Checking presence of CI target ConCert - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"ConCert\" \\\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 "8.18" --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 "8.18" --argstr - job "metacoq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: QuickChick' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "QuickChick" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdpp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "stdpp" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: RustExtraction' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "RustExtraction" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: ElmExtraction' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "ElmExtraction" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "ConCert" - QuickChick: - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - id: stepCheck - name: Checking presence of CI target QuickChick - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"QuickChick\" \\\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 "8.18" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-ext-lib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "coq-ext-lib" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: simple-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "simple-io" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr - job "QuickChick" - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - 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 \"8.18\" --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 "8.18" --argstr - job "coq" - metacoq: - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - 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 \"8.18\" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --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 "8.18" --argstr - job "metacoq" - stdpp: - 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 au-cobra - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, metacoq - name: au-cobra - - id: stepCheck - name: Checking presence of CI target stdpp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.18\" --argstr job \"stdpp\" \\\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 "8.18" --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 "8.18" --argstr - job "stdpp" -name: Nix CI for bundle 8.18 -'on': - pull_request: - paths: - - .github/workflows/nix-action-8.18.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.18.yml - - '**.md' - - '**.gitignore' - - '**.opam' - - '**.editorconfig' - - 'LICENSE' - - 'papers/**' - - 'extra/docker/**' - types: - - opened - - synchronize - - reopened - push: - branches: - - master -concurrency: - group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}" - cancel-in-progress: true -permissions: - contents: read diff --git a/.nix/config.nix b/.nix/config.nix index acd0f0f9..0a180bd3 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -6,20 +6,8 @@ attribute = "ConCert"; - default-bundle = "8.17"; + default-bundle = "8.19"; - bundles."8.17" = { - coqPackages.coq.override.version = "8.17"; - coqPackages.metacoq.override.version = "1.3.1-8.17"; - coqPackages.stdpp.override.version = "1.10.0"; - coqPackages.QuickChick.override.version = "2.0.4"; - }; - bundles."8.18" = { - coqPackages.coq.override.version = "8.18"; - coqPackages.metacoq.override.version = "1.3.1-8.18"; - coqPackages.stdpp.override.version = "1.10.0"; - coqPackages.QuickChick.override.version = "2.0.4"; - }; bundles."8.19" = { coqPackages.coq.override.version = "8.19"; coqPackages.metacoq.override.version = "coq-8.19"; From a937ea37f2f444229f8fe2ea748a62e15f1773ee Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Thu, 16 Jan 2025 21:45:13 +0100 Subject: [PATCH 09/10] Update coq-nix-toolbox --- .github/workflows/nix-action-8.19.yml | 164 +++++++++++++------------- .nix/coq-nix-toolbox.nix | 2 +- 2 files changed, 81 insertions(+), 85 deletions(-) diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index fc71390a..0dfda838 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -8,23 +8,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: @@ -42,8 +42,8 @@ jobs: name: au-cobra - id: stepCheck name: Checking presence of CI target ConCert - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"ConCert\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"ConCert\" \\\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' @@ -66,14 +66,6 @@ jobs: name: 'Building/fetching previous CI target: stdpp' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "stdpp" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: RustExtraction' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "RustExtraction" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: ElmExtraction' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "ElmExtraction" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -84,23 +76,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: @@ -118,8 +110,8 @@ jobs: name: au-cobra - id: stepCheck name: Checking presence of CI target QuickChick - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"QuickChick\" \\\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' @@ -131,9 +123,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-ext-lib' + name: 'Building/fetching previous CI target: ExtLib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "coq-ext-lib" + job "ExtLib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: simple-io' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -147,23 +139,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: @@ -181,8 +173,8 @@ jobs: name: au-cobra - 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 \"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 \"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' @@ -195,23 +187,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: @@ -229,8 +221,8 @@ jobs: name: au-cobra - 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 \"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 \"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' @@ -242,21 +234,21 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "equations" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-template-coq' + name: 'Building/fetching previous CI target: metacoq-safechecker-plugin' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "metacoq-template-coq" + job "metacoq-safechecker-plugin" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-pcuic' + name: 'Building/fetching previous CI target: metacoq-erasure-plugin' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "metacoq-pcuic" + job "metacoq-erasure-plugin" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-safechecker' + name: 'Building/fetching previous CI target: metacoq-translations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "metacoq-safechecker" + job "metacoq-translations" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: metacoq-erasure' + name: 'Building/fetching previous CI target: metacoq-quotation' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "metacoq-erasure" + 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 "8.19" --argstr @@ -267,23 +259,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: @@ -301,20 +293,24 @@ jobs: name: au-cobra - id: stepCheck name: Checking presence of CI target stdpp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"stdpp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"stdpp\" \\\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 "8.19" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "stdpp" name: Nix CI for bundle 8.19 -'on': +on: pull_request: paths: - .github/workflows/nix-action-8.19.yml diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 58de04d0..12ed0a44 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"6325dec49c36d36c17b8cbfc80efe1e4cef972b5" +"a24e6f4fb01d4ca0811dc8d16246cfe36b37ac52" From 178c65d3654062f514572d9ba37c53d65ee92a1d Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Thu, 16 Jan 2025 23:07:15 +0100 Subject: [PATCH 10/10] Add extraction dependencies --- .github/workflows/nix-action-8.19.yml | 136 +++++++++++++++++++++++--- .nix/config.nix | 2 + 2 files changed, 126 insertions(+), 12 deletions(-) diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 0dfda838..4a557e24 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -5,6 +5,8 @@ jobs: - metacoq - QuickChick - stdpp + - RustExtraction + - ElmExtraction runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -66,10 +68,75 @@ jobs: name: 'Building/fetching previous CI target: stdpp' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "stdpp" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: RustExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "RustExtraction" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: ElmExtraction' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "ElmExtraction" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "ConCert" + 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 au-cobra + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra + - 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 \"8.19\" --argstr job \"ElmExtraction\" \\\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 "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 "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 "8.19" --argstr + job "ElmExtraction" QuickChick: needs: - coq @@ -134,6 +201,63 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "QuickChick" + 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 au-cobra + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, metacoq + name: au-cobra + - 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 \"8.19\" --argstr job \"RustExtraction\" \\\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 "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 "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 "8.19" --argstr + job "RustExtraction" coq: needs: [] runs-on: ubuntu-latest @@ -317,13 +441,6 @@ on: pull_request_target: paths-ignore: - .github/workflows/nix-action-8.19.yml - - '**.md' - - '**.gitignore' - - '**.opam' - - '**.editorconfig' - - 'LICENSE' - - 'papers/**' - - 'extra/docker/**' types: - opened - synchronize @@ -331,8 +448,3 @@ on: push: branches: - master -concurrency: - group: "${{ github.workflow }}-${{ github.event.pull_request.number || github.head_ref || github.ref }}" - cancel-in-progress: true -permissions: - contents: read diff --git a/.nix/config.nix b/.nix/config.nix index 0a180bd3..cc6fc641 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -13,6 +13,8 @@ coqPackages.metacoq.override.version = "coq-8.19"; coqPackages.stdpp.override.version = "1.10.0"; coqPackages.QuickChick.override.version = "2.0.4"; + coqPackages.RustExtraction.override.version = "0.1.0"; + coqPackages.ElmExtraction.override.version = "0.1.0"; }; cachix.coq = {};