From 16a944a7fe88ac66d1905407be8ad85f69f4352d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 6 Sep 2023 18:25:32 +0200 Subject: [PATCH] Drop support for Coq 8.15 --- .github/workflows/main.yml | 1 - .github/workflows/nix-action-coq-8.15.yml | 670 ---------------------- .nix/config.nix | 8 - HB/common/compat_815.elpi | 2 - HB/common/compat_all.elpi | 2 - HB/common/log.elpi | 2 +- coq-hierarchy-builder.opam | 2 +- structures.v | 36 -- tests/about.v.out.15 | 149 ----- tests/compress_coe.v.out.15 | 21 - tests/hnf.v.out.15 | 12 - 11 files changed, 2 insertions(+), 903 deletions(-) delete mode 100644 .github/workflows/nix-action-coq-8.15.yml delete mode 100644 HB/common/compat_815.elpi delete mode 100644 HB/common/compat_all.elpi delete mode 100644 tests/about.v.out.15 delete mode 100644 tests/compress_coe.v.out.15 delete mode 100644 tests/hnf.v.out.15 diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8227457f..8479474e 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -17,7 +17,6 @@ jobs: fail-fast: false matrix: coq_version: - - '8.15' - '8.16' - '8.17' steps: diff --git a/.github/workflows/nix-action-coq-8.15.yml b/.github/workflows/nix-action-coq-8.15.yml deleted file mode 100644 index 3dff0f8d..00000000 --- a/.github/workflows/nix-action-coq-8.15.yml +++ /dev/null @@ -1,670 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - 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 \"coq-8.15\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\ - \ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coq" - coq-bits: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq-bits - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"coq-bits\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\ - \ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coq" - - 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 "coq-8.15" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coq-bits" - fourcolor: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target fourcolor - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"fourcolor\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\ - \ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coq" - - 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 "coq-8.15" - --argstr job "mathcomp-algebra" - - 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 "coq-8.15" - --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 "coq-8.15" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "fourcolor" - hierarchy-builder: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - 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 \"coq-8.15\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --argstr job "hierarchy-builder" - hierarchy-builder-shim: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target hierarchy-builder-shim - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"hierarchy-builder-shim\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --argstr job "hierarchy-builder-shim" - interval: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target interval - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\ - \ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coquelicot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coquelicot" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: flocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "flocq" - - 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 "coq-8.15" - --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 "coq-8.15" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "interval" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - 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 \"coq-8.15\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --argstr job "mathcomp-finmap" - mathcomp-single: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"mathcomp-single\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --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 "coq-8.15" - --argstr job "mathcomp-single" - mathcomp-single-planB-src: - needs: - - coq - - hierarchy-builder - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-single-planB-src - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --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 "coq-8.15" - --argstr job "coq-elpi" - - 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 "coq-8.15" - --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 "coq-8.15" - --argstr job "mathcomp-single-planB-src" - odd-order: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target odd-order - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\ - \ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "coq" - - 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 "coq-8.15" - --argstr job "mathcomp-character" - - 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 "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "mathcomp" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "odd-order" - reglang: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target reglang - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.15\" --argstr job \"reglang\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\ - \ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --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 "coq-8.15" - --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 "coq-8.15" - --argstr job "reglang" -name: Nix CI for bundle coq-8.15 -'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 3edfe83a..6c416c10 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -38,14 +38,6 @@ "coq-8.16".coqPackages = mcHBcommon // { coq.override.version = "8.16"; }; - - "coq-8.15".coqPackages = mcHBcommon // { - coq.override.version = "8.15"; - mathcomp.job = false; - mathcomp-classical.job = false; - mathcomp-analysis.job = false; - mathcomp-infotheo.job = false; - }; }; cachix.coq = {}; cachix.coq-community = {}; diff --git a/HB/common/compat_815.elpi b/HB/common/compat_815.elpi deleted file mode 100644 index 322124f7..00000000 --- a/HB/common/compat_815.elpi +++ /dev/null @@ -1,2 +0,0 @@ -pred compat.coercion.declare i:coercion. -compat.coercion.declare C :- @global! => coq.coercion.declare C. diff --git a/HB/common/compat_all.elpi b/HB/common/compat_all.elpi deleted file mode 100644 index 5cd6cadc..00000000 --- a/HB/common/compat_all.elpi +++ /dev/null @@ -1,2 +0,0 @@ -pred compat.coercion.declare i:coercion. -compat.coercion.declare C :- @global! => @reversible! => coq.coercion.declare C. diff --git a/HB/common/log.elpi b/HB/common/log.elpi index f98c733a..5e86d403 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -159,7 +159,7 @@ env.import-module MPNice M :- std.do! [ pred coercion.declare i:coercion. coercion.declare C :- std.do! [ - compat.coercion.declare C, + @global! => @reversible! => coq.coercion.declare C, C = coercion GR _ SRCGR TGTCL, coq.gref->id GR Name, log.private.log-vernac (log.private.coq.vernac.coercion Name SRCGR TGTCL), diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index d677c47a..f8f6f85e 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -12,7 +12,7 @@ build: [ [ make "build"] [ make "test-suite" ] {with-test} ] install: [ make "install" ] -depends: [ "coq-elpi" { (>= "1.14" & < "1.20~") | = "dev" } ] +depends: [ "coq-elpi" { (>= "1.15" & < "1.20~") | = "dev" } ] conflicts: [ "coq-hierarchy-builder-shim" ] synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" description: """ diff --git a/structures.v b/structures.v index 0efec3a6..cfe1a247 100644 --- a/structures.v +++ b/structures.v @@ -244,8 +244,6 @@ Elpi Accumulate Db hb.db. the commands. To this end, we accumulate the DB first in each command to ensure the same dependencies and maximize cache hits. For instance, this can save a few (2 or 3) percents of total compilation time on MathComp. *) -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate lp:{{ main [str S] :- !, @@ -274,8 +272,6 @@ Elpi Export HB.locate. #[arguments(raw)] Elpi Command HB.about. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -309,8 +305,6 @@ Elpi Export HB.about. #[arguments(raw)] Elpi Command HB.howto. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -352,8 +346,6 @@ Elpi Export HB.howto. #[arguments(raw)] Elpi Command HB.status. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -382,8 +374,6 @@ tred file.dot | xdot - #[arguments(raw)] Elpi Command HB.graph. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -432,8 +422,6 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := { #[arguments(raw)] Elpi Command HB.mixin. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -495,8 +483,6 @@ Elpi Export HB.mixin. Elpi Tactic HB.pack_for. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -519,8 +505,6 @@ Elpi Export HB.pack_for. Elpi Tactic HB.pack. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -605,8 +589,6 @@ HB.structure Definition StructureName params := #[arguments(raw)] Elpi Command HB.structure. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -661,8 +643,6 @@ HB.instance Definition N Params := Factory.Build Params T … #[arguments(raw)] Elpi Command HB.instance. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -694,8 +674,6 @@ Elpi Export HB.instance. #[arguments(raw)] Elpi Command HB.factory. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -756,8 +734,6 @@ HB.end. #[arguments(raw)] Elpi Command HB.builders. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -782,8 +758,6 @@ Elpi Export HB.builders. #[arguments(raw)] Elpi Command HB.end. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -836,8 +810,6 @@ Export Algebra.Exports. #[arguments(raw)] Elpi Command HB.export. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -864,8 +836,6 @@ Elpi Export HB.export. #[arguments(raw)] Elpi Command HB.reexport. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -912,8 +882,6 @@ Notation foo := foo.body. #[arguments(raw)] Elpi Command HB.lock. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -963,8 +931,6 @@ HB.instance Definition _ : Ml ... T := ml. #[arguments(raw)] Elpi Command HB.declare. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". @@ -1000,8 +966,6 @@ Elpi Export HB.declare. #[arguments(raw)] Elpi Command HB.check. Elpi Accumulate Db hb.db. -#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". -#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/database.elpi". #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". diff --git a/tests/about.v.out.15 b/tests/about.v.out.15 deleted file mode 100644 index bd8d9aa6..00000000 --- a/tests/about.v.out.15 +++ /dev/null @@ -1,149 +0,0 @@ -HB: AddMonoid_of_TYPE is a factory - (from "./examples/demo1/hierarchy_5.v", line 10) -HB: AddMonoid_of_TYPE operations and axioms are: - - zero - - add - - addrA - - add0r - - addr0 -HB: AddMonoid_of_TYPE requires the following mixins: -HB: AddMonoid_of_TYPE provides the following mixins: - - AddMonoid_of_TYPE - -HB: AddMonoid_of_TYPE.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 10) -HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: -HB: AddMonoid_of_TYPE.Build provides the following mixins: - - AddMonoid_of_TYPE -HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - - S : Type - - zero : AddMonoid.sort S - - add : S -> S -> S - - addrA : associative add - - add0r : left_id 0%G add - - addr0 : right_id 0%G add - -HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) -HB: AddAG.type characterizing operations and axioms are: - - addNr - - opp -HB: AddAG is a factory for the following mixins: - - AddMonoid_of_TYPE - - AddComoid_of_AddMonoid - - AddAG_of_AddComoid (* new, not from inheritance *) -HB: AddAG inherits from: - - AddMonoid - - AddComoid -HB: AddAG is inherited by: - - Ring - -HB: AddMonoid.type is a structure - (from "./examples/demo1/hierarchy_5.v", line 17) -HB: AddMonoid.type characterizing operations and axioms are: - - addr0 - - add0r - - addrA - - add - - zero -HB: AddMonoid is a factory for the following mixins: - - AddMonoid_of_TYPE (* new, not from inheritance *) -HB: AddMonoid inherits from: -HB: AddMonoid is inherited by: - - AddComoid - - AddAG - - BiNearRing - - SemiRing - - Ring - -HB: Ring_of_AddAG is a factory - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG operations and axioms are: - - one - - mul - - mulrA - - mulr1 - - mul1r - - mulrDl - - mulrDr -HB: Ring_of_AddAG requires the following mixins: - - AddMonoid_of_TYPE - - AddComoid_of_AddMonoid - - AddAG_of_AddComoid -HB: Ring_of_AddAG provides the following mixins: - - BiNearRing_of_AddMonoid -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: Ring_of_AddAG.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - AddMonoid_of_TYPE - - AddComoid_of_AddMonoid - - AddAG_of_AddComoid -HB: Ring_of_AddAG.Build provides the following mixins: - - BiNearRing_of_AddMonoid -HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - - A : Type - - one : A - - mul : A -> A -> A - - mulrA : associative mul - - mulr1 : left_id one mul - - mul1r : right_id one mul - - mulrDl : left_distributive mul add - - mulrDr : right_distributive mul add -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: add is an operation of structure AddMonoid - (from "./examples/demo1/hierarchy_5.v", line 17) -HB: add comes from mixin AddMonoid_of_TYPE - (from "./examples/demo1/hierarchy_5.v", line 10) - -HB: AddAG.sort is a canonical projection - (from "./examples/demo1/hierarchy_5.v", line 73) -HB: AddAG.sort has the following canonical values: - - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - - Z - -HB: AddAG.sort is a coercion from AddAG to Sortclass - (from "./examples/demo1/hierarchy_5.v", line 73) - -HB: Z is canonically equipped with structures: - - AddMonoid - AddComoid - AddAG - (from "(stdin)", line 5) - - BiNearRing - SemiRing - Ring - (from "(stdin)", line 10) - -HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) - -HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) - -HB: synthesized in file File "(stdin)", line 5, column 122, character 127: -Interactive Module hierarchy_5 started -Interactive Module AddComoid started -HB: Z is canonically equipped with structures: - - AddMonoid - demo1.hierarchy_5.AddComoid - AddAG - (from "(stdin)", line 5) - - BiNearRing - SemiRing - Ring - (from "(stdin)", line 10) - diff --git a/tests/compress_coe.v.out.15 b/tests/compress_coe.v.out.15 deleted file mode 100644 index 0d249e43..00000000 --- a/tests/compress_coe.v.out.15 +++ /dev/null @@ -1,21 +0,0 @@ -Datatypes_prod__canonical__compress_coe_D = -fun D D' : D.type => -{| - D.sort := D.sort D * D.sort D'; - D.class := - {| - D.compress_coe_hasA_mixin := - prodA (compress_coe_D__to__compress_coe_A D) - (compress_coe_D__to__compress_coe_A D'); - D.compress_coe_hasB_mixin := - prodB tt (compress_coe_D__to__compress_coe_B D) - (compress_coe_D__to__compress_coe_B D'); - D.compress_coe_hasC_mixin := - prodC tt tt (compress_coe_D__to__compress_coe_C D) - (compress_coe_D__to__compress_coe_C D'); - D.compress_coe_hasD_mixin := prodD D D' - |} -|} - : D.type -> D.type -> D.type - -Arguments Datatypes_prod__canonical__compress_coe_D D D' diff --git a/tests/hnf.v.out.15 b/tests/hnf.v.out.15 deleted file mode 100644 index a7211d45..00000000 --- a/tests/hnf.v.out.15 +++ /dev/null @@ -1,12 +0,0 @@ -Datatypes_nat__canonical__hnf_S = -{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} - : S.type -HB_unnamed_mixin_8 = -{| M.x := f.y nat HB_unnamed_factory_6 + 1 |} - : M.axioms_ nat -Datatypes_bool__canonical__hnf_S = -{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} - : S.type -HB_unnamed_mixin_12 = -Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9 - : M.axioms_ bool