diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index d353e1778..8de5871a4 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -16,7 +16,7 @@ jobs: strategy: matrix: coq_version: - - '8.17' + - '8.18' ocaml_version: - '4.09-flambda' - '4.13-flambda' diff --git a/.github/workflows/nix-action-coq-8.17.yml b/.github/workflows/nix-action-coq-8.17.yml deleted file mode 100644 index 1c46b950d..000000000 --- a/.github/workflows/nix-action-coq-8.17.yml +++ /dev/null @@ -1,1278 +0,0 @@ -jobs: - addition-chains: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra - - mathcomp-fingroup - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target addition-chains - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"addition-chains\" \\\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 "coq-8.17" - --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.17" - --argstr job "mathcomp-ssreflect" - - 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.17" - --argstr job "mathcomp-algebra" - - 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.17" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: paramcoq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "paramcoq" - - 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.17" - --argstr job "addition-chains" - category-theory: - needs: - - coq - - mathcomp-ssreflect - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target category-theory - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"category-theory\" \\\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 "coq-8.17" - --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.17" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "equations" - - 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.17" - --argstr job "category-theory" - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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.17\" --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 "coq-8.17" - --argstr job "coq" - coq-elpi: - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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 \"coq-8.17\" --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 "coq-8.17" - --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.17" - --argstr job "coq-elpi" - coquelicot: - needs: - - coq - - mathcomp-ssreflect - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target coquelicot - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"coquelicot\" \\\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 "coq-8.17" - --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.17" - --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.17" - --argstr job "coquelicot" - hierarchy-builder: - needs: - - coq - - coq-elpi - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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.17\" --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 "coq-8.17" - --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.17" - --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.17" - --argstr job "hierarchy-builder" - interval: - needs: - - coq - - coquelicot - - mathcomp-ssreflect - - mathcomp-fingroup - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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.17\" --argstr job \"interval\" \\\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 "coq-8.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --argstr job "interval" - mathcomp: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - mathcomp-character - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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 \"coq-8.17\" --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 "coq-8.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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 "coq-8.17" - --argstr job "mathcomp-character" - - 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.17" - --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.17" - --argstr job "mathcomp" - mathcomp-algebra: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-algebra - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-algebra\" \\\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 "coq-8.17" - --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.17" - --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.17" - --argstr job "mathcomp-fingroup" - - 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.17" - --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.17" - --argstr job "mathcomp-algebra" - mathcomp-analysis: - needs: - - coq - - mathcomp-classical - - mathcomp-field - - mathcomp-bigenough - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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 \"coq-8.17\" --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 "coq-8.17" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.17" - --argstr job "mathcomp-classical" - - 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.17" - --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 "coq-8.17" - --argstr job "mathcomp-bigenough" - - 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.17" - --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.17" - --argstr job "mathcomp-analysis" - mathcomp-bigenough: - needs: - - coq - - mathcomp-ssreflect - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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 \"coq-8.17\" --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 "coq-8.17" - --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.17" - --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.17" - --argstr job "mathcomp-bigenough" - mathcomp-character: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-character - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-character\" \\\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 "coq-8.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --argstr job "mathcomp-field" - - 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.17" - --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.17" - --argstr job "mathcomp-character" - mathcomp-classical: - needs: - - coq - - mathcomp-algebra - - hierarchy-builder - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-classical - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-classical\" \\\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 "coq-8.17" - --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.17" - --argstr job "mathcomp-algebra" - - 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.17" - --argstr job "hierarchy-builder" - - 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.17" - --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.17" - --argstr job "mathcomp-classical" - mathcomp-field: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-field - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-field\" \\\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 "coq-8.17" - --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.17" - --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.17" - --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.17" - --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.17" - --argstr job "mathcomp-solvable" - - 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.17" - --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.17" - --argstr job "mathcomp-field" - mathcomp-fingroup: - needs: - - coq - - mathcomp-ssreflect - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-fingroup - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-fingroup\" \\\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 "coq-8.17" - --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.17" - --argstr job "mathcomp-ssreflect" - - 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.17" - --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.17" - --argstr job "mathcomp-fingroup" - mathcomp-solvable: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-solvable - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-solvable\" \\\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 "coq-8.17" - --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.17" - --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.17" - --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.17" - --argstr job "mathcomp-algebra" - - 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.17" - --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.17" - --argstr job "mathcomp-solvable" - mathcomp-ssreflect: - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target mathcomp-ssreflect - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"mathcomp-ssreflect\" \\\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 "coq-8.17" - --argstr job "coq" - - 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.17" - --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.17" - --argstr job "mathcomp-ssreflect" - odd-order: - needs: - - coq - - mathcomp-character - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - mathcomp - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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.17\" --argstr job \"odd-order\" \\\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 "coq-8.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --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.17" - --argstr job "odd-order" - trakt: - needs: - - coq - - coq-elpi - 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 coq-elpi - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target trakt - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.17\" --argstr job \"trakt\" \\\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 "coq-8.17" - --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.17" - --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.17" - --argstr job "trakt" -name: Nix CI for bundle coq-8.17 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.gitignore b/.gitignore index f24dc3406..a8d712e50 100644 --- a/.gitignore +++ b/.gitignore @@ -43,4 +43,7 @@ tests/test_glob/*.css META -*.cache \ No newline at end of file +*.cache + +apps/coercion/src/coq_elpi_coercion_hook.ml +.filestoinstall \ No newline at end of file diff --git a/Changelog.md b/Changelog.md index e613aaab6..19985282a 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,18 @@ # Changelog +## [1.19.0] - 04/08/2023 + +Requires Elpi 1.16.5 and Coq 8.18. + +### APPS +- New `coercion` app providing `coercion` predicate + to program coercions (thanks @proux01). + This app is experimental. + +### API: +- Removed option `@nonuniform!` as it disappears from Coq 8.18. + (c.f. https://github.com/coq/coq/pull/17716 ) + ## [1.18.0] - 27/07/2023 Requires Elpi 1.16.5 and Coq 8.17. diff --git a/Makefile b/Makefile index f10353683..8455c470a 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ export ELPIDIR DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma -APPS=$(addprefix apps/, derive eltac NES locker) +APPS=$(addprefix apps/, derive eltac NES locker coercion) ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" "" DOCDEP=build diff --git a/Makefile.coq.local b/Makefile.coq.local index de6e205d3..ae2d441fc 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -1,6 +1,7 @@ CAMLPKGS+= -package elpi,stdlib-shims CAMLFLAGS+= -bin-annot -g OCAMLWARN+=-warn-error -32 +COQEXTRAFLAGS=-bt theories/elpi.vo: $(wildcard elpi/*.elpi) diff --git a/README.md b/README.md index ddb40ed50..bcb537507 100644 --- a/README.md +++ b/README.md @@ -152,7 +152,9 @@ all the dependencies installed first (see [coq-elpi.opam](coq-elpi.opam)). - [Dx](https://gitlab.univ-lille.fr/samuel.hym/dx) uses elpi to generate an intermediate representation of Coq terms, to be later tranformed into C. - +- [Coercion](apps/coercion) enable to program coercions in Elpi. + It comes bundled with Coq-Elpi. + ### Quick Reference In order to load Coq-Elpi use `From elpi Require Import elpi`. diff --git a/_CoqProject b/_CoqProject index 13c179c0a..1e0d91b72 100644 --- a/_CoqProject +++ b/_CoqProject @@ -17,6 +17,7 @@ -R apps/eltac/theories elpi.apps.eltac -R apps/eltac/tests elpi.apps.eltac.tests -R apps/eltac/examples elpi.apps.eltac.examples +-R apps/coercion/theories elpi.apps.coercion theories/elpi.v theories/wip/memoization.v diff --git a/apps/coercion/Makefile b/apps/coercion/Makefile new file mode 100644 index 000000000..9b84ee407 --- /dev/null +++ b/apps/coercion/Makefile @@ -0,0 +1,40 @@ +# detection of coq +ifeq "$(COQBIN)" "" +COQBIN := $(shell which coqc >/dev/null 2>&1 && dirname `which coqc`) +endif +ifeq "$(COQBIN)" "" +$(error Coq not found, make sure it is installed in your PATH or set COQBIN) +else +$(info Using coq found in $(COQBIN), from COQBIN or PATH) +endif +export COQBIN := $(COQBIN)/ + +all: build test + +build: Makefile.coq + @$(MAKE) --no-print-directory -f Makefile.coq + +test: Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq + +theories/%.vo: force + @$(MAKE) --no-print-directory -f Makefile.coq $@ +tests/%.vo: force build Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq $@ +examples/%.vo: force build Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq $@ + +Makefile.coq Makefile.coq.conf: _CoqProject + @$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq + @$(MAKE) --no-print-directory -f Makefile.coq .merlin +Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test + @$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq + +clean: Makefile.coq Makefile.test.coq + @$(MAKE) -f Makefile.coq $@ + @$(MAKE) -f Makefile.test.coq $@ + +.PHONY: force all build test + +install: + @$(MAKE) -f Makefile.coq $@ diff --git a/apps/coercion/Makefile.coq.local b/apps/coercion/Makefile.coq.local new file mode 100644 index 000000000..f120308b2 --- /dev/null +++ b/apps/coercion/Makefile.coq.local @@ -0,0 +1,3 @@ +CAMLPKGS+= -package coq-elpi.elpi +OCAMLPATH:=../../src/:$(OCAMLPATH) +export OCAMLPATH \ No newline at end of file diff --git a/apps/coercion/README.md b/apps/coercion/README.md new file mode 100644 index 000000000..acd6131a4 --- /dev/null +++ b/apps/coercion/README.md @@ -0,0 +1,80 @@ +# Coercion + +The `coercion` app enables to program Coq coercions in Elpi. + +This app is experimental. + +## The coercion predicate + +The `coercion` predicate lives in the database `coercion.db` + +```elpi +% [coercion Ctx V Inferred Expected Res] is queried to cast V to Res +% - [Ctx] is the context +% - [V] is the value to be coerced +% - [Inferred] is the type of [V] +% - [Expected] is the type [V] should be coerced to +% - [Res] is the result (of type [Expected]) +pred coercion i:goal-ctx, i:term, i:term, i:term, o:term. +``` + +By addings rules for this predicate one can recover from a type error, that is +when `Inferred` and `Expected` are not unifiable. + +## Simple example of coercion + +This example maps `True : Prop` to `true : bool`, which is a function you +cannot express in type theory, hence in the standard Coercion system. + +```coq +From elpi.apps Require Import coercion. +From Coq Require Import Bool. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}. +coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}. + +}}. +Elpi Typecheck coercion. (* checks the elpi program is OK *) + +Check True && False. +``` + +## Example of coercion with proof automation + +This coercion enriches `x : T` to a `{x : T | P x}` by using +`my_solver` to prove `P x`. + +```coq +From elpi.apps Require Import coercion. +From Coq Require Import Arith ssreflect. + +Ltac my_solver := trivial with arith. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [ + % we unfold letins since the solver is dumb and the `as` in the second + % example introduces a letin + (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1, + % we build the solution + Solution = {{ @exist lp:Ty lp:P lp:X1 _ }}, + % we call the solver + coq.ltac.collect-goals Solution [G] [], + coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [], +]. + +}}. +Elpi Typecheck coercion. + +Goal {x : nat | x > 0}. +apply: 3. +Qed. + +Definition ensure_pos n : {x : nat | x > 0} := + match n with + | O => 1 + | S x as y => y + end. +``` diff --git a/apps/coercion/_CoqProject b/apps/coercion/_CoqProject new file mode 100644 index 000000000..b5b8d84f0 --- /dev/null +++ b/apps/coercion/_CoqProject @@ -0,0 +1,14 @@ +# Hack to see Coq-Elpi even if it is not installed yet +-Q ../../theories elpi +-I ../../src +-docroot elpi.apps + +-R theories elpi.apps + +src/coq_elpi_coercion_hook.mlg +src/elpi_coercion_plugin.mlpack + +-I src/ +src/META.coq-elpi-coercion + +theories/coercion.v diff --git a/apps/coercion/_CoqProject.test b/apps/coercion/_CoqProject.test new file mode 100644 index 000000000..e6e1f59ad --- /dev/null +++ b/apps/coercion/_CoqProject.test @@ -0,0 +1,13 @@ +# Hack to see Coq-Elpi even if it is not installed yet +-Q ../../theories elpi +-I ../../src +-docroot elpi.apps + +-R theories elpi.apps +-R tests elpi.apps.coercion.tests + +tests/test_coercion.v +tests/test_coercion_open.v +tests/test_coercion_load.v + +-I src diff --git a/apps/coercion/src/META.coq-elpi-coercion b/apps/coercion/src/META.coq-elpi-coercion new file mode 100644 index 000000000..507e9af0e --- /dev/null +++ b/apps/coercion/src/META.coq-elpi-coercion @@ -0,0 +1,10 @@ + +package "plugin" ( + directory = "." + requires = "coq-core.plugins.ltac coq-elpi.elpi" + archive(byte) = "elpi_coercion_plugin.cma" + archive(native) = "elpi_coercion_plugin.cmxa" + plugin(byte) = "elpi_coercion_plugin.cma" + plugin(native) = "elpi_coercion_plugin.cmxs" +) +directory = "." diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg new file mode 100644 index 000000000..89b8d0d45 --- /dev/null +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -0,0 +1,58 @@ +DECLARE PLUGIN "coq-elpi-coercion.plugin" + +{ + +open Elpi +open Elpi_plugin +open Coq_elpi_arg_syntax +open Coq_elpi_vernacular + + +let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = + let loc = API.Ast.Loc.initial "(unknown)" in + let atts = [] in + let sigma, goal = Evarutil.new_evar env sigma expected in + let goal_evar, _ = EConstr.destEvar sigma goal in + let query ~depth state = + let state, (loc, q), gls = + Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred]) + ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in + let state, qatts = atts2impl loc ~depth state atts q in + let state = API.State.set Coq_elpi_builtins.tactic_mode state true in + state, (loc, qatts), gls + in + let cprogram, _ = get_and_compile program in + match run ~static_check:false cprogram (`Fun query) with + | API.Execute.Success solution -> + let gls = Evar.Set.singleton goal_evar in + let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in + if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None + | API.Execute.NoMoreSteps + | API.Execute.Failure -> None + | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None + +let add_coercion_hook = + let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in + let coercion_hook env sigma ~flags v ~inferred ~expected = + match !coercion_hook_program with + | None -> None + | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in + let name = "elpi-coercion" in + Coercion.register_hook ~name coercion_hook; + let inCoercion = + let cache program = + coercion_hook_program := Some program; + Coercion.activate_hook ~name in + let open Libobject in + declare_object + @@ superglobal_object_nodischarge "ELPI-COERCION" ~cache ~subst:None in + fun program -> Lib.add_leaf (inCoercion program) + +} + +VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF +| #[ atts = any_attribute ] [ "Elpi" "CoercionFallbackTactic" qualified_name(p) ] -> { + let () = ignore_unknown_attributes atts in + add_coercion_hook (snd p) } + +END \ No newline at end of file diff --git a/apps/coercion/src/elpi_coercion_plugin.mlpack b/apps/coercion/src/elpi_coercion_plugin.mlpack new file mode 100644 index 000000000..0e41afce5 --- /dev/null +++ b/apps/coercion/src/elpi_coercion_plugin.mlpack @@ -0,0 +1 @@ +Coq_elpi_coercion_hook \ No newline at end of file diff --git a/apps/coercion/tests/test_coercion.v b/apps/coercion/tests/test_coercion.v new file mode 100644 index 000000000..932605cb2 --- /dev/null +++ b/apps/coercion/tests/test_coercion.v @@ -0,0 +1,34 @@ +From elpi.apps Require Import coercion. +From Coq Require Import Bool. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}. +coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}. + +}}. +Elpi Typecheck coercion. + +Check True && False. + +Parameter ringType : Type. +Parameter ringType_sort : ringType -> Type. +Parameter natmul : forall (R : ringType) (n : nat), (ringType_sort R). + +Elpi Accumulate coercion.db lp:{{ + +coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :- + coq.typecheck R {{ ringType }} ok. + +}}. +Elpi Typecheck coercion. + +Section TestNatMul. + +Variable R : ringType. +Variable n : nat. + +Check natmul R n : ringType_sort R. +Check n : ringType_sort R. + +End TestNatMul. diff --git a/apps/coercion/tests/test_coercion_load.v b/apps/coercion/tests/test_coercion_load.v new file mode 100644 index 000000000..ee11df134 --- /dev/null +++ b/apps/coercion/tests/test_coercion_load.v @@ -0,0 +1,3 @@ +Require Import test_coercion. + +Check True : bool. diff --git a/apps/coercion/tests/test_coercion_open.v b/apps/coercion/tests/test_coercion_open.v new file mode 100644 index 000000000..4adcb6c57 --- /dev/null +++ b/apps/coercion/tests/test_coercion_open.v @@ -0,0 +1,29 @@ +From elpi.apps Require Import coercion. +From Coq Require Import Arith ssreflect. + +Ltac my_solver := trivial with arith. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [ + % we unfold letins since the solve is dumb + (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1, + % we build the solution + Solution = {{ @exist lp:Ty lp:P lp:X1 _ }}, + % we call the solver + coq.ltac.collect-goals Solution [G] [], + coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [], +]. + +}}. +Elpi Typecheck coercion. + +Goal {x : nat | x > 0}. +apply: 3. +Qed. + +Definition add1 n : {x : nat | x > 0} := + match n with + | O => 1 + | S x as y => y + end. diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v new file mode 100644 index 000000000..c4b50c273 --- /dev/null +++ b/apps/coercion/theories/coercion.v @@ -0,0 +1,25 @@ +Declare ML Module "coq-elpi-coercion.plugin". +From elpi Require Import elpi. + +Elpi Db coercion.db lp:{{ + +% predicate [coercion Ctx V Inferred Expected Res] used to add new coercion, with +% - [Ctx] is the context +% - [V] is the value to be coerced +% - [Inferred] is the type of [V] +% - [Expected] is the type [V] should be coerced to +% - [Res] is the result (of type [Expected]) +% Be careful not to trigger coercion as this may loop. +pred coercion i:goal-ctx, i:term, i:term, i:term, o:term. + +}}. + +Elpi Tactic coercion. +Elpi Accumulate lp:{{ + +solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol. + +}}. +Elpi Accumulate Db coercion.db. +Elpi Typecheck. +Elpi CoercionFallbackTactic coercion. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 64f2d3a08..f8008b533 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -355,7 +355,6 @@ macro @global! :- get-option "coq:locality" "global". macro @local! :- get-option "coq:locality" "local". macro @primitive! :- get-option "coq:primitive" tt. % primitive records -macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions macro @reversible! :- get-option "coq:reversible" tt. % coercions macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference diff --git a/coq-elpi.opam b/coq-elpi.opam index 3ec186694..1682397f4 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -15,7 +15,7 @@ install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] depends: [ "stdlib-shims" "elpi" {>= "1.16.5" & < "1.18.0~"} - "coq" {>= "8.17" & < "8.18~" } + "coq" {>= "8.18" & < "8.19~" } ] tags: [ "category:Miscellaneous/Coq Extensions" diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 9cda7e407..272635bcc 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -340,7 +340,6 @@ macro @global! :- get-option "coq:locality" "global". macro @local! :- get-option "coq:locality" "local". macro @primitive! :- get-option "coq:primitive" tt. % primitive records -macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions macro @reversible! :- get-option "coq:reversible" tt. % coercions macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 7a5538136..8c65bd859 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -67,7 +67,7 @@ let pre_engine : coq_engine S.component option ref = ref None module UnivOrd = struct type t = Univ.Universe.t let compare = Univ.Universe.compare - let show x = Pp.string_of_ppcmds (Univ.Universe.pr x) + let show x = Pp.string_of_ppcmds (Univ.Universe.pr UnivNames.pr_with_global_universes x) let pp fmt x = Format.fprintf fmt "%s" (show x) end module UnivSet = U.Set.Make(UnivOrd) @@ -75,7 +75,7 @@ module UnivMap = U.Map.Make(UnivOrd) module UnivLevelOrd = struct type t = Univ.Level.t let compare = Univ.Level.compare - let show x = Pp.string_of_ppcmds (Univ.Level.pr x) + let show x = Pp.string_of_ppcmds (UnivNames.pr_with_global_universes x) let pp fmt x = Format.fprintf fmt "%s" (show x) end module UnivLevelSet = U.Set.Make(UnivLevelOrd) @@ -85,8 +85,8 @@ module UnivLevelMap = U.Map.Make(UnivLevelOrd) module UM = F.Map(struct type t = Univ.Universe.t let compare = Univ.Universe.compare - let show x = Pp.string_of_ppcmds @@ Univ.Universe.pr x - let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr x) + let show x = Pp.string_of_ppcmds @@ Univ.Universe.pr UnivNames.pr_with_global_universes x + let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr UnivNames.pr_with_global_universes x) end) let um = S.declare ~name:"coq-elpi:evar-univ-map" @@ -111,7 +111,7 @@ let add_universe_constraint state c = | UGraph.UniverseInconsistency p -> Feedback.msg_debug (UGraph.explain_universe_inconsistency - UnivNames.(pr_with_global_universes empty_binders) p); + UnivNames.pr_with_global_universes p); raise API.BuiltInPredicate.No_clause | Evd.UniversesDiffer | UState.UniversesDiffer -> Feedback.msg_debug Pp.(str"UniversesDiffer"); @@ -138,7 +138,7 @@ let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) = CD.name = "univ"; doc = "universe level (algebraic: max, +1, univ.variable)"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (Univ.Universe.pr x) in + let s = Pp.string_of_ppcmds (Univ.Universe.pr UnivNames.pr_with_global_universes x) in Format.fprintf fmt "«%s»" s); compare = Univ.Universe.compare; hash = Univ.Universe.hash; @@ -172,7 +172,8 @@ let sort = | Sorts.Type _ -> Format.fprintf fmt "Type" | Sorts.Set -> Format.fprintf fmt "Set" | Sorts.Prop -> Format.fprintf fmt "Prop" - | Sorts.SProp -> Format.fprintf fmt "SProp"); + | Sorts.SProp -> Format.fprintf fmt "SProp" + | Sorts.QSort _ -> Format.fprintf fmt "Type"); constructors = [ K("prop","impredicative sort of propositions",N, B Sorts.prop, @@ -206,7 +207,7 @@ let universe_level_variable = CD.name = "univ.variable"; doc = "universe level variable"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (Univ.Level.pr x) in + let s = Pp.string_of_ppcmds (UnivNames.pr_with_global_universes x) in Format.fprintf fmt "«%s»" s); compare = Univ.Level.compare; hash = Univ.Level.hash; @@ -339,7 +340,6 @@ type options = { inline : Declaremods.inline; uinstance : uinstanceoption; universe_decl : universe_decl_option; - nonuniform : bool option; reversible : bool option; keepunivs : bool option; redflags : CClosure.RedFlags.reds option; @@ -359,7 +359,6 @@ let default_options () = { inline = Declaremods.NoInline; uinstance = NoInstance; universe_decl = NotUniversePolymorphic; - nonuniform = None; reversible = None; keepunivs = None; redflags = None; @@ -478,7 +477,7 @@ let uinstancein, isuinstance, uinstanceout, uinstance = CD.name = "univ-instance"; doc = "Universes level instance for a universe-polymoprhic constant"; pp = (fun fmt x -> - let s = Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr x) in + let s = Pp.string_of_ppcmds (Univ.Instance.pr UnivNames.pr_with_global_universes x) in Format.fprintf fmt "«%s»" s); compare = (fun x y -> CArray.compare Univ.Level.compare (Univ.Instance.to_array x) (Univ.Instance.to_array y)); @@ -908,7 +907,7 @@ let force_level_of_universe state u = let purge_algebraic_univs_sort state s = let sigma = (S.get engine state).sigma in match EConstr.ESorts.kind sigma s with - | Sorts.Type u -> + | Sorts.Type u | Sorts.QSort (_ , u) -> let state, _, _, s = force_level_of_universe state u in state, s | x -> state, x @@ -1129,7 +1128,6 @@ let get_options ~depth hyps state = inline = get_module_inline_option "coq:inline"; uinstance = get_uinstance_option "coq:uinstance"; universe_decl = get_universe_decl (); - nonuniform = get_bool_option "coq:nonuniform"; reversible = get_bool_option "coq:reversible"; no_tc = get_bool_option "coq:no_tc"; keepunivs = get_bool_option "coq:keepunivs"; @@ -1222,7 +1220,8 @@ let restrict_coq_context live_db state { proof; proof_len; local; name2db; env; let info_of_evar ~env ~sigma ~section k = let open Context.Named in - let info = Evarutil.nf_evar_info sigma (Evd.find sigma k) in + let evi = Evd.find_undefined sigma k in + let info = Evarutil.nf_evar_info sigma evi in let filtered_hyps = Evd.evar_filtered_hyps info in let ctx = EC.named_context_of_val filtered_hyps in let ctx = ctx |> CList.filter (fun x -> @@ -1510,7 +1509,7 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x -> | None -> x, (None, None)) |> (fun (x,(y,z)) -> x,y,z) let evar_arity k state = - let info = Evd.find (S.get engine state).sigma k in + let EvarInfo info = Evd.find (S.get engine state).sigma k in let filtered_hyps = Evd.evar_filtered_hyps info in List.length (Environ.named_context_of_val filtered_hyps) @@ -1561,7 +1560,7 @@ let pp_cst fmt { E.goal = (depth,concl); context } = (P.term depth) concl let find_evar var csts = - csts |> CList.find_map (fun ({ E.goal = (depth,concl); context } as cst) -> + csts |> CList.find_map_exn (fun ({ E.goal = (depth,concl); context } as cst) -> match E.look ~depth concl with | E.App(c,x,[ty;rx]) when c == evarc -> begin match E.look ~depth x, E.look ~depth rx with @@ -1607,7 +1606,7 @@ let rec dblset_of_canonical_ctx ~depth acc = function str(pp2string (P.term depth) x)) let find_evar_decl var csts = - csts |> CList.find_map (fun ({ E.goal = (depth,concl); context } as cst) -> + csts |> CList.find_map_exn (fun ({ E.goal = (depth,concl); context } as cst) -> match E.look ~depth concl with | E.App(c,x,[ty;rx]) when c == evarc -> begin match E.look ~depth x, E.look ~depth rx with @@ -1644,8 +1643,8 @@ module UIM = F.Map(struct type t = Univ.Instance.t let compare i1 i2 = CArray.compare Univ.Level.compare (Univ.Instance.to_array i1) (Univ.Instance.to_array i2) - let show x = Pp.string_of_ppcmds @@ Univ.Instance.pr Univ.Level.pr x - let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr Univ.Level.pr x) + let show x = Pp.string_of_ppcmds @@ Univ.Instance.pr UnivNames.pr_with_global_universes x + let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr UnivNames.pr_with_global_universes x) end) let uim = S.declare ~name:"coq-elpi:evar-univ-instance-map" @@ -1772,15 +1771,15 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals match E.look ~depth t with | E.App(s,p,[]) when sortc == s -> let state, u, gsl = sort.API.Conversion.readback ~depth state p in - state, EC.mkSort u, gsl + state, EC.mkSort (EC.ESorts.make u), gsl (* constants *) | E.App(c,d,[]) when globalc == c -> let state, gr = in_coq_gref ~depth ~origin:t ~failsafe:coq_ctx.options.failsafe state d in begin match gr with | G.VarRef x -> state, EC.mkVar x, [] - | G.ConstRef x -> state, EC.mkConst x, [] - | G.ConstructRef x -> state, EC.mkConstruct x, [] - | G.IndRef x -> state, EC.mkInd x, [] + | G.ConstRef x -> state, EC.UnsafeMonomorphic.mkConst x, [] + | G.ConstructRef x -> state, EC.UnsafeMonomorphic.mkConstruct x, [] + | G.IndRef x -> state, EC.UnsafeMonomorphic.mkInd x, [] end | E.App(c,d,[i]) when pglobalc == c -> let state, gr, i, gls = @@ -1880,7 +1879,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals | _ -> assert false end Sorts.Relevant C.LetStyle in let b = List.hd bt in - let l, _ = EC.decompose_lam (get_sigma state) b in + let l, _ = EC.decompose_lambda (get_sigma state) b in let ci_pp_info = { unknown_ind_cinfo.Constr.ci_pp_info with Constr.cstr_tags = [| List.map (fun _ -> false) l |] } in { unknown_ind_cinfo with Constr.ci_pp_info} in @@ -1916,7 +1915,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals begin match v with | Uint63 i -> state, EC.mkInt i, gls | Float64 f -> state, EC.mkFloat f, gls - | Projection p -> state, EC.mkConst (Names.Projection.constant p), gls + | Projection p -> state, EC.UnsafeMonomorphic.mkConst (Names.Projection.constant p), gls end (* evar *) @@ -2185,7 +2184,7 @@ let customtac2query sigma goals loc text ~depth:calldepth state = | [] | _ :: _ :: _ -> CErrors.user_err Pp.(str "elpi query can only be used on one goal") | [goal] -> - let info = Evd.find sigma goal in + let EvarInfo info = Evd.find sigma goal in let env = get_global_env state in let env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env in if not (Evd.is_undefined sigma goal) then @@ -2358,9 +2357,9 @@ let get_declared_goals all_goals constraints state assignments pp_ctx = *) let rec reachable1 sigma root acc = - let info = Evd.find sigma root in - let res = if Evd.evar_body info == Evd.Evar_empty then Evar.Set.add root acc else acc in - let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma (Evd.find sigma root) in + let EvarInfo info = Evd.find sigma root in + let res = match Evd.evar_body info with Evd.Evar_empty -> Evar.Set.add root acc | Evd.Evar_defined _ -> acc in + let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma info in if Evar.Set.equal res acc then acc else reachable sigma res res and reachable sigma roots acc = Evar.Set.fold (reachable1 sigma) roots acc @@ -2411,7 +2410,7 @@ let set_current_sigma ~depth state sigma = let state = set_sigma state sigma in let state, assignments, decls, to_remove_coq, to_remove_elpi = UVMap.fold (fun k elpi_raw_evk elpi_evk solution (state, assignments, decls, to_remove_coq, to_remove_elpi as acc) -> - let info = Evd.find sigma k in + let EvarInfo info = Evd.find sigma k in match Evd.evar_body info with | Evd.Evar_empty -> acc | Evd.Evar_defined c -> @@ -2654,7 +2653,7 @@ let readback_arity ~depth coq_ctx constraints state t = let inference_nonuniform_params_off = CWarnings.create ~name:"elpi.unsupported-nonuniform-parameters-inference" - ~category:"elpi" Pp.(fun () -> + ~category:Coq_elpi_utils.elpi_cat Pp.(fun () -> strbrk"Inference of non-uniform parameters is not available in Elpi, please use the explicit | mark in the inductive declaration or Set Uniform Inductive Parameters") let restricted_sigma_of s state = @@ -3135,7 +3134,7 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,uinst,(mind,ind), let sigma = get_sigma state in let drop_nparams_from_term n x = let x = EConstr.of_constr x in - let ctx, sort = EConstr.decompose_prod_assum sigma x in + let ctx, sort = EConstr.decompose_prod_decls sigma x in let ctx = drop_nparams_from_ctx n ctx in EConstr.it_mkProd_or_LetIn sort ctx in let decl = @@ -3148,7 +3147,7 @@ let inductive_decl2lp ~depth coq_ctx constraints state (mutind,uinst,(mind,ind), Term.it_mkProd_or_LetIn x ctx |> Inductive.abstract_constructor_type_relatively_to_inductive_types_context ntyps mutind in let nonexpimplsno = List.length (nonexpimpls impls) in - let ctx, typ = Term.decompose_prod_n_assum (max allparamsno nonexpimplsno) x in + let ctx, typ = Term.decompose_prod_n_decls (max allparamsno nonexpimplsno) x in let ctx = EConstr.of_rel_context ctx in let typ = EConstr.of_constr typ in let ctx = safe_combine2_impls ctx impls ~default2:Glob_term.Explicit in @@ -3302,7 +3301,7 @@ let record_entry2lp ~depth coq_ctx constraints state ~loose_udecl e = let kid = List.hd ind.mind_entry_consnames in let fieldsno = List.length record.proj_flags in - let kctx, _ = Term.decompose_prod_assum @@ List.hd ind.mind_entry_lc in + let kctx, _ = Term.decompose_prod_decls @@ List.hd ind.mind_entry_lc in let kctx = EConstr.of_rel_context kctx in if (List.length kctx != fieldsno) then CErrors.anomaly Pp.(str"record fields number != projections"); @@ -3404,7 +3403,7 @@ let lp2skeleton ~depth coq_ctx constraints state t = let gt = let is_GRef_hole x = match DAst.get x with - | Glob_term.GRef(r,None) -> Names.GlobRef.equal r (Coqlib.lib_ref "elpi.hole") + | Glob_term.GRef(r,None) -> Environ.QGlobRef.equal coq_ctx.env r (Coqlib.lib_ref "elpi.hole") | _ -> false in let rec map x = match DAst.get x with | Glob_term.GEvar _ -> mkGHole @@ -3442,7 +3441,7 @@ let rec in_elpi_module_item ~depth path state (name, item) = and functor_params x = let open Declarations in match x with - | MoreFunctor(_,{ mod_type_alg = Some (NoFunctor (MEident mod_mp)) },rest) -> mod_mp :: functor_params rest + | MoreFunctor(_,{ mod_type_alg = Some (MENoFunctor (MEident mod_mp)) },rest) -> mod_mp :: functor_params rest | _ -> [] (* XXX non trivial functors, eg P : X with type a = nat, are badly described (no params) *) and in_elpi_module : 'a. depth:int -> API.Data.state -> 'a Declarations.generic_module_body -> module_item list = diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index 0371e3b57..97901a856 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -43,7 +43,6 @@ type options = { inline : Declaremods.inline; uinstance : uinstanceoption; universe_decl : universe_decl_option; - nonuniform : bool option; reversible : bool option; keepunivs : bool option; redflags : CClosure.RedFlags.reds option; diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index b2b4dec84..83875d7f1 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -205,7 +205,7 @@ let univpoly_of ~poly ~cumulative = if notations != [] then CErrors.user_err Pp.(str "notations not supported"); let name = [Names.Id.to_string name.CAst.v] in let constructors = - List.map (function (Vernacexpr.(NoCoercion,NoInstance),c) -> c + List.map (function (Vernacexpr.(_,NoCoercion,NoInstance),c) -> c | _ -> CErrors.user_err Pp.(str "coercion and instance flags not supported")) constructors in let { template; udecl; cumulative; poly; finite } = flags in @@ -300,7 +300,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly } let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it -let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) +let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous) let raw_context_decl_to_glob glob_sign fields = let _intern_env, fields = intern_global_context ~intern_env:Constrintern.empty_internalization_env glob_sign fields in @@ -684,6 +684,11 @@ let in_elpi_term_arg ~depth state coq_ctx hyps sigma ist glob_or_expr = let state, t = Coq_elpi_glob_quotation.gterm2lp ~depth state g in state, E.mkApp trmc t [], [] +let in_elpi_tac_econstr ~depth ?calldepth coq_ctx hyps sigma state x = + let state, gls0 = set_current_sigma ~depth state sigma in + let state, t, gls1 = Coq_elpi_HOAS.constr2lp ~depth ?calldepth coq_ctx E.no_constraints state x in + state, [E.mkApp trmc t []], gls0 @ gls1 + let in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr = let sigma, t = Ltac_plugin.Tacinterp.interp_open_constr_with_classes ist coq_ctx.env sigma glob_or_expr in let state, gls0 = set_current_sigma ~depth state sigma in diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli index 56d3901b8..09a08a4c6 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/coq_elpi_arg_HOAS.mli @@ -95,6 +95,16 @@ val in_elpi_tac : Tac.top -> Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals +(* for coercions *) +val in_elpi_tac_econstr : + depth:int -> ?calldepth:int -> + Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context -> + Coq_elpi_HOAS.hyp list -> + Evd.evar_map -> + Elpi.API.State.t -> + EConstr.t -> + Elpi.API.State.t * term list * Elpi.API.Conversion.extra_goals + (* for commands *) val in_elpi_cmd : depth:int -> ?calldepth:int -> diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index 4649b7f0b..334c87c0f 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -62,18 +62,18 @@ let pr_fp _ _ _ (_,x) = U.pr_qualified_name x let pp_elpi_loc _ _ _ (l : Loc.t) = Pp.mt () let the_qname = ref "" -let any_qname strm = +let any_qname kwstate strm = let re = Str.regexp "[A-Za-z][A-Za-z0-9]*\\(\\.?[A-Za-z][A-Za-z0-9]*\\)*" in - match LStream.peek strm with + match LStream.peek kwstate strm with | Some (Tok.KEYWORD sym) when Str.string_match re sym 0 -> let pos = LStream.count strm in let _, ep = Loc.unloc (LStream.get_loc pos strm) in - LStream.junk strm; - begin match LStream.peek strm with + LStream.junk kwstate strm; + begin match LStream.peek kwstate strm with | Some (Tok.IDENT id) -> let bp, _ = Loc.unloc (LStream.get_loc (pos+1) strm) in if Int.equal ep bp then - (LStream.junk strm; the_qname := sym ^ id) + (LStream.junk kwstate strm; the_qname := sym ^ id) else the_qname := sym | _ -> the_qname := sym @@ -100,9 +100,9 @@ END { -let telescope = Pcoq.Entry.create "elpi:telescope" -let colon_sort = Pcoq.Entry.create "elpi:colon_sort" -let colon_constr = Pcoq.Entry.create "elpi:colon_constr" +let telescope = Pcoq.Entry.make "elpi:telescope" +let colon_sort = Pcoq.Entry.make "elpi:colon_sort" +let colon_constr = Pcoq.Entry.make "elpi:colon_constr" let any_attribute : Attributes.vernac_flags Attributes.attribute = Attributes.make_attribute (fun x -> [],x) @@ -132,14 +132,14 @@ let validate_attributes a flags = ignore_unknown_attributes extra; raw_args -let coq_kwd_or_symbol = Pcoq.Entry.create "elpi:kwd_or_symbol" +let coq_kwd_or_symbol = Pcoq.Entry.make "elpi:kwd_or_symbol" let opt2list = function None -> [] | Some l -> l let the_kwd = ref "" -let any_kwd strm = - match LStream.peek strm with - | Some (Tok.KEYWORD sym) when sym <> "." -> LStream.junk strm; the_kwd := sym +let any_kwd kwstate strm = + match LStream.peek kwstate strm with + | Some (Tok.KEYWORD sym) when sym <> "." -> LStream.junk kwstate strm; the_kwd := sym | _ -> raise Stream.Failure let any_kwd = Pcoq.Entry.(of_parser "any_symbols_or_kwd" { parser_fun = any_kwd }) @@ -280,7 +280,7 @@ ARGUMENT EXTEND ltac_attributes Ltac_plugin.Tacinterp.interp_ltac_var (Ltac_plugin.Tacinterp.Value.cast (Genarg.topwit wit_attributes)) ist None (CAst.make id) | _ -> assert false } GLOBALIZED BY { fun gsig t -> fst @@ Ltac_plugin.Tacintern.intern_constr gsig t } - SUBSTITUTED BY { Detyping.subst_glob_constr (Global.env()) } + SUBSTITUTED BY { fun x -> Detyping.subst_glob_constr (Global.env()) x } RAW_PRINTED BY { fun _ _ _ -> Ppconstr.pr_constr_expr env sigma } GLOB_PRINTED BY { fun _ _ _ -> Printer.pr_glob_constr_env env sigma } | [ ident(v) ] -> { (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string v,None)) } diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index dc5004520..8e9c74e0a 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -95,7 +95,7 @@ let pr_econstr_env options env sigma t = let expr = Constrextern.extern_constr env sigma t in let expr = let rec aux () ({ CAst.v } as orig) = match v with - | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in if options.hoas_holes = Some Heuristic then aux () expr else expr in Ppconstr.pr_constr_expr_n env sigma options.pplevel expr) @@ -149,7 +149,7 @@ let err_if_contains_alg_univ ~depth t = begin match Univ.Universe.level u with | None -> err Pp.(strbrk "The hypothetical clause contains terms of type univ which are not global, you should abstract them out or replace them by global ones: " ++ - Univ.Universe.pr u) + Univ.Universe.pr UnivNames.pr_with_global_universes u) | _ -> Univ.Universe.Set.add u acc end | x -> Coq_elpi_utils.fold_elpi_term aux acc ~depth x @@ -171,7 +171,7 @@ let mk_algebraic_super x = Sorts.super x let univ_super state u v = let state, u = match u with | Sorts.Set | Sorts.Prop | Sorts.SProp -> state, u - | Sorts.Type ul -> + | Sorts.Type ul | Sorts.QSort (_, ul) -> if Univ.Universe.is_level ul then state, u else let state, (_,w) = new_univ_level_variable state in @@ -731,7 +731,7 @@ let attribute_value = let open API.AlgebraicData in let open CConv in declare { let attribute = attribute attribute_value -let warning = CWarnings.create ~name:"lib" ~category:"elpi" Pp.str +let warning = CWarnings.create ~name:"lib" ~category:elpi_cat Pp.str let keep x = (x = Pred.Keep) @@ -847,7 +847,7 @@ let ppboxes = let open Conv in let open Pp in let open API.AlgebraicData in decl let warn_deprecated_add_axiom = CWarnings.create ~name:"elpi.add-const-for-axiom-or-sectionvar" - ~category:"elpi.deprecated" + ~category:elpi_depr_cat Pp.(fun () -> strbrk ("elpi: Using coq.env.add-const for declaring axioms or " ^ "section variables is deprecated. Use coq.env.add-axiom or " ^ @@ -889,12 +889,13 @@ type tac_abbrev = { tac_fixed_args : Coq_elpi_arg_HOAS.Tac.glob list; } +type ('a,'d) gbpmp = Gbpmp : ('d, _, 'b, Loc.t -> 'd) Pcoq.Rule.t * ('a -> 'b) -> ('a,'d) gbpmp -let rec gbpmp = fun f -> function - | [x] -> Pcoq.Rule.next Pcoq.Rule.stop (Pcoq.Symbol.token (Tok.PIDENT(Some x))), (fun a _ -> f a) +let rec gbpmp f = function + | [x] -> Gbpmp (Pcoq.Rule.next Pcoq.Rule.stop (Pcoq.Symbol.token (Tok.PIDENT(Some x))), (fun a _ -> f a)) | x :: xs -> - let r, f = gbpmp f xs in - Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a) + let Gbpmp (r, f) = gbpmp f xs in + Gbpmp (Pcoq.Rule.next r (Pcoq.Symbol.token (Tok.PFIELD (Some x))), (fun a _ -> f a)) | [] -> assert false let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = more_args } = @@ -914,7 +915,7 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor | Coq_elpi_arg_HOAS.Tac.Term (t,_) -> let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in let rec aux () ({ CAst.v } as orig) = match v with - | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous,None) + | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in Coq_elpi_arg_HOAS.Tac.Term (aux () expr) | _ -> assert false) in @@ -923,13 +924,13 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Tac.Term(arg)) in let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in (TacML (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)])) in - CAst.make @@ Constrexpr.CHole (None, Namegen.IntroAnonymous, Some (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac))) in - let rule, action = gbpmp (Obj.magic action) (List.rev abbrev_name) in + CAst.make @@ Constrexpr.CGenarg (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac)) in + let Gbpmp (rule, action) = gbpmp action (List.rev abbrev_name) in Pcoq.grammar_extend Pcoq.Constr.term (Pcoq.Fresh (Gramlib.Gramext.Before "10", - [ (None, None, [ Pcoq.Production.make - (Pcoq.Rule.next (Obj.magic rule) (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) - (Obj.magic action) + [ (None, None, [ Pcoq.Production.make + (Pcoq.Rule.next rule (Pcoq.Symbol.list0 (Pcoq.Symbol.nterm Pcoq.Constr.arg))) + action ])])) let subst_abbrev_for_tac (subst, { abbrev_name; tac_name; tac_fixed_args }) = { @@ -951,17 +952,16 @@ let cache_tac_abbrev qualid = cache_abbrev_for_tac { let cache_goption_declaration (depr,key,value) = let open Goptions in + let depr = if depr then Some (Deprecation.make ~note:"elpi" ()) else None in match value with | BoolValue x -> - let _ : unit -> bool = Goptions.declare_bool_option_and_ref ~key ~value:x ~depr in + let _ : bool Goptions.getter = Goptions.declare_bool_option_and_ref ~key ~value:x ?depr () in () | IntValue x -> - let _ : unit -> int option = Goptions.declare_intopt_option_and_ref ~key ~depr in - Goptions.set_int_option_value key x; + let _ : int option Goptions.getter = Goptions.declare_intopt_option_and_ref ~stage:Interp ~key ?depr ~value:x () in () | StringOptValue x -> - let _ : unit -> string option = Goptions.declare_stringopt_option_and_ref ~key ~depr in - Option.iter (Goptions.set_string_option_value key) x; + let _ : string option Goptions.getter = Goptions.declare_stringopt_option_and_ref ~stage:Interp ~key ?depr ~value:x () in () | StringValue _ -> assert false @@ -1083,12 +1083,12 @@ let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes = | IndRef ind -> let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - Reduction.inductive_cumulativity_arguments (mib,snd ind), Univ.AbstractContext.size univs + Conversion.inductive_cumulativity_arguments (mib,snd ind), Univ.AbstractContext.size univs | ConstructRef (ind,kno) -> let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - Reduction.constructor_cumulativity_arguments (mib,snd ind,kno), Univ.AbstractContext.size univs + Conversion.constructor_cumulativity_arguments (mib,snd ind,kno), Univ.AbstractContext.size univs in let l1 = Univ.Instance.length ui1 in let l2 = Univ.Instance.length ui2 in @@ -1118,7 +1118,7 @@ let unify_instances_gref gr ui1 ui2 diag env state cmp_constr_universes = | _ -> let msg = UGraph.explain_universe_inconsistency - UnivNames.(pr_with_global_universes empty_binders) p in + UnivNames.pr_with_global_universes p in state, !: (B.mkERROR (Pp.string_of_ppcmds msg)), [] let gref_set, gref_set_decl = B.ocaml_set_conv ~name:"coq.gref.set" gref (module GRSet) @@ -1326,8 +1326,18 @@ let coq_builtins = Prints a warning message with a Name and Category which can be used to silence this warning or turn it into an error. See coqc -w command line option|}))), - (fun category name args ~depth _hyps _constraints state -> - let warning = CWarnings.create ~name ~category Pp.str in + (fun category_name name args ~depth _hyps _constraints state -> + let category = match CWarnings.get_category category_name with + | There c -> c + | OtherType -> CErrors.anomaly Pp.(str category_name ++ str "is a warning, not a warning category.") + | NotThere -> CWarnings.create_category ~from:[elpi_cat] ~name:category_name () + in + let w = match CWarnings.get_warning name with + | There w -> w + | OtherType -> CErrors.anomaly Pp.(str name ++ str " is a warning category, not a warning.") + | NotThere -> CWarnings.create_warning ~from:[category] ~name () + in + let warning = CWarnings.create_in w Pp.str in let pp = pp ~depth in let loc, args = if args = [] then None, args @@ -1339,7 +1349,7 @@ line option|}))), | _ -> None, x :: args in let txt = pp2string (P.list ~boxed:true pp " ") args in - if coq_warning_cache category name loc txt then warning ?loc txt; + if coq_warning_cache category_name name loc txt then warning ?loc txt; state, ())), DocAbove); @@ -1601,7 +1611,7 @@ regarded as not non-informative).|})), match indbo.Declarations.mind_kelim with | (Sorts.InSProp | Sorts.InProp) -> raise No_clause | Sorts.InSet when Environ.is_impredicative_set env -> raise No_clause - | (Sorts.InSet | Sorts.InType) -> () + | (Sorts.InSet | Sorts.InType | Sorts.InQSort) -> () )), DocAbove); @@ -2046,7 +2056,7 @@ Supported attributes: let is_implicit = List.map (fun _ -> []) names in let open Entries in let k_ty = List.(hd (hd me.mind_entry_inds).mind_entry_lc) in - let fields_as_relctx = Term.prod_assum k_ty in + let fields_as_relctx = Term.prod_decls k_ty in let projections = Record.Internal.declare_projections ind ~kind:Decls.Definition (uentry, ubinders) @@ -2689,9 +2699,7 @@ Supported attributes: (fun gr priority ~depth { options } _ -> grab_global_env "coq.TC.declare-instance" (fun state -> let global = if options.local = Some false then Hints.SuperGlobal else Hints.Local in let hint_priority = Some priority in - let qualid = - Nametab.shortest_qualid_of_global Names.Id.Set.empty gr in - Classes.existing_instance global qualid + Classes.existing_instance global gr (Some { Hints.empty_hint_info with Typeclasses.hint_priority }); state, (), []))), DocAbove); @@ -2716,7 +2724,7 @@ Supported attributes: Out(list tc_instance, "Db", Read(global,"reads all instances of the given class GR"))), (fun gr _ ~depth { env } _ state -> - !: (Typeclasses.instances env (get_sigma state) gr))), + !: (Typeclasses.instances_exn env (get_sigma state) gr))), DocAbove); MLCode(Pred("coq.TC.class?", @@ -2743,15 +2751,14 @@ NParams can always be omitted, since it is inferred. (fun (gr, _, source, target) ~depth { options } _ -> grab_global_env "coq.coercion.declare" (fun state -> let local = options.local <> Some false in let poly = false in - let nonuniform = options.nonuniform = Some true in let reversible = options.reversible = Some true in begin match source, target with | B.Given source, B.Given target -> let source = ComCoercion.class_of_global source in ComCoercion.try_add_new_coercion_with_target gr ~local ~poly - ~nonuniform ~reversible ~source ~target + ~reversible ~source ~target | _, _ -> - ComCoercion.try_add_new_coercion gr ~local ~poly ~nonuniform ~reversible + ComCoercion.try_add_new_coercion gr ~local ~poly ~reversible end; state, (), []))), DocAbove); @@ -3050,7 +3057,7 @@ Supported attributes: { nenv with Notation_term.ninterp_var_type = Id.Map.add id (Notation_term.NtnInternTypeAny None) nenv.Notation_term.ninterp_var_type }, - (id, ((Constrexpr.InConstrEntrySomeLevel,([],[])),Notation_term.NtnTypeConstr)) :: vars in + (id, ((Constrexpr.(InConstrEntry,(LevelSome,None)),([],[])),Notation_term.NtnTypeConstr)) :: vars in let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum(name,ty)) env in aux vars nenv env (n-1) t | _ -> @@ -3095,7 +3102,7 @@ Supported attributes: let binders, vars = List.split (CList.init nargs (fun i -> let name = Coq_elpi_glob_quotation.mk_restricted_name i in let lname = CAst.make @@ Name.Name (Id.of_string name) in - CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous,None)), + CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous)), (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in let sigma = get_sigma state in @@ -3125,7 +3132,7 @@ Supported attributes: let binders, vars = List.split (CList.init nargs (fun i -> let name = Coq_elpi_glob_quotation.mk_restricted_name i in let lname = CAst.make @@ Name.Name (Id.of_string name) in - CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous,None)), + CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous)), (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in let sigma = get_sigma state in @@ -3198,7 +3205,7 @@ Universe constraints are put in the constraint store.|})))), let sigma, ty = Typing.type_of proof_context.env sigma t in match ety with | Data ety -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL ty ety in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in let state, assignments = set_current_sigma ~depth state sigma in state, ?: None +! B.mkOK, assignments | NoData -> @@ -3230,14 +3237,14 @@ Universe constraints are put in the constraint store.|})))), let sigma, s = Typing.sort_of proof_context.env sigma ty in match es with | Data es -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL (EConstr.mkSort s) (EConstr.mkSort es) in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL (EConstr.mkSort s) (EConstr.mkSort (EConstr.ESorts.make es)) in let state, assignments = set_current_sigma ~depth state sigma in state, !: es +! B.mkOK, assignments | NoData -> let flags = Evarconv.default_flags_of TransparentState.full in let sigma = Evarconv.solve_unif_constraints_with_heuristics ~flags ~with_ho:true proof_context.env sigma in let state, assignments = set_current_sigma ~depth state sigma in - state, !: s +! B.mkOK, assignments + state, !: (EConstr.ESorts.kind sigma s) +! B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> match diag with | Data B.OK -> @@ -3256,7 +3263,7 @@ Universe constraints are put in the constraint store.|})))), (fun a b diag ~depth proof_context _ state -> let sigma = get_sigma state in try - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CONV a b in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CONV a b in let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> @@ -3277,7 +3284,7 @@ Universe constraints are put in the constraint store.|})))), (fun a b diag ~depth proof_context _ state -> let sigma = get_sigma state in try - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL a b in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL a b in let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> @@ -3324,7 +3331,7 @@ Supported attributes: let state, assignments = set_current_sigma ~depth state sigma in state, ?: None +! uj_val +! B.mkOK, assignments | `NoUnify ety -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Reduction.CUMUL uj_type ety in + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL uj_type ety in let state, assignments = set_current_sigma ~depth state sigma in state, ?: None +! uj_val +! B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> @@ -3591,7 +3598,7 @@ fold_left over the terms, letin body comes before the type). let free_evars = let cache = Evarutil.create_undefined_evars_cache () in let map ev = - let evi = Evd.find sigma ev in + let EvarInfo evi = Evd.find sigma ev in let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in (ev, fevs) in @@ -3640,15 +3647,15 @@ fold_left over the terms, letin body comes before the type). Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in let _, pv = init sigma [] in let (), pv, _, _ = - let vernac_state = Vernacstate.freeze_interp_state ~marshallable:false in + let vernac_state = Vernacstate.freeze_full_state () in try let rc = apply ~name:(Id.of_string "elpi") ~poly:false proof_context.env focused_tac pv in - let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_interp_state ~marshallable:false) in + let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in - Vernacstate.unfreeze_interp_state vernac_state; + Vernacstate.unfreeze_full_state vernac_state; rc with e when CErrors.noncritical e -> - Vernacstate.unfreeze_interp_state vernac_state; + Vernacstate.unfreeze_full_state vernac_state; Feedback.msg_debug (CErrors.print e); raise Pred.No_clause in @@ -3711,7 +3718,7 @@ fold_left over the terms, letin body comes before the type). (fun name _ ~depth -> let table = Goptions.get_tables () in match Goptions.OptionMap.find_opt name table with - | Some { Goptions.opt_depr = x; _ } -> !: x + | Some { Goptions.opt_depr = x; _ } -> !: (Option.has_some x) | None -> raise No_clause)), DocAbove); diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 0f65f4ce3..bd1e2fbb4 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -168,7 +168,7 @@ let rec gterm2lp ~depth state x = let state, f = F.Elpi.make state in let s = API.RawData.mkUnifVar f ~args:[] state in state, in_elpi_flex_sort s - | GSort(UNamed u) -> + | GSort(UNamed (None, u)) -> let env = get_glob_env state in in_elpi_sort ~depth state (sort_name env (get_sigma state) u) | GSort(_) -> nYI "(glob)HOAS for Type@{i j}" @@ -194,7 +194,7 @@ let rec gterm2lp ~depth state x = let state, t, () = under_ctx name ty (Some bo) (nogls gterm2lp) ~depth state t in state, in_elpi_let name bo ty t - | GHole(_,_,Some arg) when !is_elpi_code arg -> + | GGenarg arg when !is_elpi_code arg -> let loc, text = !get_elpi_code arg in let s, x = Q.lp ~depth state loc text in let s, x = @@ -208,7 +208,7 @@ let rec gterm2lp ~depth state x = in (* Format.eprintf "unquote: %a\n" (Elpi_API.Extend.Pp.term depth) x; *) s, x - | GHole(_,_,Some arg) when !is_elpi_code_appArg arg -> + | GGenarg arg when !is_elpi_code_appArg arg -> begin match !get_elpi_code_appArg arg with | _, [] -> assert false | loc, hd :: vars -> @@ -222,7 +222,9 @@ let rec gterm2lp ~depth state x = state, mkApp ~depth hd args end - | GHole (_,_,None) -> + | GGenarg _ -> nYI "(glob)HOAS for GGenarg" + + | GHole _ -> let state, uv = F.Elpi.make state in let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in let args = @@ -234,8 +236,6 @@ let rec gterm2lp ~depth state x = in state, E.mkUnifVar uv ~args state - | GHole _ -> nYI "(glob)HOAS for GHole" - | GCast(t,_,c_ty) -> let state, t = gterm2lp ~depth state t in let state, c_ty = gterm2lp ~depth state c_ty in @@ -342,11 +342,13 @@ let rec gterm2lp ~depth state x = assert(List.length def <= 1); let bs = CList.init no_constructors (fun i -> let cno = i + 1 in - try CList.find_map (function + match CList.find_map (function | `Case((_,n as k),vars,bo) when n = cno -> Some (k,vars,bo) | `Case _ -> None | `Def _ -> assert false) bs - with Not_found -> + with + | Some v -> v + | None -> match def with | [`Def bo] -> let missing_k = ind,cno in diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index d65b011fe..9ce389a97 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -14,8 +14,8 @@ let debug_vars = Summary.ref ~name:"elpi-debug" EC.StrSet.empty let cc_flags () = { EC.default_flags with EC.defined_variables = !debug_vars } -let source_cache1 = Summary.Local.ref ~name:"elpi-units1" Names.KNmap.empty -let source_cache2 = Summary.Local.ref ~name:"elpi-units2" CString.Map.empty +let source_cache1 = Summary.ref ~local:true ~name:"elpi-units1" Names.KNmap.empty +let source_cache2 = Summary.ref ~local:true ~name:"elpi-units2" CString.Map.empty let last_kn = ref None @@ -23,7 +23,6 @@ let in_source : Names.Id.t -> string option * EC.compilation_unit * EC.flags -> let open Libobject in let cache ((_,kn), (hash,u,cf)) = last_kn := Some kn; - let open Summary.Local in source_cache1 := Names.KNmap.add kn (u,cf) !source_cache1; hash |> Option.iter (fun hash -> source_cache2 := CString.Map.add hash kn !source_cache2); in @@ -46,7 +45,6 @@ let intern_unit (hash,u,flags) = last_kn := None; Lib.add_leaf (in_source id (hash,u,flags)); let kn = Option.get !last_kn in - let open Summary.Local in let u,_ = Names.KNmap.find kn !source_cache1 in kn,u @@ -61,7 +59,6 @@ let unit_from_ast ~elpi ~flags h ast = CErrors.user_err ?loc Pp.(str (Option.default "" @@ Option.map API.Ast.Loc.show oloc) ++ cut () ++ str msg) let unit_from_file ~elpi x : cunit = - let open Summary.Local in let flags = cc_flags () in let hash = Digest.(to_hex @@ file (EP.resolve_file ~elpi ~unit:x ())) in try diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 6c7c27d36..3a63fc9a4 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -43,10 +43,16 @@ let feedback_fmt_write, feedback_fmt_flush = Feedback.msg_notice Pp.(str s); Buffer.clear b) +let elpi_cat = CWarnings.create_category ~name:"elpi" () +let elpi_depr_cat = + CWarnings.create_category + ~from:[elpi_cat;CWarnings.CoreCategories.deprecated] + ~name:"elpi.deprecated" () + let () = API.Setup.set_error (fun ?loc s -> err ?loc Pp.(str s)) let () = API.Setup.set_anomaly (fun ?loc s -> err ?loc Pp.(str s)) let () = API.Setup.set_type_error (fun ?loc s -> err ?loc Pp.(str s)) -let warn = CWarnings.create ~name:"runtime" ~category:"elpi" Pp.str +let warn = CWarnings.create ~name:"runtime" ~category:elpi_cat Pp.str let () = API.Setup.set_warn (fun ?loc x -> warn ?loc:(Option.map to_coq_loc loc) x) let () = API.Setup.set_std_formatter (Format.make_formatter feedback_fmt_write feedback_fmt_flush) let () = API.Setup.set_err_formatter (Format.make_formatter feedback_fmt_write feedback_fmt_flush) @@ -71,7 +77,7 @@ let safe_destApp sigma t = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None)) + (Glob_term.GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous)) let mkApp ~depth t l = match l with @@ -223,11 +229,11 @@ let detype ?(keepunivs=false) env sigma t = if keepunivs then Flags.with_option Constrextern.print_universes else Flags.without_option Constrextern.print_universes in let gbody = - options (Detyping.detype Detyping.Now false Names.Id.Set.empty env sigma) t in + options (Detyping.detype Detyping.Now Names.Id.Set.empty env sigma) t in fix_detype gbody let detype_closed_glob env sigma closure = - let gbody = Detyping.detype_closed_glob false Names.Id.Set.empty env sigma closure in + let gbody = Detyping.detype_closed_glob Names.Id.Set.empty env sigma closure in fix_detype gbody type qualified_name = string list diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index 0bdf758db..f2bd1e5dd 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -6,6 +6,9 @@ val to_coq_loc : Elpi.API.Ast.Loc.t -> Loc.t val of_coq_loc : Loc.t -> Elpi.API.Ast.Loc.t +val elpi_cat : CWarnings.category +val elpi_depr_cat : CWarnings.category + val err : ?loc:Elpi.API.Ast.Loc.t -> Pp.t -> 'a exception LtacFail of int * Pp.t val ltac_fail_err : ?loc:Elpi.API.Ast.Loc.t -> int -> Pp.t -> 'a diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 1ff5d7f7f..6fb16636c 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -55,33 +55,30 @@ let bound_steps n = (* Units are marshalable, but programs are not *) -let compiler_cache_code = Summary.Local.ref +let compiler_cache_code = Summary.ref ~local:true ~name:"elpi-compiler-cache-code" Int.Map.empty -let compiler_cache_chunk = Summary.Local.ref +let compiler_cache_chunk = Summary.ref ~local:true ~name:"elpi-compiler-cache-chunk" Int.Map.empty -let programs_tip = Summary.Local.ref +let programs_tip = Summary.ref ~local:true ~name:"elpi-compiler-cache-gc" SLMap.empty (* lookup/cache for hash h shifted over base b *) let lookup b h src r cmp = - let open Summary.Local in let h = combine_hash b h in let p, src' = Int.Map.find h !r in if cmp src src' then p else assert false let cache b h prog src r = - let open Summary.Local in let h = combine_hash b h in r := Int.Map.add h (prog,src) !r; prog let uncache b h r = - let open Summary.Local in let h = combine_hash b h in r := Int.Map.remove h !r @@ -100,7 +97,6 @@ let recache_chunk b h1 h2 p src = cache_chunk b h2 p src let get_and_compile name = - let open Summary.Local in let src = code name in let prog = let rec compile_code src = @@ -282,7 +278,7 @@ let run_program loc name ~atts args = let env = Global.env () in let sigma = Evd.from_env env in let args = args - |> List.map (Coq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign env)) + |> List.map (Coq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign ~strict:true env)) |> List.map (Coq_elpi_arg_HOAS.Cmd.interp (Ltac_plugin.Tacinterp.default_ist ()) env sigma) in let query ~depth state = @@ -448,27 +444,31 @@ let loc_merge l1 l2 = let cache_program (nature,p,p_str) = match nature with | Command _ -> - Vernacextend.vernac_extend - ~command:("Elpi"^p_str) - ~classifier:(fun _ -> Vernacextend.(VtSideff ([], VtNow))) - ?entry:None - [ Vernacextend.TyML - (false, - Vernacextend.TyNonTerminal - (Extend.TUentry - (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), - Vernacextend.TyTerminal - (p_str, - Vernacextend.TyNonTerminal - (Extend.TUlist0 - (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_cmd_arg)) - ,Vernacextend.TyNonTerminal - (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), - Vernacextend.TyNil)))), - (fun loc0 args loc1 ?loc ~atts () -> Vernacextend.vtdefault (fun () -> - run_program (Option.default (loc_merge loc0 loc1) loc) p ~atts args)), - None) - ] + let ext = + Vernacextend.declare_dynamic_vernac_extend + ~command:("Elpi"^p_str) + ?entry:None + ~depr:false + + (fun _loc0 _args _loc1 -> (Vernacextend.VtSideff ([], VtNow))) + + (Vernacextend.TyNonTerminal + (Extend.TUentry + (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), + Vernacextend.TyTerminal + (p_str, + Vernacextend.TyNonTerminal + (Extend.TUlist0 + (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_cmd_arg)) + ,Vernacextend.TyNonTerminal + (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), + Vernacextend.TyNil))))) + + (fun loc0 args loc1 ?loc ~atts () -> Vernacextend.vtdefault (fun () -> + run_program (Option.default (loc_merge loc0 loc1) loc) p ~atts args)) + in + Egramml.extend_vernac_command_grammar ~undoable:true ext + | Tactic -> Coq_elpi_builtins.cache_tac_abbrev p | Program _ -> @@ -500,5 +500,3 @@ let skip ~atts:(skip,only) f x = | Some _, Some _ -> CErrors.user_err Pp.(str "Attributes #[skip] and #[only] cannot be used at the same time") in if exec then f x else () - - diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index bfd44adad..ac3ca1eef 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -44,3 +44,18 @@ val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Ge val export_command : qualified_name -> unit +val atts2impl : + Elpi.API.Ast.Loc.t -> depth:int -> Elpi.API.State.t -> Attributes.vernac_flags -> + Elpi.API.Data.term -> Elpi.API.State.t * Elpi.API.Data.term +val get_and_compile : + qualified_name -> Elpi.API.Compile.program * bool +val run : static_check:bool -> + Elpi.API.Compile.program -> + [ `Ast of Elpi.API.Ast.query + | `Fun of + depth:int -> + Elpi.API.State.t -> + Elpi.API.State.t * + (Elpi.API.Ast.Loc.t * Elpi.API.Data.term) * + Elpi.API.Conversion.extra_goals ] -> + unit Elpi.API.Execute.outcome \ No newline at end of file diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 748c54eca..a81d1a39a 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -50,12 +50,14 @@ let rec inlogpath q = function | [] -> [] | x :: xs -> ("coq://" ^ Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs -let warning_legacy_accumulate = - CWarnings.create ~name:"elpi.accumulate-syntax" ~category:"elpi.deprecated" (fun () -> - Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'") -let warning_legacy_accumulate2 = - CWarnings.create ~name:"elpi.accumulate-syntax" ~category:"elpi.deprecated" (fun () -> - Pp.strbrk "The syntax 'Elpi Accumulate File \"path\" From logpath' is deprecated, use 'From logpath Extra Dependency \"path\" as name. Elpi Accumulate File name.'") +let warning_legacy_accumulate_gen = + CWarnings.create ~name:"elpi.accumulate-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun has_from -> + if has_from then + Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'" + else Pp.strbrk "The syntax 'Elpi Accumulate File \"path\" From logpath' is deprecated, use 'From logpath Extra Dependency \"path\" as name. Elpi Accumulate File name.'") + +let warning_legacy_accumulate ?loc () = warning_legacy_accumulate_gen ?loc true +let warning_legacy_accumulate2 ?loc () = warning_legacy_accumulate_gen ?loc false } GRAMMAR EXTEND Gram @@ -71,7 +73,7 @@ GRAMMAR EXTEND Gram then Genarg.in_gen (Genarg.rawwit wit_elpi_code) (strip_curly loc s) else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Coq_elpi_utils.of_coq_loc loc,s) in CAst.make ~loc - (Constrexpr.CHole (None, Namegen.IntroAnonymous, Some arg)) } ] + (Constrexpr.CGenarg arg) } ] ] ; END @@ -206,7 +208,6 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF | #[ atts = any_attribute ] [ "Elpi" "Template" "Tactic" string(s) ] -> { let () = ignore_unknown_attributes atts in EV.load_tactic s } - END VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([], VtNow)) } diff --git a/tests/test_API_TC_CS.v b/tests/test_API_TC_CS.v index 8fda5598f..ac45723e2 100644 --- a/tests/test_API_TC_CS.v +++ b/tests/test_API_TC_CS.v @@ -112,8 +112,8 @@ Elpi Query lp:{{coq.coercion.db L}}. Axiom C3 : nat -> Type. Axiom nuc : forall x, C1 -> C3 x. -Set Warnings "+uniform-inheritance". -Elpi Query lp:{{ @nonuniform! => @reversible! => coq.coercion.declare (coercion {coq.locate "nuc"} _ _ _) }}. +Set Warnings "-uniform-inheritance". +Elpi Query lp:{{ @reversible! => coq.coercion.declare (coercion {coq.locate "nuc"} _ _ _) }}. About nuc. diff --git a/tests/test_API_env.v b/tests/test_API_env.v index b07c046b6..341b55fee 100644 --- a/tests/test_API_env.v +++ b/tests/test_API_env.v @@ -281,7 +281,7 @@ Elpi Query lp:{{ }}. -#[nonuniform] Coercion f2 : r1 >-> eq. +#[warning="-uniform-inheritance"] Coercion f2 : r1 >-> eq. Elpi Query lp:{{