diff --git a/.github/workflows/nix-action-9.0-2.5.0.yml b/.github/workflows/nix-action-9.0-master.yml similarity index 80% rename from .github/workflows/nix-action-9.0-2.5.0.yml rename to .github/workflows/nix-action-9.0-master.yml index 60b7ea7085..758425db49 100644 --- a/.github/workflows/nix-action-9.0-2.5.0.yml +++ b/.github/workflows/nix-action-9.0-master.yml @@ -40,7 +40,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch + \"9.0-master\" --argstr job \"coq\" \\\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 @@ -53,11 +53,11 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "coq" + "9.0-master" --argstr job "coq" mathcomp: needs: - rocq-core @@ -99,9 +99,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp\" \\\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" + \"9.0-master\" --argstr job \"mathcomp\" \\\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 @@ -112,23 +112,24 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-character" + "9.0-master" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "hierarchy-builder" + "9.0-master" --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp" + "9.0-master" --argstr job "mathcomp" mathcomp-analysis: needs: - rocq-core - mathcomp-reals + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -167,8 +168,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2> err > - out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + \"9.0-master\" --argstr job \"mathcomp-analysis\" \\\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 @@ -180,26 +181,29 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-reals" + "9.0-master" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-field" + "9.0-master" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-bigenough" + "9.0-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-analysis" + "9.0-master" --argstr job "mathcomp-analysis" mathcomp-analysis-single: needs: - rocq-core + - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -238,9 +242,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-single) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-analysis-single\" \\\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" + \"9.0-master\" --argstr job \"mathcomp-analysis-single\" \\\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 @@ -251,35 +255,35 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - 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 - "9.0-2.5.0" --argstr job "mathcomp-algebra" + "9.0-master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-finmap" + "9.0-master" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-bigenough" + "9.0-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-field" + "9.0-master" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-bigenough" + "9.0-master" --argstr job "mathcomp-bigenough" - 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 - "9.0-2.5.0" --argstr job "stdlib" + "9.0-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 - "9.0-2.5.0" --argstr job "mathcomp-analysis-single" + "9.0-master" --argstr job "mathcomp-analysis-single" mathcomp-analysis-stdlib: needs: - rocq-core @@ -323,9 +327,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-analysis-stdlib\" \\\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" + \"9.0-master\" --argstr job \"mathcomp-analysis-stdlib\" \\\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 @@ -336,26 +340,90 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-analysis" + "9.0-master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-reals-stdlib" + "9.0-master" --argstr job "mathcomp-reals-stdlib" - 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 - "9.0-2.5.0" --argstr job "stdlib" + "9.0-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 + "9.0-master" --argstr job "mathcomp-analysis-stdlib" + mathcomp-bigenough: + needs: + - rocq-core + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-bigenough) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-master\" --argstr job \"mathcomp-bigenough\" \\\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 + "9.0-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 + "9.0-master" --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 - "9.0-2.5.0" --argstr job "mathcomp-analysis-stdlib" + "9.0-master" --argstr job "mathcomp-bigenough" mathcomp-classical: needs: - rocq-core + - mathcomp-finmap runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -394,7 +462,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-classical) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2> err + \"9.0-master\" --argstr job \"mathcomp-classical\" \\\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 @@ -407,23 +475,24 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - 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 - "9.0-2.5.0" --argstr job "mathcomp-algebra" + "9.0-master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-finmap" + "9.0-master" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-classical" + "9.0-master" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - rocq-core - mathcomp-reals + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -462,7 +531,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-experimental-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run + \"9.0-master\" --argstr job \"mathcomp-experimental-reals\" \\\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 @@ -475,19 +544,82 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-reals" + "9.0-master" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-bigenough" + "9.0-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-experimental-reals" + "9.0-master" --argstr job "mathcomp-experimental-reals" + mathcomp-finmap: + needs: + - rocq-core + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-finmap) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-master\" --argstr job \"mathcomp-finmap\" \\\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 + "9.0-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 + "9.0-master" --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 + "9.0-master" --argstr job "mathcomp-finmap" mathcomp-infotheo: needs: - coq @@ -530,8 +662,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-infotheo) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-infotheo\" \\\n --dry-run 2> err > - out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + \"9.0-master\" --argstr job \"mathcomp-infotheo\" \\\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 @@ -543,23 +675,23 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "coq" + "9.0-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-analysis-stdlib" + "9.0-master" --argstr job "mathcomp-analysis-stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-algebra-tactics" + "9.0-master" --argstr job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: interval' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "interval" + "9.0-master" --argstr job "interval" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-infotheo" + "9.0-master" --argstr job "mathcomp-infotheo" mathcomp-reals: needs: - rocq-core @@ -602,7 +734,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2> err > out + \"9.0-master\" --argstr job \"mathcomp-reals\" \\\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 @@ -615,15 +747,15 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-classical" + "9.0-master" --argstr job "mathcomp-classical" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-reals" + "9.0-master" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: - rocq-core @@ -666,9 +798,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-reals-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"mathcomp-reals-stdlib\" \\\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" + \"9.0-master\" --argstr job \"mathcomp-reals-stdlib\" \\\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 @@ -679,21 +811,22 @@ jobs: - 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 - "9.0-2.5.0" --argstr job "rocq-core" + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-reals" + "9.0-master" --argstr job "mathcomp-reals" - 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 - "9.0-2.5.0" --argstr job "stdlib" + "9.0-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 - "9.0-2.5.0" --argstr job "mathcomp-reals-stdlib" - rocq-core: - needs: [] + "9.0-master" --argstr job "mathcomp-reals-stdlib" + micromega-plugin: + needs: + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -730,11 +863,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (rocq-core) + name: Getting derivation for current job (micromega-plugin) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --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" + \"9.0-master\" --argstr job \"micromega-plugin\" \\\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 @@ -742,15 +875,16 @@ 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: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "rocq-core" - ssprove: - needs: - - coq - - mathcomp-analysis - - mathcomp-experimental-reals + "9.0-master" --argstr job "micromega-plugin" + rocq-core: + needs: [] runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -787,11 +921,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (ssprove) + name: Getting derivation for current job (rocq-core) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0-2.5.0\" --argstr job \"ssprove\" \\\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" + \"9.0-master\" --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 name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -799,50 +933,18 @@ 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 - "9.0-2.5.0" --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "equations" - - 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 - "9.0-2.5.0" --argstr job "mathcomp-boot" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-analysis" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-experimental-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-experimental-reals" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: extructures' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "extructures" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: deriving' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "deriving" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-word' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "mathcomp-word" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-2.5.0" --argstr job "ssprove" -name: Nix CI for bundle 9.0-2.5.0 + "9.0-master" --argstr job "rocq-core" +name: Nix CI for bundle 9.0-master on: pull_request: paths: - - .github/workflows/nix-action-9.0-2.5.0.yml + - .github/workflows/nix-action-9.0-master.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-9.0-2.5.0.yml + - .github/workflows/nix-action-9.0-master.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-9.0.yml b/.github/workflows/nix-action-9.1-master.yml similarity index 72% rename from .github/workflows/nix-action-9.0.yml rename to .github/workflows/nix-action-9.1-master.yml index b8b466753e..9424a3bb46 100644 --- a/.github/workflows/nix-action-9.0.yml +++ b/.github/workflows/nix-action-9.1-master.yml @@ -40,8 +40,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; - true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + \"9.1-master\" --argstr job \"coq\" \\\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 @@ -52,16 +52,84 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "coq" + mathcomp: + needs: + - rocq-core + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"mathcomp\" \\\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 + "9.1-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp" mathcomp-analysis: needs: - rocq-core - mathcomp-reals + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -100,9 +168,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-analysis\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-analysis\" \\\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 @@ -112,27 +180,30 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-reals" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-field" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-bigenough" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-analysis" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-analysis" mathcomp-analysis-single: needs: - rocq-core + - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -171,9 +242,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-single) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-analysis-single\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-analysis-single\" \\\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 @@ -183,36 +254,36 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - 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 "9.0" - --argstr job "mathcomp-algebra" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-finmap" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-bigenough" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-field" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-bigenough" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" - 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 "9.0" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-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 "9.0" - --argstr job "mathcomp-analysis-single" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-analysis-single" mathcomp-analysis-stdlib: needs: - rocq-core @@ -256,9 +327,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-analysis-stdlib\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-analysis-stdlib\" \\\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 @@ -268,27 +339,91 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-analysis" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-reals-stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-reals-stdlib" - 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 "9.0" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-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 + "9.1-master" --argstr job "mathcomp-analysis-stdlib" + mathcomp-bigenough: + needs: + - rocq-core + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-bigenough) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"mathcomp-bigenough\" \\\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 + "9.1-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 + "9.1-master" --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 "9.0" - --argstr job "mathcomp-analysis-stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" mathcomp-classical: needs: - rocq-core + - mathcomp-finmap runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -327,9 +462,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-classical) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-classical\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-classical\" \\\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 @@ -339,24 +474,25 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - 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 "9.0" - --argstr job "mathcomp-algebra" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-finmap" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-classical" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - rocq-core - mathcomp-reals + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -395,9 +531,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-experimental-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-experimental-reals\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-experimental-reals\" \\\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 @@ -407,20 +543,83 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-reals" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-bigenough" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-experimental-reals" + mathcomp-finmap: + needs: + - rocq-core + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-finmap) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.1-master\" --argstr job \"mathcomp-finmap\" \\\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 + "9.1-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 + "9.1-master" --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 "9.0" - --argstr job "mathcomp-experimental-reals" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-finmap" mathcomp-infotheo: needs: - coq @@ -463,9 +662,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-infotheo) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-infotheo\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-infotheo\" \\\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 @@ -475,24 +674,24 @@ jobs: 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 "9.0" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-analysis-stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-analysis-stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-algebra-tactics" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: interval' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "interval" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "interval" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-infotheo" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-infotheo" mathcomp-reals: needs: - rocq-core @@ -535,9 +734,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-reals\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-reals\" \\\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 @@ -547,16 +746,16 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-classical" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-classical" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-reals" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: - rocq-core @@ -599,9 +798,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-reals-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"mathcomp-reals-stdlib\" \\\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" + \"9.1-master\" --argstr job \"mathcomp-reals-stdlib\" \\\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 @@ -611,22 +810,23 @@ jobs: 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 "9.0" - --argstr job "rocq-core" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-reals" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-reals" - 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 "9.0" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-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 "9.0" - --argstr job "mathcomp-reals-stdlib" - rocq-core: - needs: [] + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "mathcomp-reals-stdlib" + micromega-plugin: + needs: + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -663,11 +863,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (rocq-core) + name: Getting derivation for current job (micromega-plugin) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --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" + \"9.1-master\" --argstr job \"micromega-plugin\" \\\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 @@ -675,15 +875,16 @@ 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: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "rocq-core" - ssprove: - needs: - - coq - - mathcomp-analysis - - mathcomp-experimental-reals + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "micromega-plugin" + rocq-core: + needs: [] runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -720,11 +921,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (ssprove) + name: Getting derivation for current job (rocq-core) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0\" --argstr job \"ssprove\" \\\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" + \"9.1-master\" --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 name: Checking presence of CI target for current job run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs @@ -732,50 +933,18 @@ 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 "9.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "equations" - - 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 "9.0" - --argstr job "mathcomp-boot" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-analysis" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-experimental-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-experimental-reals" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: extructures' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "extructures" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: deriving' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "deriving" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-word' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "mathcomp-word" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" - --argstr job "ssprove" -name: Nix CI for bundle 9.0 + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "9.1-master" --argstr job "rocq-core" +name: Nix CI for bundle 9.1-master on: pull_request: paths: - - .github/workflows/nix-action-9.0.yml + - .github/workflows/nix-action-9.1-master.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-9.0.yml + - .github/workflows/nix-action-9.1-master.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-9.1.yml b/.github/workflows/nix-action-9.1.yml deleted file mode 100644 index 4799d71a17..0000000000 --- a/.github/workflows/nix-action-9.1.yml +++ /dev/null @@ -1,696 +0,0 @@ -jobs: - coq: - needs: - - rocq-core - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (coq) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"coq\" \\\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 "9.1" - --argstr job "rocq-core" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "coq" - mathcomp-analysis: - needs: - - rocq-core - - mathcomp-reals - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-analysis) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-analysis\" \\\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 "9.1" - --argstr job "rocq-core" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-reals" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-analysis" - mathcomp-analysis-single: - needs: - - rocq-core - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-analysis-single) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-analysis-single\" \\\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 "9.1" - --argstr job "rocq-core" - - 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 "9.1" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-bigenough" - - 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 "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 "9.1" - --argstr job "mathcomp-analysis-single" - mathcomp-analysis-stdlib: - needs: - - rocq-core - - mathcomp-analysis - - mathcomp-reals-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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-analysis-stdlib) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-analysis-stdlib\" \\\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 "9.1" - --argstr job "rocq-core" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-analysis" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-reals-stdlib" - - 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 "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 "9.1" - --argstr job "mathcomp-analysis-stdlib" - mathcomp-classical: - needs: - - rocq-core - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-classical) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-classical\" \\\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 "9.1" - --argstr job "rocq-core" - - 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 "9.1" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-classical" - mathcomp-experimental-reals: - needs: - - rocq-core - - mathcomp-reals - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-experimental-reals) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-experimental-reals\" \\\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 "9.1" - --argstr job "rocq-core" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-reals" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-experimental-reals" - mathcomp-infotheo: - needs: - - coq - - mathcomp-analysis-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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-infotheo) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-infotheo\" \\\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 "9.1" - --argstr job "coq" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-analysis-stdlib" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-algebra-tactics" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: interval' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "interval" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-infotheo" - mathcomp-reals: - needs: - - rocq-core - - mathcomp-classical - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-reals) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-reals\" \\\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 "9.1" - --argstr job "rocq-core" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-classical" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-reals" - mathcomp-reals-stdlib: - needs: - - rocq-core - - mathcomp-reals - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-reals-stdlib) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --argstr job \"mathcomp-reals-stdlib\" \\\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 "9.1" - --argstr job "rocq-core" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "mathcomp-reals" - - 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 "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 "9.1" - --argstr job "mathcomp-reals-stdlib" - rocq-core: - 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 math-comp - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (rocq-core) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.1\" --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 - 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 current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" - --argstr job "rocq-core" -name: Nix CI for bundle 9.1 -on: - pull_request: - paths: - - .github/workflows/nix-action-9.1.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-9.1.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.nix/config.nix b/.nix/config.nix index 50f6625c3d..566993c3e4 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -42,36 +42,45 @@ in { ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "9.1"; + default-bundle = "9.1-master"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."9.0-2.5.0" = { + bundles."9.0-master" = { rocqPackages = { rocq-core.override.version = "9.0"; - mathcomp.override.version = "2.5.0"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; + micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { coq.override.version = "9.0"; - mathcomp.override.version = "2.5.0"; + ssprove.job = false; # not yet available for 9.1 }; }; - bundles."9.0" = { - rocqPackages = { - rocq-core.override.version = "9.0"; - }; - coqPackages = common-bundle // { - coq.override.version = "9.0"; - }; - }; + # bundles."9.1-2.5.0" = { + # rocqPackages = { + # rocq-core.override.version = "9.1"; + # mathcomp.override.version = "2.5.0"; + # }; + # coqPackages = common-bundle // { + # coq.override.version = "9.1"; + # ssprove.job = false; # not yet available for 9.1 + # }; + # }; - bundles."9.1" = { + bundles."9.1-master" = { rocqPackages = { rocq-core.override.version = "9.1"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; + micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { coq.override.version = "9.1"; @@ -90,6 +99,7 @@ in { mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; + micromega-plugin.override.version = "master"; }; coqPackages = common-bundle // { coq.override.version = "master"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 4f18023e08..ff570aeca7 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"175e68be5dcde92457dbb949ef905e771d765a68" +"6b32b8cd491ec44b75da86fb17e4353f2f102328" diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0e61ee4fbc..349029b70b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -95,6 +95,38 @@ - in `reals.v`: + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn` +- in `mathcomp_extra.v`: + + lemmas `divDl_ge0`, `divDl_le1` + +- in `unstable.v`: + + lemmas `divD_onem` + +- in `filter.v`: + + mixin `isSubNbhs`, structure `SubNbhs`, notation `subNbhsType` + +- in `topology_structure.v`: + + structure `SubTopological`, notation `subTopologicalType` + +- in `tvs.v`: + + structure `SubConvexTvs`, notation `subConvexTvsType` + +- in `normed_module.v`: + + structure `SubNormedModule`, notation `subNormedModType` + + instance `ent_xsection_filter` + + factory `SubLmodule_isSubNormedmodule` + +- new file `hahn_banach_theorem.v`: + + module `LinearGraph` + * definitions `graph`, `linear_graph` + * lemmas `lingraph_00`, `lingraphZ`, `lingraphD` + + module `HahnBanachZorn` + * definitions `extend_graph`, `le_graph`, `functional_graph`, `le_extend_graph` + * record `zorn_type` + * definition `zphi` + * lemma `zorn_type_eq` + * definition `zornS` + * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness` + + theorems `hahn_banach_extension`, `hahn_banach_extension_normed` ### Changed @@ -126,9 +158,14 @@ - new files `signed_measure.v` and `radon_nikodym.v` + with the contents of `charge.v` (deprecated) - + ### Changed +- moved from `measurable_structure.v` to `classical_sets.v`: + + definition `preimage_set_system` + + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, + `preimage_set_system_id` + - moved from `measurable_structure.v` to `classical_sets.v`: + definition `preimage_set_system` + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`, diff --git a/_CoqProject b/_CoqProject index 8d0e2e3439..f0b745c7f6 100644 --- a/_CoqProject +++ b/_CoqProject @@ -88,6 +88,8 @@ theories/normedtype_theory/urysohn.v theories/normedtype_theory/vitali_lemma.v theories/normedtype_theory/normedtype.v +theories/functional_analysis/hahn_banach_theorem.v + theories/sequences.v theories/realfun.v theories/exp.v diff --git a/classical/filter.v b/classical/filter.v index bf37191256..172c8ac6d0 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat all_algebra finmap. From mathcomp Require Import boolp classical_sets functions wochoice. @@ -15,21 +15,31 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. (* *) (* ## Structure of filter *) (* ``` *) -(* filteredType U == interface type for types whose *) -(* elements represent sets of sets on U *) -(* These sets are intended to be filters *) -(* on U but this is not enforced yet. *) -(* The HB class is called Filtered. *) -(* It extends Pointed. *) -(* nbhs p == set of sets associated to p (in a *) -(* filtered type) *) -(* pfilteredType U == a pointed and filtered type *) -(* hasNbhs == factory for filteredType *) +(* filteredType U == interface type for types whose elements *) +(* represent sets of sets on U *) +(* These sets are intended to be filters on U *) +(* but this is not enforced yet. *) +(* The HB class is called Filtered. *) +(* It extends Pointed. *) +(* nbhs p == set of sets associated to p (in a filtered *) +(* type) *) +(* pfilteredType U == a pointed and filtered type *) +(* hasNbhs == factory for filteredType *) +(* nbhsType == type of a structure that has a set system *) +(* of neighborhoods associated to each point *) +(* pnbhsType == same has nbhsType for pointed types *) (* continuous f == f is continuous w.r.t the topology *) -(* filterI_iter F n == nth stage of recursively building the *) -(* filter of finite intersections of F *) -(* finI_from D f == set of \bigcap_(i in E) f i where E is *) -(* a finite subset of D *) +(* isSubNbhs V S U == interface that states the continuity of val *) +(* for U which has a subChoiceType and a *) +(* nbhsType *) +(* subNbhsType V S == structure that extends a *) +(* subChoiceType/nbhsType with the isSubNbhs *) +(* interface *) +(* The HB class is SubNbhs. *) +(* filterI_iter F n == nth stage of recursively building the *) +(* filter of finite intersections of F *) +(* finI_from D f == set of \bigcap_(i in E) f i where E is a *) +(* a finite subset of D *) (* ``` *) (* *) (* We endow several standard types with the structure of filter, e.g.: *) @@ -951,6 +961,15 @@ Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x : {for x, continuous (g \o f)}. Proof. exact: cvg_comp. Qed. +HB.mixin Record isSubNbhs + (V : nbhsType) (S : pred V) U & SubChoice V S U & Nbhs U := { + continuous_valE : continuous (val : U -> V) +}. + +#[short(type="subNbhsType")] +HB.structure Definition SubNbhs (V : nbhsType) (S : pred V) := + { U of SubChoice V S U & Nbhs U & isSubNbhs V S U}. + Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) : {for x, continuous f} -> (\forall y \near f x, P y) -> (\near x, P (f x)). diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 0b87d5fc7c..d3a14ce6e8 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,5 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. +From HB Require Import structures. +From mathcomp Require Import all_ssreflect_compat finmap all_algebra. (**md**************************************************************************) (* # MathComp extra *) @@ -93,10 +94,21 @@ Proof. by case: C => //= /ltW. Qed. (* MathComp 2.6 additions *) (**************************) -(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) Lemma intrD1 {R : pzRingType} (i : int) : (i + 1)%:~R = i%:~R + 1 :> R. Proof. by rewrite intrD. Qed. -(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *) Lemma intr1D {R : pzRingType} (i : int) : (1 + i)%:~R = 1 + i%:~R :> R. Proof. by rewrite intrD. Qed. + +Lemma divDl_ge0 (R : numDomainType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : + 0 <= s / (s + t). +Proof. +by apply: divr_ge0 => //; apply: addr_ge0. +Qed. + +Lemma divDl_le1 (R : numFieldType) (s t : R) (s0 : 0 <= s) (t0 : 0 <= t) : + s / (s + t) <= 1. +Proof. +move: s0; rewrite le0r => /predU1P [->|s0]; first by rewrite mul0r. +by rewrite ler_pdivrMr ?mul1r ?lerDl // ltr_wpDr. +Qed. diff --git a/classical/unstable.v b/classical/unstable.v index e331d2836d..cf8b4ce04a 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -369,6 +369,13 @@ Qed. Lemma onemV (F : numFieldType) (x : F) : x != 0 -> x^-1.~ = (x - 1) / x. Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed. +Lemma divD_onem (R : realFieldType) (s t : R) (s0 : 0 < s) (t0 : 0 < t) : + (s / (s + t)).~ = t / (s + t). +Proof. +rewrite /onem. +by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK. +Qed. + Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N. Proof. by case: a => //= n _; case: b. Qed. diff --git a/theories/Make b/theories/Make index 136692568d..17da83d2a3 100644 --- a/theories/Make +++ b/theories/Make @@ -55,6 +55,8 @@ normedtype_theory/urysohn.v normedtype_theory/vitali_lemma.v normedtype_theory/normedtype.v +functional_analysis/hahn_banach_theorem.v + realfun.v sequences.v exp.v diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v new file mode 100644 index 0000000000..ec779acb2b --- /dev/null +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -0,0 +1,363 @@ +From HB Require Import structures. +From mathcomp Require Import all_boot all_order all_algebra. +From mathcomp Require Import interval_inference. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra boolp contra classical_sets filter. +From mathcomp Require Import topology convex reals normedtype. + +(**md**************************************************************************) +(* # The Hahn-Banach theorem *) +(* *) +(* This files proves the Hahn-Banach theorem thanks to Zorn's lemma. *) +(* Theorem `hahn_banach_extensionHahnbanach` states that, considering `V` an *) +(* lmodType on a realtype, a linear function on a subLmodType of V, that is *) +(* bounded by a convex function, can be extended to a linear map on V bounded *) +(* by the same convex function. *) +(* Theorem `hahn_banach_extension_normed` specifies this to the extension of *) +(* a linear continuous function on a subspace to the whole normed module. *) +(* *) +(* ``` *) +(* Module LinearGraph == definitions on linear relations, thought of *) +(* as graph of functions *) +(* Module HahnBanachZorn == definition of the type zorn_type of linear *) +(* functional graphs, bounded by a convex *) +(* function and extending to the whole space a *) +(* given linear graph. *) +(* ``` *) +(* *) +(******************************************************************************) + +Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope convex_scope. +Local Open Scope real_scope. + +(* TODO : use a lightweight factory to make every subLmodType a subnormedmodtype *) + +Module LinearGraph. +Section linear_graph. +Context (R : numDomainType) (V : lmodType R). + +Definition graph := V -> R -> Prop. + +Definition linear_graph (f : graph) := + forall v1 v2 l r1 r2, f v1 r1 -> f v2 r2 -> f (v1 + l *: v2) (r1 + l * r2). + +Variable f : graph. +Hypothesis lf : linear_graph f. + +Lemma lingraph_00 x r : f x r -> f 0 0. +Proof. +by move=> fxr; have := lf (-1) fxr fxr; rewrite scaleN1r mulN1r !subrr. +Qed. + +Lemma lingraphZ x r l : f x r -> f (l *: x) (l * r). +Proof. by move=> fxr; have := lf l (lingraph_00 fxr) fxr; rewrite !add0r. Qed. + +Lemma lingraphD x1 x2 r1 r2 : f x1 r1 -> f x2 r2 -> f (x1 - x2) (r1 - r2). +Proof. by move=> f1 f2; have := lf (-1) f1 f2; rewrite !scaleN1r mulN1r. Qed. + +End linear_graph. +End LinearGraph. + +Module HahnBanachZorn. +Section HahnBanachZorn. +Import LinearGraph. +Context (R : realType) (V : lmodType R) (F : pred V). +Variables (F' : subLmodType F) (phi : {linear F' -> R}) (p : V -> R). + +Implicit Types f g : graph V. + +Hypothesis phi_le_p : forall v, phi v <= p (val v). + +Hypothesis p_cvx : @convex_function R V [set: V] p. + +Definition extend_graph f := forall v : F', f (\val v) (phi v). + +Definition le_graph p f := forall v r, f v r -> r <= p v. + +Definition functional_graph f := forall v r1 r2, f v r1 -> f v r2 -> r1 = r2. + +Definition le_extend_graph f := + [/\ functional_graph f, linear_graph f, le_graph p f & extend_graph f]. + +Record zorn_type : Type := ZornType + {carrier : graph V; specP : le_extend_graph carrier}. + +Implicit Types z : zorn_type. + +Let spec_phi : + le_extend_graph (fun v r => exists2 y : F', v = val y & r = phi y). +Proof. +split. +- by move=> v r1 r2 [y1 -> ->] [y2 + ->] => /val_inj ->. +- move => v1 v2 l r1 r2 [y1 -> ->] [y2 -> ->]. + by exists (y1 + l *: y2); rewrite !linearD !linearZ. +- by move=> r v [y -> ->]. +- by move=> v; exists v. +Qed. + +Definition zphi := ZornType spec_phi. + +Lemma zorn_type_eq z1 z2 : carrier z1 = carrier z2 -> z1 = z2. +Proof. +case: z1 => m1 pm1; case: z2 => m2 pm2 /= e; rewrite e in pm1 pm2 *. +by congr ZornType; exact: Prop_irrelevance. +Qed. + +Definition zornS z1 z2 := forall x y, carrier z1 x y -> carrier z2 x y. + +(* Zorn applied to the relation of extending the graph of the first function: *) +Lemma zornS_ex : exists g : zorn_type, forall z, zornS g z -> z = g. +Proof. +pose Rbool x y := `[< zornS x y >]. +have RboolP z t : Rbool z t <-> zornS z t by split => /asboolP. +suff [t st] : exists t : zorn_type, forall s : zorn_type, Rbool t s -> s = t. + by exists t; move => z /RboolP tz; exact: st. +apply: (@Zorn zorn_type Rbool); first by move=> t; exact/RboolP. +- by move=> r s t /RboolP a /RboolP b; apply/RboolP => x y /a /b. +- move=> r s /RboolP a /RboolP b; apply: zorn_type_eq. + by apply: funext => z; apply: funext => h; apply: propext; split => [/a | /b]. +move=> A Amax. +have [[w Aw]|eA] := lem (exists a, A a); last first. + by exists zphi => a Aa; absurd: eA; exists a. +(* g is the union of the graphs indexed by elements in a *) +pose g v r := exists2 a, A a & carrier a v r. +have g_fun : functional_graph g. + move=> v r1 r2 [a Aa avr1] [b Ab bvr2]. + have [|] : Rbool a b \/ Rbool b a by exact: Amax. + - rewrite /Rbool /RboolP /zornS. + case: b Ab bvr2 {Aa} => s2 [fs2 _ _ _] /= _ s2vr2 /asboolP ecas2. + by move/ecas2 : avr1 => /fs2 /(_ s2vr2). + - rewrite /Rbool /RboolP /zornS. + case: a Aa avr1 {Ab} => s1 [fs1 _ _ _] /= _ s1vr1 /asboolP ecbs1. + by move/ecbs1: bvr2; exact: fs1. +have g_lin : linear_graph g. + move=> v1 v2 l r1 r2 [a1 Aa1 c1] [a2 Aa2 c2]. + have [/RboolP sc12 | /RboolP sc21] := Amax _ _ Aa1 Aa2. + - have {sc12 Aa1 a1} {}c1 : carrier a2 v1 r1 by exact: sc12. + by exists a2 => //; case: a2 {Aa2} c2 c1 => c /= [_ + _ _] *; exact. + - have {sc21 Aa2 a2} {}c2 : carrier a1 v2 r2 by exact: sc21. + by exists a1 => //; case: a1 {Aa1} c2 c1 => c /= [_ + _ _] *; exact. +have g_majp : le_graph p g by move=> v r [[c/= [fs1 ls1 ms1 ps1]]]/= _ => /ms1. +have g_prol : extend_graph g. + by move=> *; exists w => //; case: w Aw => [c [_ _ _ +]] _ //=; exact. +have spec_g : le_extend_graph g by split. +pose zg := ZornType spec_g. +by exists zg => [a Aa]; apply/RboolP; rewrite /zornS => v r cvr; exists a. +Qed. + +Variable g : zorn_type. + +(* The next lemma proves that when z is of zorn_type, it can be extended on any +real line directed by an arbitrary vector v *) +Lemma domain_extend z v : exists2 ze, zornS z ze & exists r, (carrier ze) v r. +Proof. +have [[r rP]|] := lem (exists r, carrier z v r). + by exists z => //; exists r. +case: z => [c [fs1 ls1 ms1 ps1]] /= nzv. +have c00 : c 0 0. + have <- : phi 0 = 0 by rewrite linear0. + by have := ps1 0; rewrite GRing.val0. +have [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> + r + lambda * a <= p (x + lambda *: v). + suff [a aP] : exists a, forall (x : V) (r lambda : R), c x r -> 0 < lambda -> + r + lambda * a <= p (x + lambda *: v) /\ + r - lambda * a <= p (x - lambda *: v). + exists a => x r lambda /[dup] cxr /aP {}aP. + have [/aP[]// | ltl0 | ->] := ltrgt0P lambda. + rewrite -[lambda]opprK scaleNr mulNr. + by have /aP[] : 0 < - lambda by rewrite oppr_gt0. + by rewrite mul0r scale0r !addr0 ms1. + pose b (x : V) r lambda : R := (p (x + lambda *: v) - r) / lambda. + pose a (x : V) r lambda : R := (r - p (x - lambda *: v)) / lambda. + have le_a_b x1 x2 r1 r2 (s t : R) : c x1 r1 -> c x2 r2 -> 0 < s -> 0 < t -> + a x1 r1 s <= b x2 r2 t. + move=> cxr1 cxr2 lt0s lt0t; rewrite /a /b. + rewrite ler_pdivlMr// mulrAC ler_pdivrMr// [leLHS]mulrC [leRHS]mulrC. + rewrite !mulrDr !mulrN lerBlDr addrAC lerBrDr. + have /ler_pM2r <- : 0 < (s + t)^-1 by rewrite invr_gt0 addr_gt0. + set y1 : V := _ + _ *: _; set y2 : V := _ - _ *: _. + rewrite (@le_trans _ _ (p (s / (s + t) *: y1 + t / (s + t) *: y2)))//. + set u : V := (X in p X). + have {u y1 y2} -> : u = t / (s + t) *: x1 + s / (s + t) *: x2. + rewrite /u ![_ / _]mulrC -!scalerA -!scalerDr /y1 /y2; congr (_ *: _). + by rewrite !scalerDr addrCA scalerN scalerA (mulrC s) -scalerA addrK. + set l := t / _; set m := s / _. + rewrite [leLHS](_ : _ = l * r1 + m * r2). + by rewrite mulrDl ![_ * _ / _]mulrAC. + apply: ms1; apply: (ls1) => //. + by rewrite -[_ *: _]add0r -[_ * _]add0r; exact: ls1. + rewrite !mulrDl ![_ * _ / _]mulrAC -divD_onem//. + pose st := Itv01 (divDl_ge0 (ltW lt0s) (ltW lt0t)) + (divDl_le1 (ltW lt0s) (ltW lt0t)). + exact: (p_cvx st (in_setT y1) (in_setT y2)). + pose Pa := + [set r | exists x1 r1 (s1 : R), [/\ c x1 r1, 0 < s1 & r = a x1 r1 s1]]. + pose Pb := + [set r | exists x1 r1 (s1 : R), [/\ c x1 r1, 0 < s1 & r = b x1 r1 s1]]. + pose sa := sup Pa. (* We need p with values in a *realType* *) + have Pax : Pa !=set0 by exists (a 0 0 1), 0, 0, 1. + have ubdP : ubound Pa sa. + apply: sup_upper_bound; split => //=. + by exists (b 0 0 1) =>/= x [y [r [s [cry lt0s ->]]]]; exact: le_a_b. + have saP (u : R) : ubound Pa u -> sa <= u by exact: ge_sup. + pose ib := inf Pb. (* We need P with values in a *realType* *) + have Pbx : Pb !=set0 by exists (b 0 0 1), 0, 0, 1. + have ibdP : lbound Pb ib. + apply: ge_inf; exists (a 0 0 1) => /= x [y [r [s [cry lt0s ->]]]]. + exact: le_a_b. + have ibP (u : R) : lbound Pb u -> u <= ib by exact: lb_le_inf Pbx. + have le_sa_ib : sa <= ib. + apply: saP => _ [y [r [l [cry lt0l ->]]]]. + by apply: ibP => _ [z [s [m [crz lt0m ->]]]]; exact: le_a_b. + pose alpha := (sa + ib) / 2. + exists alpha => x r l cxr lt0l; split. + - suff : alpha <= b x r l by rewrite (ler_pdivlMr _ _ lt0l) lerBrDl mulrC. + by apply: (le_trans (midf_le le_sa_ib).2); apply: ibdP; exists x, r, l. + - suff : a x r l <= alpha. + by rewrite (ler_pdivrMr _ _ lt0l) lerBlDl -lerBlDr mulrC. + by apply: (le_trans _ (midf_le le_sa_ib).1); apply: ubdP; exists x, r, l. +pose z' := fun k r => exists (v' : V) (r' lambda : R), + [/\ c v' r', k = v' + lambda *: v & r = r' + lambda * a]. +have z'_extends x r : c x r -> z' x r. + by move=> cxr; exists x, r, 0; split; rewrite // ?scale0r ?mul0r ?addr0. +have z'_prol : extend_graph z'. + move=> x. + by exists (val x), (phi x), 0; split; rewrite // ?scale0r ?mul0r ?addr0. +have z'_maj_by_p : le_graph p z' + by move=> x r [w [s [l [cws -> ->]]]]; apply: aP. +have z'_lin : linear_graph z'. + move=> x1 x2 l r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 -> ->]]]]. + rewrite [X in z' X _](_ : _ = w1 + l *: w2 + (m1 + l * m2) *: v). + by rewrite !scalerDr !scalerDl scalerA -!addrA [X in _ + X]addrCA. + rewrite [X in z' _ X](_ : _ = s1 + l * s2 + (m1 + l * m2) * a). + by rewrite !mulrDr !mulrDl mulrA -!addrA [X in _ + X]addrCA. + exists (w1 + l *: w2), (s1 + l * s2), (m1 + l * m2); split => //. + exact: ls1. +have z'_functional : functional_graph z'. + move=> w r1 r2 [w1 [s1 [m1 [cws1 -> ->]]]] [w2 [s2 [m2 [cws2 e1 ->]]]]. + have [rw12 erw12] : exists r, c (w1 - w2) r. + by exists (s1 + -1 * s2); rewrite -(scaleN1r w2); exact: ls1. + have h1 (x : V) (r l : R) : x = l *: v -> c x r -> x = 0 /\ l = 0. + move=> -> cxr; have [->|ln0] := eqVneq l 0; first by rewrite scale0r. + suff cvs : c v (l^-1 * r) by absurd: nzv; exists (l^-1 * r). + suff -> : v = l ^-1 *: (l *: v). + by rewrite -(add0r (_ *: _)) -(add0r (_ * _)); exact: ls1. + by rewrite scalerA mulVf ?scale1r. + have [ew12] : w1 - w2 = 0 /\ m2 - m1 = 0. + apply: h1 erw12; rewrite scalerBl. + by apply: subr0_eq; rewrite opprB addrACA e1 -opprD subrr. + suff -> : s1 = s2 by move/subr0_eq => ->. + by apply: fs1 cws2; rewrite -(subr0_eq ew12). +have z'_spec : le_extend_graph z' by []. +exists (ZornType z'_spec) => //=; exists a, 0, 0, 1. +by rewrite !add0r mul1r scale1r. +Qed. + +Hypothesis gP : forall z, zornS g z -> z = g. + +Let total_g v : exists r, carrier g v r. +Proof. +have [z /gP sgz [r zr]] := domain_extend g v. +by exists r; rewrite -sgz. +Qed. + +Lemma hahn_banach_witness : + exists h : V -> R, forall v r, carrier g v r <-> h v = r. +Proof. +have [h hP] := choice total_g. +exists h => v r; split=> [|<-//]. +move: g gP total_g hP => [c /= [fg _ _ _]] _ _ hP cvr. +by rewrite (fg v r (h v)). +Qed. + +End HahnBanachZorn. +End HahnBanachZorn. + +(* NB: could go to convex.v *) +Section hahn_banach. +Import LinearGraph. +Import HahnBanachZorn. +(* Now we prove HahnBanach on functions *) +(* We consider R a real (=ordered) field with supremum, and V a (left) module + on R. We do not make use of the 'vector' interface as the latter enforces + finite dimension. *) +Context {R : realType} (V : lmodType R) (F : pred V). +Variables (F' : subLmodType F) (f : {linear F' -> R}) (p : V -> R). + +Hypothesis p_cvx : @convex_function R V [set: V] p. + +Hypothesis f_bounded_by_p : forall z : F', f z <= p (\val z). + +Theorem hahn_banach_extension : exists2 g : {scalar V}, + (forall x, g x <= p x) & forall z : F', g (\val z) = f z. +Proof. +pose graphF (v : V) r := exists2 z : F', v = \val z & r = f z. +have [z /(hahn_banach_witness p_cvx)[g gP]] := zornS_ex f_bounded_by_p. +have scalg : linear_for *%R g. + case: z gP => [c [_ ls1 _ _]] /= gP. + have addg : zmod_morphism g. + by move=> w1 w2; apply/gP; apply: lingraphD => //; apply/gP. + suff scalg : scalable_for *%R g. + by move=> a u v; rewrite -gP -(addrC v) -(addrC (g v)); apply/ls1; exact/gP. + by move=> w l; apply/gP; apply: lingraphZ => //; exact/gP. +pose lg := GRing.isLinear.Build _ _ _ _ g scalg. +pose g' : {linear V -> R | *%R} := HB.pack g lg. +exists g'. + by case: z gP => [c [_ _ bp _]] /= gP => x; apply: bp; exact/gP. +by move=> z'; apply/gP; case: z {gP} => [c [_ _ _ pf]] /=; exact: pf. +Qed. + +End hahn_banach. + +Section hahn_banach_normed. +Variable (R : realType) (V : normedModType R) (F : pred V) + (F' : subNormedModType F) (f : {linear_continuous F' -> R}). + +Theorem hahn_banach_extension_normed : + exists g : {linear_continuous V -> R}, forall x : F', g (val x) = f x. +Proof. +have [r ltr0 fxrx] : exists2 r, r > 0 & forall z : F', `|f z| <= `|val z| * r. + suff: \forall r \near +oo, forall x : F', `|f x| <= r * `|x|. + move=> [t [_ tf]]. + exists (`|t| + 1); first by rewrite ltr_wpDl. + by move=> z; rewrite mulrC norm_valE tf// (le_lt_trans (ler_norm _)) ?ltrDl. + exact/linear_boundedP/continuous_linear_bounded/continuous_fun. +pose p := fun x : V => `|x| * r. +have convp : @convex_function _ _ [set: V] p. + rewrite /convex_function /conv => l v1 v2 _ _ /=. + rewrite [in leRHS]/conv /= /p. + apply: le_trans. + have /ler_pM := ler_normD (l%:num *: v1) (l%:num.~ *: v2). + by apply => //; exact: ltW. + rewrite mulrDl !normrZ -![_ *: _]/(_ * _) (@ger0_norm _ l%:num)//. + by rewrite (@ger0_norm _ l%:num.~)// ?mulrA// onem_ge0. +have : forall z : F', f z <= p (\val z). + by move=> z; rewrite /p (le_trans (ler_norm _)). +move=> /(hahn_banach_extension convp)[g majgp F_eqgf]. +have ling : linear (g : V -> R) by exact: linearP. +have contg : continuous (g : V -> R). + move=> x; apply/continuousfor0_continuous/bounded_linear_continuous. + exists r; split; first exact: gtr0_real. + move=> M rM; rewrite nbhs_ballP; exists 1 => //=. + move=> y; rewrite -ball_normE//= sub0r => y1. + rewrite ler_norml; apply/andP; split. + - rewrite lerNl -linearN (le_trans (majgp (- y)))//. + by rewrite /p -(mul1r M) ltW// ltr_pM// ltW. + - by rewrite (le_trans (majgp y))// /p -(mul1r M) -normrN ltW// ltr_pM// ltW. +pose lcg := isLinearContinuous.Build _ _ _ _ g ling contg. +pose g' : {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) lcg. +by exists g'. +Qed. + +End hahn_banach_normed. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 30e02866ea..a7f0da6485 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -19,6 +19,12 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (* normedModType K == interface type for a normed module *) (* structure over the numDomainType K *) (* The HB class is NormedModule. *) +(* subNormedModType R V S == join of *) +(* SubChoice *) +(* NormedModule *) +(* SubLmodule *) +(* SubNormedZmodule *) +(* SubConvexTvs *) (* normedVectType K == interface type for a normed vectType *) (* structure over the numDomainType K *) (* The HB class is NormedVector. *) @@ -34,6 +40,9 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (* M : normedZmodType K with K : numFieldType. *) (* Lmodule_isNormed M == factory for a normed module defined using *) (* an L-module M over R : numFieldType *) +(* SubLmodule_isSubNormedmodule R V S == factory that builds a *) +(* SubNormedmodule given a SubLmodule over a *) +(* normedModType *) (* ``` *) (* ## Hulls *) (* ``` *) @@ -88,6 +97,13 @@ HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & ConvexTvs K T & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}. +#[short(type="subNormedModType")] +HB.structure Definition SubNormedModule (R : numDomainType) + (V : normedModType R) (S : pred V) := + { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U + & @SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U & + @SubConvexTvs R V S U}. + HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V & PseudoMetricNormedZmod K V & GRing.Lmodule K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; @@ -302,6 +318,29 @@ Module Exports. HB.reexport. End Exports. End pseudoMetric_from_normedZmodType. Export pseudoMetric_from_normedZmodType.Exports. +Section filter_ent. + +Import pseudoMetric_from_normedZmodType. + +Global Instance ent_xsection_filter {R : realFieldType} (U : normedZmodType R) x + : Filter [set P | exists2 A : set (pseudoMetric_normed U * + pseudoMetric_normed U), + ent A & xsection A x `<=` P]. +Proof. +apply: Build_Filter => /=. +- by exists setT => //; exact: (@entourageT (pseudoMetric_normed U)). +- move=> A B/= [A' [r/= r0 ballA'] A'A] [B' [d/= d0 ballB'] B'B]. + exists (A' `&` B'); last by rewrite xsectionI; exact: setISS. + rewrite entourageE /entourage_. + exists (Num.min r d); first by rewrite /= lt_min r0. + move=> z/= Hz; split. + + by apply: ballA' => /=; rewrite /ball/= (lt_le_trans Hz)// ge_min lexx. + + by apply: ballB' => /=; rewrite /ball/= (lt_le_trans Hz)// ge_min lexx orbT. +- by move=> P Q PQ [A entA AP]; exists A => //; exact: (subset_trans AP). +Qed. + +End filter_ent. + HB.factory Record Lmodule_isNormed (R : numFieldType) M & GRing.Lmodule R M := { norm : M -> R; @@ -335,6 +374,57 @@ HB.instance Definition _ := HB.end. +HB.factory Record SubLmodule_isSubNormedmodule (R : realFieldType) + (V : normedModType R) (S : pred V) U & + SubChoice V S U & @GRing.SubLmodule R V S U := {}. + +HB.builders Context R V S U & SubLmodule_isSubNormedmodule R V S U. + +Local Definition normu := fun u : U => `|\val u|. + +Let ler_normuD (x y : U) : normu (x + y) <= normu x + normu y. +Proof. by rewrite /normu GRing.valD; exact: ler_normD. Qed. + +Let normru0_eq0 x : normu x = 0 -> x = 0. +Proof. by move/eqP; rewrite normr_eq0 -(@GRing.val0 V S U) => /eqP/val_inj. Qed. + +Let normruMn x n : normu (x *+ n) = normu x *+ n. +Proof. by rewrite /normu raddfMn /=; exact: normrMn. Qed. + +Let normruN x : normu (- x) = normu x. +Proof. by rewrite /normu raddfN /=; exact: normrN. Qed. + +Let normruZ (l : R) (x : U) : normu (l *: x) = `|l| * normu x. +Proof. by rewrite /normu GRing.valZ; exact: normrZ. Qed. + +HB.instance Definition _ := + @Lmodule_isNormed.Build R U normu ler_normuD normruZ normru0_eq0. + +(* hack, produces no instance with MathComp 2.5.0, + can be remove when supporting MC >= 2.6.0 *) +HB.instance Definition _ := @isTmp.Build R V S U Logic.I. + +Let normu_valE : forall x, @Num.norm _ V ((val : U -> V) x) = @Num.norm _ U x. +Proof. by []. Qed. + +HB.instance Definition _ := Zmodule_isSubNormed.Build _ _ _ U normu_valE. + +Let continuous_valE : continuous (val : U -> V). +Proof. +move=> /= x. +rewrite /continuous_at. +set rhs := (X in _ --> X). +apply/cvgrPdist_le => //=. +move=> e e0; near=> t. +rewrite -GRing.valN -GRing.valD norm_valE. +by near: t; exact: cvgr_dist_le e e0. +Unshelve. all: by end_near. Qed. + +HB.instance Definition _ := isSubNbhs.Build _ _ U continuous_valE. + +HB.instance Definition _ := SubLmodule_isSubNormedmodule.Build _ _ _ U. +HB.end. + Lemma scaler1 {R : numFieldType} h : h%:A = h :> R. Proof. by rewrite /GRing.scale/= mulr1. Qed. @@ -2624,8 +2714,8 @@ have leNoo (x : max_space V) : N x <= M0 * `|x|. by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0. have NC0 : continuous (N : max_space V -> R). move=> /= x; rewrite /continuous_at. - apply: cvg_zero; first exact: nbhs_filter. - apply/cvgr0Pnorm_le; first exact: nbhs_filter. + apply: cvg_zero. + apply/cvgr0Pnorm_le. move=> /= e e0. near=> y. rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index c578687637..01882c6196 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -46,6 +46,11 @@ From mathcomp Require Import pseudometric_normed_Zmodule. (* A convex tvs is constructed over a uniform *) (* space. *) (* The HB class is ConvexTvs. *) +(* subConvexTvsType R V S == join of subTopologicalType, convexTvsType, *) +(* and subLmoduleType *) +(* The HB class is SubConvexTvs. *) +(* Instance: in particular, it is shown that a *) +(* sub-Lmodule is a sub-convex TVS. *) (* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a *) (* convex tvs from an Lmodule which is also a *) (* topological space *) @@ -394,6 +399,99 @@ HB.mixin Record Uniform_isConvexTvs (R : numDomainType) E HB.structure Definition ConvexTvs (R : numDomainType) := {E of Uniform_isConvexTvs R E & Uniform E & TopologicalLmodule R E}. +#[short(type="subConvexTvsType")] +HB.structure Definition SubConvexTvs (R : numDomainType) (V : convexTvsType R) + (S : pred V) := + { U of SubTopological V S U & ConvexTvs R U & @GRing.SubLmodule R V S U }. + +Section SubLmodule_isSubConvexTvs. +Context (R : numFieldType) (V : convexTvsType R) (S : pred V) (U : subLmodType S). + +Local Notation sub_init_topo := (sub_initial_topology U). +HB.instance Definition _ := Uniform.on sub_init_topo. +HB.instance Definition _ := GRing.Lmodule.on sub_init_topo. + +Let add_sub: continuous (fun x : sub_init_topo * sub_init_topo => x.1 + x.2). +Proof. +apply: continuous_comp_initial => -[/= x y]. +pose h := fun xy : U * U => (\val xy.1, \val xy.2). +pose g := fun xy : V * V => xy.1 + xy.2. +rewrite (_ : _ \o _ = g \o h). + by apply/funext => i /=; rewrite GRing.valD. +apply: continuous_comp; last exact: add_continuous. +apply: cvg_pair => //=. +- apply: (cvg_comp _ _ cvg_fst). + exact: (continuous_valE (x : sub_init_topo)). +- apply: (cvg_comp _ _ cvg_snd). + exact: (continuous_valE (y : sub_init_topo)). +Qed. + +HB.instance Definition _ := + @PreTopologicalNmodule_isTopologicalNmodule.Build sub_init_topo add_sub. + +Let opp_sub : continuous (-%R : sub_init_topo -> sub_init_topo). +Proof. +apply: continuous_comp_initial => x. +rewrite (_ : _ \o _ = -%R \o \val). + by apply/funext=> i /=; rewrite GRing.valN. +apply: continuous_comp; first exact: continuous_valE. +exact: opp_continuous. +Qed. + +HB.instance Definition _ := + TopologicalNmodule_isTopologicalZmodule.Build sub_init_topo opp_sub. + +Let scale_sub : continuous (fun z : R^o * sub_init_topo => z.1 *: z.2). +Proof. +apply: continuous_comp_initial => - [] /= x /= y. +pose h := fun xy : R * U => (xy.1, \val xy.2). +pose g := fun xy : R * V => xy.1 *: xy.2. +rewrite (_ : _ \o _ = g \o h); first by apply/funext=> i /=; rewrite GRing.valZ. +apply: continuous_comp; last exact: scale_continuous. +move=> /= A [/= [/= B C]] [[r/= r0 xrB]]. +move/(continuous_valE (y : sub_init_topo)) => [/= C' [woC' C'y C'C] BCA]. +apply: filterS; first exact: BCA. +exists (ball x r, C') => /=. + by split; [exact: nbhsx_ballx|exists C'; split]. +by move=> su/= [xru C'u]; split; [exact: xrB|exact: C'C]. +Qed. + +HB.instance Definition _ := + TopologicalZmodule_isTopologicalLmodule.Build R sub_init_topo scale_sub. + +Local Open Scope convex_scope. + +Let locally_convex_sub : exists2 B : set_system sub_init_topo, + (forall b, b \in B -> convex_set b) & basis B. +Proof. +have [B convexB [openB/= genB]] := @locally_convex R V. +exists [set a | exists2 b, B b & \val @^-1` b = a]. + move=> a /[!inE]/= -[b Bb ba] r s l ra sa. + suff : \val (r <|l|> s) \in b by rewrite !inE /= -ba. + rewrite !GRing.valD !GRing.valZ convexB//; first exact: mem_set. + - by move: ra; rewrite -ba !inE. + - by move: sa; rewrite -ba !inE. +split => /=. + move=> a/= [b Bb <-]; rewrite /open/= /wopen/=; exists b => //. + exact: openB. +move=> x a [/= b [[/=c openc] cb bx ba]]. +rewrite /nbhs/= /filter_from/=. +have : nbhs (val x) c. + rewrite nbhsE /=; exists c => //; split => //. + by move: bx; rewrite -cb. +move/genB => [d [Bd dx dc]]. +exists (\val @^-1` d); first by split => //; exists d. +by move=> y dy; apply: ba; rewrite -cb; exact: dc. +Qed. + +Local Close Scope convex_scope. + +HB.instance Definition _ := + @Uniform_isConvexTvs.Build R sub_init_topo locally_convex_sub. +HB.instance Definition _ := GRing.SubLmodule.on sub_init_topo. + +End SubLmodule_isSubConvexTvs. + Section properties_of_topologicalLmodule. Context (R : numDomainType) (E : preTopologicalLmodType R) (U : set E). diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index c678dd5a9c..f0d861df4d 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -20,8 +20,18 @@ From mathcomp Require Import pseudometric_structure. (* vector space by its dual. *) (* *) (* ``` *) -(* initial_topology f == initial topology by a function f : S -> T on S *) -(* S must be a choiceType and T a topologicalType. *) +(* initial_topology f == initial topology by a function f : S -> T *) +(* on S *) +(* S must be a choiceType and T a *) +(* topologicalType. *) +(* sub_initial_topology V S U == sub-initial topology generated by the *) +(* \val : U -> V *) +(* U has type subChoiceType S with S : pred V. *) +(* This is a subTopologicalType when V is *) +(* endowed with a topology. *) +(* This is a subConvexTvsType when V is *) +(* endowed with a convexTvsType (and when U is *) +(* subLmodType). *) (* ``` *) (* `initial_topology` is equipped with the structures of: *) (* - uniform space *) @@ -96,6 +106,24 @@ End Initial_Topology. HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) := Pointed.on (initial_topology f). +Definition sub_initial_topology (V : Type) (S : pred V) (U : subChoiceType S) + : Type := initial_topology (\val : U -> V). + +Section SubType_isSubTopological. +Context (V : topologicalType) (S : pred V) (U : subChoiceType S). + +Local Notation T := (sub_initial_topology U). +HB.instance Definition _ := SubChoice.on T. +HB.instance Definition _ := Nbhs.on T. +HB.instance Definition _ := Topological.on T. + +Let top_continuous_valE : continuous (val : T -> V). +Proof. exact: initial_continuous. Qed. + +HB.instance Definition _ := @isSubNbhs.Build V S T top_continuous_valE. + +End SubType_isSubTopological. + Section initial_uniform. Local Open Scope relation_scope. Variable (pS : choiceType) (U : uniformType) (f : pS -> U). diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 3733d9de2c..ed7536d335 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -16,6 +16,9 @@ From mathcomp Require Export filter. (* topologicalType == interface type for topological space *) (* structure *) (* the HB class is Topological. *) +(* subTopologicalType S == join of SubNbhs and Topological where S has *) +(* pred V with V a topologicalType *) +(* the HB class is SubTopological. *) (* ptopologicalType == a pointed topologicalType *) (* open == set of open sets *) (* closed == set of closed sets *) @@ -112,6 +115,10 @@ HB.structure Definition PointedTopological := HB.structure Definition BiPointedTopological := { X of BiPointed X & Topological X }. +#[short(type="subTopologicalType")] +HB.structure Definition SubTopological (V : topologicalType) + (S : pred V) := {U of SubNbhs V S U & Topological U}. + Section Topological1. Context {T : topologicalType}.