From 77e0af21c3526dc9eaa07f0cd3f48370cf6f7712 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 6 Jan 2022 20:59:13 +0100 Subject: [PATCH] [CI] adding master Co-Authored-By: Pierre Roux --- .github/workflows/docker-action.yml | 3 + .github/workflows/nix-action-8.13.yml | 4 +- .github/workflows/nix-action-8.14.yml | 4 +- .github/workflows/nix-action-master.yml | 415 ++++++++++++++++++++++++ .nix/config.nix | 10 + .nix/coq-nix-toolbox.nix | 2 +- README.md | 2 +- coq-mathcomp-analysis.opam | 2 +- meta.yml | 10 +- theories/normedtype.v | 10 +- theories/sequences.v | 6 +- 11 files changed, 450 insertions(+), 18 deletions(-) create mode 100644 .github/workflows/nix-action-master.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index f6bcbd239..d916ff8c0 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -21,8 +21,11 @@ jobs: - 'mathcomp/mathcomp:1.12.0-coq-8.14' - 'mathcomp/mathcomp:1.13.0-coq-8.13' - 'mathcomp/mathcomp:1.13.0-coq-8.14' + - 'mathcomp/mathcomp:1.13.0-coq-8.15' + - 'mathcomp/mathcomp:1.13.0-coq-dev' - 'mathcomp/mathcomp-dev:coq-8.13' - 'mathcomp/mathcomp-dev:coq-8.14' + - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.github/workflows/nix-action-8.13.yml b/.github/workflows/nix-action-8.13.yml index 434cc9d73..05a4599fb 100644 --- a/.github/workflows/nix-action-8.13.yml +++ b/.github/workflows/nix-action-8.13.yml @@ -16,7 +16,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v14 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp @@ -53,7 +53,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v14 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp diff --git a/.github/workflows/nix-action-8.14.yml b/.github/workflows/nix-action-8.14.yml index 8cd445a4b..128367202 100644 --- a/.github/workflows/nix-action-8.14.yml +++ b/.github/workflows/nix-action-8.14.yml @@ -16,7 +16,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v14 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp @@ -53,7 +53,7 @@ jobs: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v14 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml new file mode 100644 index 000000000..59c733249 --- /dev/null +++ b/.github/workflows/nix-action-master.yml @@ -0,0 +1,415 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + coq-elpi: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target coq-elpi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq-elpi" + hierarchy-builder: + needs: + - coq + - coq-elpi + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target hierarchy-builder + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"hierarchy-builder\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" + mathcomp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp" + mathcomp-analysis: + needs: + - coq + - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-real-closed + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-analysis" + mathcomp-bigenough: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-bigenough" + mathcomp-finmap: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-finmap + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-finmap" + mathcomp-real-closed: + needs: + - coq + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-real-closed + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-real-closed" +name: Nix CI for bundle master +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index dbc2f81ba..be0104441 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -40,6 +40,16 @@ bundles."8.13".coqPackages.coq.override.version = "8.13"; bundles."8.14".coqPackages.coq.override.version = "8.14"; + bundles."master".coqPackages = { + coq.override.version = "master"; + coq-elpi.override.version = "coq-master"; + hierarchy-builder.override.version = "v1.2.1"; + mathcomp-bigenough.override.version = "1.0.1"; + mathcomp-finmap.override.version = "1.5.1"; + mathcomp-real-closed.override.version = "1.1.2"; + mathcomp.override.version = "1.13.0"; + }; + ## Cachix caches to use in CI ## Below we list some standard ones cachix.coq = {}; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index c45715efc..5a392e7d5 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"f8a44a0138a9f09fe8acc16082196489ab83d39e" +"ccef60688648484a499d367b1e916e8bd36db789" diff --git a/README.md b/README.md index e1e9bb2cd..3873e8510 100644 --- a/README.md +++ b/README.md @@ -37,7 +37,7 @@ the Coq proof-assistant and using the Mathematical Components library. - Pierre-Yves Strub (initial) - Laurent Théry - License: [CeCILL-C](LICENSE) -- Compatible Coq versions: Coq 8.13 to 8.14 (or dev) +- Compatible Coq versions: Coq 8.13 to 8.15 (or dev) - Additional dependencies: - [MathComp ssreflect 1.12 or later](https://math-comp.github.io) - [MathComp fingroup 1.12 or later](https://math-comp.github.io) diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index e8b014379..71c695e5b 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.13" & < "8.15~") | (= "dev") } + "coq" { (>= "8.13" & < "8.16~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.14~") | (= "dev") } "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.14~") | (= "dev") } "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.14~") | (= "dev") } diff --git a/meta.yml b/meta.yml index 84f980cfd..38d0a849a 100644 --- a/meta.yml +++ b/meta.yml @@ -49,8 +49,8 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.13 to 8.14 (or dev) - opam: '{ (>= "8.13" & < "8.15~") | (= "dev") }' + text: Coq 8.13 to 8.15 (or dev) + opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }' tested_coq_opam_versions: - version: '1.12.0-coq-8.13' @@ -61,10 +61,16 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.14' repo: 'mathcomp/mathcomp' +- version: '1.13.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.13.0-coq-dev' + repo: 'mathcomp/mathcomp' - version: 'coq-8.13' repo: 'mathcomp/mathcomp-dev' - version: 'coq-8.14' repo: 'mathcomp/mathcomp-dev' +- version: 'coq-dev' + repo: 'mathcomp/mathcomp-dev' dependencies: - opam: diff --git a/theories/normedtype.v b/theories/normedtype.v index dd15fbef8..83cab60f8 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2893,18 +2893,16 @@ split=> [Ax|[a_ [aTA a_x] ax]]; last first. by apply aTA; exists n. by apply a_U; near: n; exists m. pose U := fun n : nat => [set z : T | `|x - z| < n.+1%:R^-1]. -suff [a_ anx] : exists a_, forall n, a_ n != x /\ (U n `&` A) (a_ n). +suff /(_ _)/cid-/all_sig[a_ anx] : forall n, exists a, a != x /\ (U n `&` A) a. exists a_; split. - by move=> a [n _ <-]; have [? []] := anx n. - by move=> n; have [] := anx n. - apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> n. have [? [] Uan Aan] := anx n. by rewrite (lt_le_trans Uan)// ltW//; near: n; exact: near_infty_natSinv_lt. -have @a_ : nat -> T. - move=> n; have : nbhs (x : T) (U n). - by apply/(nbhs_ballP (x:T) (U n)); rewrite nbhs_ballE; exists n.+1%:R^-1. - by move/Ax/cid => [/= an [anx Aan Uan]]; exact: an. -by exists a_ => n; rewrite /a_ /= /ssr_have; case: cid => ? []. +move=> n; have : nbhs (x : T) (U n). + by apply/(nbhs_ballP (x:T) (U n)); rewrite nbhs_ballE; exists n.+1%:R^-1. +by move/Ax/cid => [/= an [anx Aan Uan]]; exists an. Unshelve. all: by end_near. Qed. Section open_closed_sets. diff --git a/theories/sequences.v b/theories/sequences.v index 4f1d86794..a715a7c2e 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1564,7 +1564,7 @@ rewrite lee_pmul//. - rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin. near: n; apply: (cvg_gt_ge gb) => //. by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n. -Grab Existential Variables. all: end_near. Qed. +Unshelve. all: end_near. Qed. Lemma ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b : (b < 0)%R -> f --> +oo -> g --> b%:E -> f \* g --> -oo. @@ -1580,7 +1580,7 @@ rewrite lee_pmul//. - rewrite EFinM EFinN mulNe lee_opp. rewrite -(@fineK _ (g n)) ?lee_fin; last by near: n; exact: gfin. by near: n; apply: (cvg_lt_le gb) => //; rewrite ltr_nmulr// invf_lt1// ltr1n. -Grab Existential Variables. all: end_near. Qed. +Unshelve. all: end_near. Qed. Lemma ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b : (0 < b)%R -> f --> -oo -> g --> b%:E -> f \* g --> -oo. @@ -1648,7 +1648,7 @@ move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //. - move=> _ foo goo; rewrite mule_ninfty_ninfty -mule_pinfty_pinfty. by under eq_fun do rewrite -muleNN; apply: poopoo; rewrite -/(- -oo); apply: ereal_cvgN. -Grab Existential Variables. all: end_near. Qed. +Unshelve. all: end_near. Qed. Lemma ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I) (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) :