diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 7fec0c2057..5e1167cc9c 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -860,6 +860,76 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "coqprime" + coquelicot: + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (coquelicot) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"coquelicot\" \\\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.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 previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-boot" + - 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 "coquelicot" coqutil: needs: - coq @@ -1060,7 +1130,7 @@ jobs: "rocq-9.2" --argstr job "equations" flocq: needs: - - coq + - rocq-core - stdlib runs-on: ubuntu-latest steps: @@ -1113,9 +1183,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: 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: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1643,6 +1713,164 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-reals-stdlib" + mathcomp-word: + needs: + - coq + - mathcomp-algebra + - 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (mathcomp-word) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"mathcomp-word\" \\\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.2" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-fingroup" + - 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 "mathcomp-word" + mathcomp-zify: + needs: + - rocq-core + - mathcomp-algebra + - 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (mathcomp-zify) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"mathcomp-zify\" \\\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: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-fingroup" + - 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 "mathcomp-zify" neural-net-coq-interp: needs: - coq @@ -1841,6 +2069,81 @@ jobs: 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" + relation-algebra: + needs: + - rocq-core + - aac-tactics + - 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (relation-algebra) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"relation-algebra\" \\\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: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: aac-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "aac-tactics" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-boot" + - 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 "relation-algebra" rocq-core: needs: [] runs-on: ubuntu-latest @@ -2622,3 +2925,5 @@ on: push: branches: - master +permissions: + contents: read diff --git a/.github/workflows/nix-action-rocq-9.3.yml b/.github/workflows/nix-action-rocq-9.3.yml index a2d214cbc9..2d5d749ff5 100644 --- a/.github/workflows/nix-action-rocq-9.3.yml +++ b/.github/workflows/nix-action-rocq-9.3.yml @@ -860,6 +860,76 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.3" --argstr job "coqprime" + coquelicot: + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (coquelicot) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.3\" --argstr job \"coquelicot\" \\\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.3" --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.3" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-boot" + - 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.3" --argstr job "coquelicot" coqutil: needs: - coq @@ -1060,7 +1130,7 @@ jobs: "rocq-9.3" --argstr job "equations" flocq: needs: - - coq + - rocq-core - stdlib runs-on: ubuntu-latest steps: @@ -1113,9 +1183,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: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.3" --argstr job "coq" + "rocq-9.3" --argstr job "rocq-core" - 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 @@ -1643,6 +1713,164 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.3" --argstr job "mathcomp-reals-stdlib" + mathcomp-word: + needs: + - coq + - mathcomp-algebra + - 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (mathcomp-word) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.3\" --argstr job \"mathcomp-word\" \\\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.3" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-fingroup" + - 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.3" --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.3" --argstr job "mathcomp-word" + mathcomp-zify: + needs: + - rocq-core + - mathcomp-algebra + - 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@v7 + with: + allow-unsafe-pr-checkout: true + 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@v7 + with: + allow-unsafe-pr-checkout: true + 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 (mathcomp-zify) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.3\" --argstr job \"mathcomp-zify\" \\\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: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.3" --argstr job "mathcomp-fingroup" + - 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.3" --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.3" --argstr job "mathcomp-zify" mtac2: needs: - coq @@ -2810,3 +3038,5 @@ on: push: branches: - master +permissions: + contents: read diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 5fb11972bd..05435d503f 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -2307,7 +2307,7 @@ jobs: "rocq-master" --argstr job "fiat-parsers" flocq: needs: - - coq + - rocq-core - stdlib runs-on: ubuntu-latest steps: @@ -2360,9 +2360,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: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - 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 @@ -3589,7 +3589,7 @@ jobs: "rocq-master" --argstr job "mathcomp-word" mathcomp-zify: needs: - - coq + - rocq-core - mathcomp-algebra - stdlib runs-on: ubuntu-latest @@ -3643,9 +3643,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: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -6401,3 +6401,5 @@ on: push: branches: - master +permissions: + contents: read diff --git a/.nix/config.nix b/.nix/config.nix index eb1422c628..aa34e6d724 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -298,12 +298,9 @@ with builtins; with (import {}).lib; { bignums.override.version = "36cd7009759b797b9b248ca91959e11494e89a4a"; stdlib-test.job = false; autosubst.job = false; # no release for 9.3 yet - coquelicot.job = false; # no release for 9.3 yet deriving.job = false; # no release for 9.3 yet fcsl-pcm.job = false; # no release for 9.3 yet mathcomp-algebra-tactics.job = false; # no release for 9.3 yet - mathcomp-word.job = false; # no release for 9.3 yet - mathcomp-zify.job = false; # no release for 9.3 yet QuickChick.job = false; # no release for 9.3 yet quickchick-test.job = false; # no release for 9.3 yet relation-algebra.job = false; # no release for 9.3 yet @@ -340,16 +337,12 @@ with builtins; with (import {}).lib; { bignums.override.version = "30a45625546da0a88db8689a8009d580aa3f557f"; stdlib-test.job = false; autosubst.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 itauto.job = false; # broken mathcomp-algebra-tactics.job = false; # no release for 9.2 yet - mathcomp-word.job = false; # no release for 9.2 yet - mathcomp-zify.job = false; # no release for 9.2 yet QuickChick.job = false; # no release for 9.2 yet quickchick-test.job = false; # no release for 9.2 yet - relation-algebra.job = false; # no release for 9.2 yet coinduction.override.version = "9502ae09e9f87518330f37c08bc19a8c452dcd91"; dpdgraph-test.override.version = "7a0fba21287dd8889c55e6611f8ba219d012b81b"; coq-hammer.override.version = "1d581299c2a85af175b53bd35370ea074af922ec"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index f315508937..287b7393b8 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"42df08846e50cc096c17af59110df547068557dc" +"b5a49525abfda1d45d561ada839f2be34ac369a4" diff --git a/.nix/rocq-overlays/rocq-lean-import/default.nix b/.nix/rocq-overlays/rocq-lean-import/default.nix index d3c6136a2e..7c89f8b9dd 100644 --- a/.nix/rocq-overlays/rocq-lean-import/default.nix +++ b/.nix/rocq-overlays/rocq-lean-import/default.nix @@ -1,12 +1,18 @@ -{ mkCoqDerivation, stdlib, version ? null }: +{ mkCoqDerivation, python3, rocq-core, stdlib, version ? null }: mkCoqDerivation { pname = "rocq-lean-import"; inherit version; + buildInputs = [ python3 rocq-core.ocamlPackages.yojson ]; propagatedBuildInputs = [ stdlib ]; mlPlugin = true; - buildFlags = [ "test" ]; + configurePhase = '' + export COQEXTRAFLAGS='-native-compiler no' + ''; + + # broken since it uses git-lfs, c.f., https://github.com/rocq-prover/rocq/pull/22474 + # buildFlags = [ "test" ]; }