diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index 4b655c446c..f771af55dd 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -589,12 +589,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "argosy" - async-test: + atbr: needs: - coq - - itree-io - - json - - QuickChick + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -631,11 +629,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (async-test) + name: Getting derivation for current job (atbr) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"async-test\" \\\n --dry-run 2> err > out || - (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.1\" --argstr job \"atbr\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -648,21 +646,13 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: itree-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "itree-io" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: json' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "json" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: QuickChick' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "QuickChick" + "rocq-9.1" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "async-test" + "rocq-9.1" --argstr job "atbr" autosubst: needs: - coq @@ -859,70 +849,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "bignums-test" - ceres: - needs: - - coq - - stdlib - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (ceres) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"ceres\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "stdlib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "ceres" coinduction: needs: - coq @@ -1699,213 +1625,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "flocq" - http: - needs: - - coq - - QuickChick - - async-test - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (http) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"http\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: QuickChick' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "QuickChick" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: async-test' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "async-test" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "http" - itree-io: - needs: - - coq - - ITree - - simple-io - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (itree-io) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"itree-io\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ITree' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "ITree" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: simple-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "simple-io" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "itree-io" - json: - needs: - - coq - - parsec - - MenhirLib - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (json) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"json\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: parsec' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "parsec" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: MenhirLib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "MenhirLib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "json" math-classes: needs: - coq @@ -3111,75 +2830,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "paramcoq-test" - parsec: - needs: - - coq - - ceres - - ExtLib - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (parsec) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.1\" --argstr job \"parsec\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ceres' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "ceres" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ExtLib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "ExtLib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "parsec" quickchick-test: needs: - coq @@ -3608,6 +3258,134 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "smtcoq" + stalmarck: + needs: + - coq + - stdlib + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (stalmarck) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1\" --argstr job \"stalmarck\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "stalmarck" + stalmarck-tactic: + needs: + - coq + - stalmarck + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (stalmarck-tactic) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1\" --argstr job \"stalmarck-tactic\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stalmarck' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "stalmarck" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "stalmarck-tactic" stdlib: needs: - rocq-core diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 2564d3ef92..7a1e55ee66 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -516,9 +516,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "argosy" - bignums: + atbr: needs: - - rocq-core + - coq - stdlib runs-on: ubuntu-latest steps: @@ -556,9 +556,9 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (bignums) + name: Getting derivation for current job (atbr) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch + \"rocq-9.2\" --argstr job \"atbr\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -569,9 +569,9 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: rocq-core' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "rocq-core" + "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -579,11 +579,11 @@ jobs: - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "bignums" - bignums-test: + "rocq-9.2" --argstr job "atbr" + bignums: needs: - - coq - - bignums + - rocq-core + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -620,11 +620,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (bignums-test) + name: Getting derivation for current job (bignums) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"bignums-test\" \\\n --dry-run 2> err > out || - (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -633,21 +633,21 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: bignums' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "bignums" + "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "bignums-test" - ceres: + "rocq-9.2" --argstr job "bignums" + bignums-test: needs: - coq - - stdlib + - bignums runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -684,11 +684,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (ceres) + name: Getting derivation for current job (bignums-test) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"ceres\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"bignums-test\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -701,13 +701,13 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' + name: 'Building/fetching previous CI target: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "stdlib" + "rocq-9.2" --argstr job "bignums" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "ceres" + "rocq-9.2" --argstr job "bignums-test" coinduction: needs: - coq @@ -1279,11 +1279,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "flocq" - itree-io: + math-classes: needs: - coq - - ITree - - simple-io + - bignums runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1320,11 +1319,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (itree-io) + name: Getting derivation for current job (math-classes) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"itree-io\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"math-classes\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -1337,22 +1336,18 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ITree' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "ITree" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: simple-io' + name: 'Building/fetching previous CI target: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "simple-io" + "rocq-9.2" --argstr job "bignums" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "itree-io" - json: + "rocq-9.2" --argstr job "math-classes" + mtac2: needs: - coq - - parsec - - MenhirLib + - unicoq + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1389,9 +1384,9 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (json) + name: Getting derivation for current job (mtac2) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"json\" \\\n --dry-run 2> err > out || (touch + \"rocq-9.2\" --argstr job \"mtac2\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -1406,21 +1401,21 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: parsec' + name: 'Building/fetching previous CI target: unicoq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "parsec" + "rocq-9.2" --argstr job "unicoq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: MenhirLib' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "MenhirLib" + "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "json" - math-classes: + "rocq-9.2" --argstr job "mtac2" + neural-net-coq-interp: needs: - coq - - bignums + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1457,11 +1452,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (math-classes) + name: Getting derivation for current job (neural-net-coq-interp) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"math-classes\" \\\n --dry-run 2> err > out || - (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"neural-net-coq-interp\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -1474,17 +1469,16 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: bignums' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "bignums" + "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "math-classes" - mtac2: + "rocq-9.2" --argstr job "neural-net-coq-interp" + paco: needs: - coq - - unicoq - stdlib runs-on: ubuntu-latest steps: @@ -1522,9 +1516,9 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (mtac2) + name: Getting derivation for current job (paco) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"mtac2\" \\\n --dry-run 2> err > out || (touch + \"rocq-9.2\" --argstr job \"paco\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -1538,10 +1532,6 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: unicoq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "unicoq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1549,8 +1539,8 @@ jobs: - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "mtac2" - neural-net-coq-interp: + "rocq-9.2" --argstr job "paco" + paramcoq-test: needs: - coq - stdlib @@ -1590,11 +1580,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (neural-net-coq-interp) + name: Getting derivation for current job (paramcoq-test) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"neural-net-coq-interp\" \\\n --dry-run 2> err - > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: - getting derivation failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"paramcoq-test\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -1613,11 +1603,9 @@ jobs: - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "neural-net-coq-interp" - paco: - needs: - - coq - - stdlib + "rocq-9.2" --argstr job "paramcoq-test" + rocq-core: + needs: [] runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1654,9 +1642,9 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (paco) + name: Getting derivation for current job (rocq-core) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"paco\" \\\n --dry-run 2> err > out || (touch + \"rocq-9.2\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -1666,22 +1654,12 @@ jobs: ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "paco" - paramcoq-test: - needs: - - coq - - stdlib + "rocq-9.2" --argstr job "rocq-core" + rocq-elpi: + needs: [] runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1718,11 +1696,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (paramcoq-test) + name: Getting derivation for current job (rocq-elpi) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"paramcoq-test\" \\\n --dry-run 2> err > out - || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"rocq-elpi\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -1730,23 +1708,14 @@ jobs: ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "paramcoq-test" - parsec: + "rocq-9.2" --argstr job "rocq-elpi" + rocq-lean-import: needs: - coq - - ceres - - ExtLib + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1783,11 +1752,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (parsec) + name: Getting derivation for current job (rocq-lean-import) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"parsec\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"rocq-lean-import\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -1800,19 +1769,17 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ceres' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "ceres" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ExtLib' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "ExtLib" + "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "parsec" - rocq-core: - needs: [] + "rocq-9.2" --argstr job "rocq-lean-import" + simple-io: + needs: + - coq + - ExtLib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1849,9 +1816,9 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (rocq-core) + name: Getting derivation for current job (simple-io) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch + \"rocq-9.2\" --argstr job \"simple-io\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -1862,64 +1829,18 @@ jobs: \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "rocq-core" - rocq-elpi: - 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@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (rocq-elpi) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"rocq-elpi\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + "rocq-9.2" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: ExtLib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "ExtLib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "rocq-elpi" - rocq-lean-import: + "rocq-9.2" --argstr job "simple-io" + smtcoq: needs: - coq - stdlib @@ -1959,11 +1880,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (rocq-lean-import) + name: Getting derivation for current job (smtcoq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"rocq-lean-import\" \\\n --dry-run 2> err > out - || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"smtcoq\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -1982,11 +1903,11 @@ jobs: - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "rocq-lean-import" - simple-io: + "rocq-9.2" --argstr job "smtcoq" + stalmarck: needs: - coq - - ExtLib + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2023,9 +1944,9 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (simple-io) + name: Getting derivation for current job (stalmarck) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"simple-io\" \\\n --dry-run 2> err > out || (touch + \"rocq-9.2\" --argstr job \"stalmarck\" \\\n --dry-run 2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation failed\"; exit 1; fi\n" - id: stepCheck @@ -2040,17 +1961,17 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ExtLib' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "ExtLib" + "rocq-9.2" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "simple-io" - smtcoq: + "rocq-9.2" --argstr job "stalmarck" + stalmarck-tactic: needs: - coq - - stdlib + - stalmarck runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2087,11 +2008,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (smtcoq) + name: Getting derivation for current job (stalmarck-tactic) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.2\" --argstr job \"smtcoq\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" + \"rocq-9.2\" --argstr job \"stalmarck-tactic\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -2104,13 +2025,13 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' + name: 'Building/fetching previous CI target: stalmarck' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "stdlib" + "rocq-9.2" --argstr job "stalmarck" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "smtcoq" + "rocq-9.2" --argstr job "stalmarck-tactic" stdlib: needs: - rocq-core diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index ecda28fa9f..722aa0ce41 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -530,12 +530,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "argosy" - async-test: + atbr: needs: - coq - - itree-io - - json - - QuickChick + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -572,11 +570,11 @@ jobs: extraPullNames: coq-community, math-comp name: coq - id: stepGetDerivation - name: Getting derivation for current job (async-test) + name: Getting derivation for current job (atbr) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"async-test\" \\\n --dry-run 2> err > out - || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" + \"rocq-master\" --argstr job \"atbr\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" - id: stepCheck name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -589,21 +587,13 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: itree-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "itree-io" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: json' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "json" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: QuickChick' + name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "QuickChick" + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "async-test" + "rocq-master" --argstr job "atbr" autosubst: needs: - coq @@ -932,70 +922,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "category-theory" - ceres: - needs: - - coq - - stdlib - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (ceres) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"ceres\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "stdlib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "ceres" coinduction: needs: - coq @@ -2496,75 +2422,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "hierarchy-builder" - http: - needs: - - coq - - QuickChick - - async-test - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (http) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"http\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: QuickChick' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "QuickChick" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: async-test' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "async-test" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "http" iris: needs: - coq @@ -2693,75 +2550,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "itauto" - itree-io: - needs: - - coq - - ITree - - simple-io - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (itree-io) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"itree-io\" \\\n --dry-run 2> err > out || - (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ITree' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "ITree" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: simple-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "simple-io" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "itree-io" jasmin: needs: - coq @@ -2831,75 +2619,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "jasmin" - json: - needs: - - coq - - parsec - - MenhirLib - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (json) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"json\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: parsec' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "parsec" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: MenhirLib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "MenhirLib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "json" math-classes: needs: - coq @@ -5069,75 +4788,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "paramcoq-test" - parsec: - needs: - - coq - - ceres - - ExtLib - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v6 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (parsec) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-master\" --argstr job \"parsec\" \\\n --dry-run 2> err > out || (touch - fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation - failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ceres' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "ceres" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: ExtLib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "ExtLib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "parsec" quickchick-test: needs: - coq @@ -5772,6 +5422,134 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "smtcoq" + stalmarck: + needs: + - coq + - stdlib + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (stalmarck) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"stalmarck\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "stalmarck" + stalmarck-tactic: + needs: + - coq + - stalmarck + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url + }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git + merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null + 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ + \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ + \ fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (stalmarck-tactic) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"stalmarck-tactic\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stalmarck' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "stalmarck" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "stalmarck-tactic" stdlib: needs: - rocq-core diff --git a/.nix/config.nix b/.nix/config.nix index 6b50cdb2ca..7e6dd7572b 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -102,13 +102,12 @@ with builtins; with (import {}).lib; { master = [ "aac-tactics" "argosy" - "async-test" + "atbr" "autosubst" "bedrock2" "bignums" "bignums-test" "category-theory" - "ceres" "coinduction" "CoLoR" "compcert" @@ -129,13 +128,10 @@ with builtins; with (import {}).lib; { "fiat-parsers" "flocq" "hierarchy-builder" - "http" "iris" "iris-examples" "itauto" "ITree" - "itree-io" - "json" "mathcomp-algebra-tactics" "mathcomp-analysis" "mathcomp-reals" @@ -146,7 +142,6 @@ with builtins; with (import {}).lib; { "neural-net-coq-interp" "paco" "paramcoq-test" - "parsec" "QuickChick" "quickchick-test" "relation-algebra" @@ -155,6 +150,7 @@ with builtins; with (import {}).lib; { "rupicola" "sf" "simple-io" + "stalmarck-tactic" "stdpp" "trakt" "unicoq" @@ -227,6 +223,7 @@ with builtins; with (import {}).lib; { rocq-elpi.job = true; iris-examples.job = false; # Currently broken CakeMLExtraction.job = false; # not in Rocq CI + ceres.job = false; # not in Rocq CI ceres-bs.job = false; # not in Rocq CI CertiRocq.job = false; # not in Rocq CI ConCert.job = false; # not in Rocq CI @@ -235,8 +232,10 @@ with builtins; with (import {}).lib; { extructures.job = false; # not in Rocq CI gaia.job = false; # not in Rocq CI graph-theory.job = false; # not in Rocq CI + json.job = false; # not in Rocq CI libvalidsdp.job = false; # not in Rocq CI Ordinal.job = false; # not in Rocq CI + parsec.job = false; # not in Rocq CI RustExtraction.job = false; # not in Rocq CI interval.job = false; # not in Rocq CI parseque.job = false; # not in Rocq CI @@ -302,12 +301,10 @@ with builtins; with (import {}).lib; { bignums.override.version = "30a45625546da0a88db8689a8009d580aa3f557f"; stdlib-test.job = false; autosubst.job = false; # no release for 9.2 yet - async-test.job = false; # no release for 9.2 yet coquelicot.job = false; # no release for 9.2 yet deriving.job = false; # no release for 9.2 yet fcsl-pcm.job = false; # no release for 9.2 yet hierarchy-builder.job = false; # no release for 9.2 yet - http.job = false; # no release for 9.2 yet mathcomp.job = false; # no release for 9.2 yet mathcomp-algebra.job = false; # no release for 9.2 yet mathcomp-algebra-tactics.job = false; # no release for 9.2 yet @@ -327,6 +324,7 @@ with builtins; with (import {}).lib; { coq.override.version = "9.2"; # plugin pins, from v9.2 branch of Rocq aac-tactics.override.version = "4f796a7b0ee88330162727fc6ea988a7e0ea46e3"; + atbr.override.version = "47ac8fb6bf244d9a4049e04c01e561191490f543"; bignums.override.version = "30a45625546da0a88db8689a8009d580aa3f557f"; itauto.job = false; # broken coinduction.override.version = "9502ae09e9f87518330f37c08bc19a8c452dcd91"; @@ -344,6 +342,7 @@ with builtins; with (import {}).lib; { rewriter.override.version = "dd37fb28ed7f01a3b7edc0675a86b95dd3eb1545"; rocq-lean-import.override.version = "b8291b9dae4f5ed780112e95eea484e435199b46"; smtcoq.override.version = "cff0a8cdb7c73b6c59965a749a4304f3c4ac01bf"; + stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512"; unicoq.override.version = "d52374ca86e3885197f114555e742420fa9bbe94"; waterproof.override.version = "99ad6ff78fa700c84ba0cb1d1bda27d8e0f11e1a"; compcert.job = false; # broken @@ -359,6 +358,7 @@ with builtins; with (import {}).lib; { coq.override.version = "9.1"; # plugin pins, from v9.1 branch of Rocq aac-tactics.override.version = "e68d028cef838f5821d184fed0caea9eedd5538a"; + atbr.override.version = "47ac8fb6bf244d9a4049e04c01e561191490f543"; bignums.override.version = "9f9855536bd4167af6986f826819e32354b7da22"; itauto.job = false; # broken coinduction.override.version = "823b424778feff8fbd9759bc3a044435ea4902d1"; @@ -376,6 +376,7 @@ with builtins; with (import {}).lib; { rewriter.override.version = "9496defb8b236f442d11372f6e0b5e48aa38acfc"; rocq-lean-import.override.version = "c3546102f242aaa1e9af921c78bdb1132522e444"; smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514"; + stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512"; unicoq.override.version = "28ec18aef35877829535316fc09825a25be8edf1"; waterproof.override.version = "dd712eb0b7f5c205870dbd156736a684d40eeb9a"; compcert.job = false; # broken