diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index a2b712ab8..30c0c0421 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -189,6 +189,7 @@ jobs: coq-elpi: needs: - coq + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -248,6 +249,64 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "coq-elpi" + coq-elpi-tests: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-tests) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-8.20\" --argstr job \"coq-elpi-tests\" \\\n --dry-run 2> err > out + || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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.20" + --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.20" + --argstr job "coq-elpi-tests" coqeal: needs: - coq @@ -535,6 +594,7 @@ jobs: mathcomp: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -632,6 +692,7 @@ jobs: mathcomp-algebra: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -923,6 +984,7 @@ jobs: mathcomp-character: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1161,6 +1223,7 @@ jobs: mathcomp-field: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1248,6 +1311,7 @@ jobs: mathcomp-fingroup: needs: - coq + - stdlib - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -1607,6 +1671,7 @@ jobs: mathcomp-solvable: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1689,6 +1754,7 @@ jobs: mathcomp-ssreflect: needs: - coq + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1996,6 +2062,64 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "relation-algebra" + stdlib: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-8.20\" --argstr job \"stdlib\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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.20" + --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.20" + --argstr job "stdlib" name: Nix CI for bundle coq-8.20 on: pull_request: diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-coq-master.yml index 5c15de372..36dd607d1 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.github/workflows/nix-action-coq-master.yml @@ -178,6 +178,185 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "coq-elpi" + coq-elpi-no-stdlib: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-no-stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-master\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err + > out || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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-master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" + --argstr job "coq-elpi-no-stdlib" + coq-elpi-tests: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-tests) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-master\" --argstr job \"coq-elpi-tests\" \\\n --dry-run 2> err > out + || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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-master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" + --argstr job "coq-elpi-tests" + coq-elpi-tests-stdlib: + needs: + - coq + - stdlib + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-tests-stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-master\" --argstr job \"coq-elpi-tests-stdlib\" \\\n --dry-run 2> + err > out || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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-master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" + --argstr job "stdlib" + - 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-master" + --argstr job "coq-elpi-tests-stdlib" coqeal: needs: - coq diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index e8806b78f..d3a25c9c8 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -189,6 +189,7 @@ jobs: coq-elpi: needs: - coq + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -248,6 +249,185 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "coq-elpi" + coq-elpi-no-stdlib: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-no-stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err > + out || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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 "rocq-9.0" + --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 "rocq-9.0" + --argstr job "coq-elpi-no-stdlib" + coq-elpi-tests: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-tests) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"coq-elpi-tests\" \\\n --dry-run 2> err > out + || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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 "rocq-9.0" + --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 "rocq-9.0" + --argstr job "coq-elpi-tests" + coq-elpi-tests-stdlib: + needs: + - coq + - stdlib + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi-tests-stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"coq-elpi-tests-stdlib\" \\\n --dry-run 2> err + > out || (touch fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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 "rocq-9.0" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "coq-elpi-tests-stdlib" coqeal: needs: - coq @@ -391,6 +571,7 @@ jobs: mathcomp: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -488,6 +669,7 @@ jobs: mathcomp-algebra: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -779,6 +961,7 @@ jobs: mathcomp-character: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1017,6 +1200,7 @@ jobs: mathcomp-field: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1104,6 +1288,7 @@ jobs: mathcomp-fingroup: needs: - coq + - stdlib - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -1463,6 +1648,7 @@ jobs: mathcomp-solvable: needs: - coq + - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1545,6 +1731,7 @@ jobs: mathcomp-ssreflect: needs: - coq + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1785,6 +1972,64 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "odd-order" + stdlib: + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (stdlib) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"stdlib\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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 "rocq-9.0" + --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 "rocq-9.0" + --argstr job "stdlib" name: Nix CI for bundle rocq-9.0 on: pull_request: diff --git a/.gitignore b/.gitignore index df9c20014..29784562d 100644 --- a/.gitignore +++ b/.gitignore @@ -55,4 +55,6 @@ _build tmp.out coq-elpi-tests.opam coq-elpi-tests.install -coq-elpi.install \ No newline at end of file +coq-elpi.install + +theories-stdlib/dune \ No newline at end of file diff --git a/.nix/config.nix b/.nix/config.nix index 38e340572..a4dbcc43e 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -14,6 +14,11 @@ let master = [ common-bundles = listToAttrs (forEach master (p: { name = p; value.override.version = "master"; })) // { + coq-elpi-no-stdlib.job = true; + coq-elpi-tests.job = true; + stdlib.job = true; + coq-elpi-tests-stdlib.job = true; + mathcomp-single-planB-src.job = false; mathcomp-single-planB.job = false; mathcomp-single.job = false; @@ -30,6 +35,8 @@ let master = [ "coq-8.20".coqPackages = common-bundles // { coq.override.version = "8.20"; coq-elpi.override.elpi-version = "2.0.7"; + coq-elpi-no-stdlib.job = false; + coq-elpi-tests-stdlib.job = false; }; "rocq-9.0".coqPackages = common-bundles // { @@ -49,6 +56,7 @@ let master = [ coq.override.version = "master"; coq-elpi.override.elpi-version = "2.0.7"; stdlib.override.version = "master"; + bignums.override.version = "master"; }; */ }; diff --git a/.nix/coq-overlays/coq-elpi-no-stdlib/default.nix b/.nix/coq-overlays/coq-elpi-no-stdlib/default.nix new file mode 100644 index 000000000..001239b6b --- /dev/null +++ b/.nix/coq-overlays/coq-elpi-no-stdlib/default.nix @@ -0,0 +1,11 @@ +{ lib, coq-elpi, coqPackages }: + +coqPackages.lib.overrideCoqDerivation { + + pname = "coq-elpi-no-stdlib"; + opam-name = "coq-elpi"; + + propagatedBuildInputs = + lib.filter (d: d?pname && d.pname != "stdlib") + coq-elpi.propagatedBuildInputs; +} coq-elpi diff --git a/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix b/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix new file mode 100644 index 000000000..c23648568 --- /dev/null +++ b/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix @@ -0,0 +1,15 @@ +{ coq-elpi, coqPackages }: + +coqPackages.lib.overrideCoqDerivation { + + pname = "coq-elpi-tests-stdlib"; + + buildPhase = '' + make test-stdlib + make examples-stdlib + make test-apps-stdlib + ''; + installPhase = '' + echo "nothing to install" + ''; +} coq-elpi diff --git a/.nix/coq-overlays/coq-elpi-tests/default.nix b/.nix/coq-overlays/coq-elpi-tests/default.nix new file mode 100644 index 000000000..b261deb07 --- /dev/null +++ b/.nix/coq-overlays/coq-elpi-tests/default.nix @@ -0,0 +1,19 @@ +{ lib, coq-elpi, coqPackages }: + +coqPackages.lib.overrideCoqDerivation { + + pname = "coq-elpi-tests"; + + propagatedBuildInputs = + lib.filter (d: d?pname && d.pname != "stdlib") + coq-elpi.propagatedBuildInputs; + + buildPhase = '' + make test-core + make examples + make test-apps + ''; + installPhase = '' + echo "nothing to install" + ''; +} coq-elpi diff --git a/Makefile b/Makefile index a9631c171..e8ccca073 100644 --- a/Makefile +++ b/Makefile @@ -1,53 +1,65 @@ dune = dune $(1) $(DUNE_$(1)_FLAGS) -elpi/dune: elpi/dune.in - @rm -f $@ - @echo "; generated by make, do not edit" > $@ - @if $$(coqc --version | grep -q "8.19\|8.20") ; then \ - sed -e 's/@@STDLIB_THEORY@@//' $< >> $@ ; \ - else \ - sed -e 's/@@STDLIB_THEORY@@/(theories Stdlib)/' $< >> $@ ; \ - fi - @chmod a-w $@ - -all: elpi/dune +all: theories-stdlib/dune $(call dune,build) $(call dune,build) builtin-doc .PHONY: all -build-core: elpi/dune +build-core: theories-stdlib/dune $(call dune,build) theories $(call dune,build) builtin-doc .PHONY: build-core -build-apps: elpi/dune +build-apps: theories-stdlib/dune $(call dune,build) $$(find apps -type d -name theories) .PHONY: build-apps -build: elpi/dune +build: theories-stdlib/dune $(call dune,build) -p coq-elpi @install $(call dune,build) builtin-doc .PHONY: build -test-core: elpi/dune +all-tests: test-core test-stdlib test-apps test-apps-stdlib +.PHONY: all-tests + +test-core: theories-stdlib/dune $(call dune,runtest) tests $(call dune,build) tests .PHONY: test-core -test-apps: elpi/dune +test-apps: theories-stdlib/dune $(call dune,build) $$(find apps -type d -name tests) .PHONY: test-apps -test: elpi/dune - $(call dune,runtest) - $(call dune,build) tests - $(call dune,build) $$(find apps -type d -name tests) -.PHONY: test +test-apps-stdlib: theories-stdlib/dune + $(call dune,build) $$(find apps -type d -name tests-stdlib) +.PHONY: test-apps-stdlib -examples: elpi/dune +test-stdlib: theories-stdlib/dune + $(call dune,build) tests-stdlib +.PHONY: test-stdlib + +all-examples: examples examples-stdlib +.PHONY: all-examples + +examples: theories-stdlib/dune $(call dune,build) examples .PHONY: examples +examples-stdlib: theories-stdlib/dune + $(call dune,build) examples-stdlib +.PHONY: examples-stdlib + +theories-stdlib/dune: theories-stdlib/dune.in + @rm -f $@ + @echo "; generated by make, do not edit" > $@ + @if $$(coqc --version | grep -q "8.19\|8.20") ; then \ + sed -e 's/@@STDLIB@@//' $< >> $@ ; \ + else \ + sed -e 's/@@STDLIB@@/Stdlib/' $< >> $@ ; \ + fi + @chmod a-w $@ + doc: build @echo "########################## generating doc ##########################" @mkdir -p doc @@ -66,7 +78,7 @@ clean: $(call dune,clean) .PHONY: clean -install: elpi/dune +install: $(call dune,install) coq-elpi .PHONY: install diff --git a/apps/NES/elpi/dune b/apps/NES/elpi/dune index ff3aa20ed..d5b54bc98 100644 --- a/apps/NES/elpi/dune +++ b/apps/NES/elpi/dune @@ -10,9 +10,7 @@ (action (with-stdout-to %{target} (progn - (echo "Require Import String.\nOpen Scope string_scope.\nLocal Definition _hash := \"\n") - (run coq_elpi_shafile %{deps}) - (echo "\".\n"))))) + (run coq_elpi_shafile %{deps}))))) (install (files diff --git a/apps/coercion/tests/test.v b/apps/coercion/tests/test.v index 01d8a0088..080e25f86 100644 --- a/apps/coercion/tests/test.v +++ b/apps/coercion/tests/test.v @@ -1,6 +1,5 @@ From elpi.apps Require Import coercion. #[warning="-deprecated-from-Coq"] -From Coq Require Import Bool. Elpi Accumulate coercion.db lp:{{ @@ -9,7 +8,7 @@ coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}. }}. -Check True && False. +Check andb True False. Parameter ringType : Type. Parameter ringType_sort : ringType -> Type. diff --git a/apps/coercion/tests/test_open.v b/apps/coercion/tests/test_open.v index 109b264f6..3c391ca04 100644 --- a/apps/coercion/tests/test_open.v +++ b/apps/coercion/tests/test_open.v @@ -1,8 +1,7 @@ From elpi.apps Require Import coercion. -#[warning="-deprecated-from-Coq"] -From Coq Require Import Arith ssreflect. +From elpi.core Require Import ssreflect. -Ltac my_solver := trivial with arith. +Ltac my_solver := try ((repeat apply: le_n_S); apply: le_0_n). Elpi Accumulate coercion lp:{{ diff --git a/apps/derive/elpi/dune b/apps/derive/elpi/dune index 1483b7fbc..02f0525dd 100644 --- a/apps/derive/elpi/dune +++ b/apps/derive/elpi/dune @@ -10,9 +10,7 @@ (action (with-stdout-to %{target} (progn - (echo "Require Import String.\nOpen Scope string_scope.\nLocal Definition _hash := \"\n") - (run coq_elpi_shafile %{deps}) - (echo "\".\n"))))) + (run coq_elpi_shafile %{deps}))))) (install (files diff --git a/apps/derive/elpi/eqbOK.elpi b/apps/derive/elpi/eqbOK.elpi index 8b9d4c512..1d1cd089d 100644 --- a/apps/derive/elpi/eqbOK.elpi +++ b/apps/derive/elpi/eqbOK.elpi @@ -15,7 +15,7 @@ add-reflect (type-param F) Correct Refl {{ fun (a : lp:Type) (eqA: a -> a -> bool) (heqA : lp:(HeqA a eqA)) => lp:(R a eqA heqA) }} :- Type = sort (typ {coq.univ.new}), - HeqA = (a\eqA\ {{ forall x1 x2 : lp:a, reflect (@eq lp:a x1 x2) (lp:eqA x1 x2) }}), + HeqA = (a\eqA\ {{ forall x1 x2 : lp:a, lib:elpi.reflect (@eq lp:a x1 x2) (lp:eqA x1 x2) }}), @pi-trm `a` Type aa\a\ @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\ @pi-decl `heqA` (HeqA a eqA) heqA\ @@ -56,7 +56,7 @@ main (const C) Prefix [CL] :- std.do! [ std.assert-ok! (coq.typecheck Breflect _) "eqbOK generates illtyped term", coq.ensure-fresh-global-id (Prefix ^ "eqb_OK") Namerf, X = (global (const C) : term), - coq.env.add-const Namerf Breflect {{ forall a b : lp:X, Bool.reflect (@eq lp:X a b) (lp:F a b) }} @opaque! Reflect, + coq.env.add-const Namerf Breflect {{ forall a b : lp:X, lib:elpi.reflect (@eq lp:X a b) (lp:F a b) }} @opaque! Reflect, CL = eqbok-for (const C) Reflect, coq.elpi.accumulate _ "derive.eqbOK.db" (clause _ _ CL), ]. diff --git a/apps/derive/elpi/tag.elpi b/apps/derive/elpi/tag.elpi index 63145f1b4..cda7d535e 100644 --- a/apps/derive/elpi/tag.elpi +++ b/apps/derive/elpi/tag.elpi @@ -52,7 +52,7 @@ do-dummy-branch _ _ _ _ {{ Prop }}. % dummy % [do-branch InTerm Acc NewTem NewAcc] descends into a branch and puts Acc % in place of the dummy pred do-branch i:term, i:term, o:term, o:term. -do-branch {{ Prop }} X X Y :- coq.reduction.lazy.norm {{ lp:X + 1 }} Y. +do-branch {{ Prop }} X X Y :- coq.reduction.lazy.norm {{ Pos.add lp:X 1 }} Y. do-branch (fun N T F) X (fun N T R) Y :- @pi-decl N T x\ do-branch (F x) X (R x) Y. diff --git a/apps/derive/examples/usage.v b/apps/derive/examples/usage.v index 42ec0bad8..629ad36b0 100644 --- a/apps/derive/examples/usage.v +++ b/apps/derive/examples/usage.v @@ -2,7 +2,6 @@ This example shows how to use derive *) -From Coq Require Import Bool. From elpi.apps Require Import derive.std. Set Uniform Inductive Parameters. diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune new file mode 100644 index 000000000..2411d4773 --- /dev/null +++ b/apps/derive/tests-stdlib/dune @@ -0,0 +1,7 @@ +(coq.theory + (package coq-elpi-tests-stdlib) + (name elpi_apps_derive_tests_stdlib) + (flags :standard -w -default-output-directory) + (theories elpi elpi.apps.derive elpi.apps.derive.tests elpi_stdlib)) + +(include_subdirs qualified) diff --git a/apps/derive/tests/test_derive.v b/apps/derive/tests-stdlib/test_derive.v similarity index 98% rename from apps/derive/tests/test_derive.v rename to apps/derive/tests-stdlib/test_derive.v index 10b96b1fb..a4071e9d8 100644 --- a/apps/derive/tests/test_derive.v +++ b/apps/derive/tests-stdlib/test_derive.v @@ -1,5 +1,5 @@ From elpi.apps Require Import derive.std derive.legacy derive.experimental. -From elpi.apps Require Import test_derive_stdlib. +From elpi.apps Require Import test_derive_corelib. Elpi derive Coverage.empty. Elpi derive Coverage.unit. @@ -170,7 +170,3 @@ End derive_container. About wimpls.wimpls. About wimpls.Kwi. Redirect "tmp" Check Kwi _ (refl_equal 3). - -From Coq Require Ascii. - -#[only(param2)] derive Ascii.ascii. diff --git a/apps/derive/tests/test_bcongr.v b/apps/derive/tests/test_bcongr.v index 8c21c1ad1..8d056cbd4 100644 --- a/apps/derive/tests/test_bcongr.v +++ b/apps/derive/tests/test_bcongr.v @@ -1,8 +1,9 @@ +From elpi.core Require Import Bool. From elpi.apps Require Import derive.bcongr. -From elpi.apps Require Import test_derive_stdlib test_projK. +From elpi.apps Require Import test_derive_corelib test_projK. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import test_projK.Coverage. Module Coverage. diff --git a/apps/derive/tests/test_derive_stdlib.v b/apps/derive/tests/test_derive_corelib.v similarity index 98% rename from apps/derive/tests/test_derive_stdlib.v rename to apps/derive/tests/test_derive_corelib.v index e532f62bb..98c2406fc 100644 --- a/apps/derive/tests/test_derive_stdlib.v +++ b/apps/derive/tests/test_derive_corelib.v @@ -1,6 +1,6 @@ (* Some standard data types using different features *) -From Coq Require Uint63. -From Coq Require Floats. +From elpi.core Require PrimInt63. +From elpi.core Require PrimFloat. Module Coverage. @@ -68,7 +68,7 @@ Inductive large := | K25(_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) | K26(_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit). -Inductive prim_int := PI (i : Uint63.int). +Inductive prim_int := PI (i : PrimInt63.int). Inductive prim_float := PF (f : PrimFloat.float). Record fo_record := { f1 : peano; f2 : unit; }. diff --git a/apps/derive/tests/test_derive_vector.v.skip b/apps/derive/tests/test_derive_vector.v.skip index 2236dce60..616258fd6 100644 --- a/apps/derive/tests/test_derive_vector.v.skip +++ b/apps/derive/tests/test_derive_vector.v.skip @@ -1,6 +1,6 @@ From elpi.apps Require Import derive derive.projK. -From elpi.apps Require Import test_derive_stdlib. +From elpi.apps Require Import test_derive_corelib. Elpi derive.projK Coverage.vect. diff --git a/apps/derive/tests/test_eq.v b/apps/derive/tests/test_eq.v index 931523ac6..87737912a 100644 --- a/apps/derive/tests/test_eq.v +++ b/apps/derive/tests/test_eq.v @@ -1,6 +1,6 @@ -From elpi.apps Require Import test_derive_stdlib derive.eq. +From elpi.apps Require Import test_derive_corelib derive.eq. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Module Coverage. Elpi derive.eq empty. diff --git a/apps/derive/tests/test_eqK.v b/apps/derive/tests/test_eqK.v index e37551f4b..90f0c25f0 100644 --- a/apps/derive/tests/test_eqK.v +++ b/apps/derive/tests/test_eqK.v @@ -2,13 +2,13 @@ From elpi Require Import elpi. From elpi.apps Require Import derive.eqK. From elpi.apps.derive.tests Require Import - test_derive_stdlib + test_derive_corelib test_isK test_projK test_bcongr test_eq. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import test_isK.Coverage. Import test_projK.Coverage. Import test_bcongr.Coverage. diff --git a/apps/derive/tests/test_eqOK.v b/apps/derive/tests/test_eqOK.v index 48918e20f..f07711e2e 100644 --- a/apps/derive/tests/test_eqOK.v +++ b/apps/derive/tests/test_eqOK.v @@ -1,8 +1,8 @@ From elpi.apps Require Import derive.eqOK. -From elpi.apps Require Import test_derive_stdlib test_eqcorrect test_param1 test_param1_trivial. +From elpi.apps Require Import test_derive_corelib test_eqcorrect test_param1 test_param1_trivial. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import tests.test_eq.Coverage. Import test_eqcorrect.Coverage. Import test_param1.Coverage. diff --git a/apps/derive/tests/test_eqType_ast.v b/apps/derive/tests/test_eqType_ast.v index 37c4e1888..ae2c8d282 100644 --- a/apps/derive/tests/test_eqType_ast.v +++ b/apps/derive/tests/test_eqType_ast.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.eqType_ast. -From elpi.apps.derive.tests Require Import test_derive_stdlib. -Import test_derive_stdlib.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib. +Import test_derive_corelib.Coverage. Module Coverage. Elpi derive.eqType.ast empty. diff --git a/apps/derive/tests/test_eqb.v b/apps/derive/tests/test_eqb.v index 3eff38e6a..09095d2e5 100644 --- a/apps/derive/tests/test_eqb.v +++ b/apps/derive/tests/test_eqb.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.eqb. -From elpi.apps.derive.tests Require Import test_derive_stdlib test_eqType_ast test_tag test_fields. -Import test_derive_stdlib.Coverage test_eqType_ast.Coverage test_tag.Coverage test_fields.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib test_eqType_ast test_tag test_fields. +Import test_derive_corelib.Coverage test_eqType_ast.Coverage test_tag.Coverage test_fields.Coverage. Module Coverage. Elpi derive.eqb empty. @@ -41,7 +41,7 @@ Elpi derive.eqb alias. End Coverage. Import Coverage. -Import PArith. +From elpi.core Require Import PosDef. Notation eq_test T := (T -> T -> bool). Notation eq_test2 T1 T2 := (T1 -> T2 -> bool). diff --git a/apps/derive/tests/test_eqbOK.v b/apps/derive/tests/test_eqbOK.v index ca74704fe..1db6f062b 100644 --- a/apps/derive/tests/test_eqbOK.v +++ b/apps/derive/tests/test_eqbOK.v @@ -1,8 +1,9 @@ +From elpi.core Require Import Bool. From elpi.apps Require Import derive.eqbOK. -From elpi.apps.derive.tests Require Import test_derive_stdlib test_eqb test_eqbcorrect. +From elpi.apps.derive.tests Require Import test_derive_corelib test_eqb test_eqbcorrect. -Import test_derive_stdlib.Coverage +Import test_derive_corelib.Coverage test_eqType_ast.Coverage test_eqb.Coverage test_eqbcorrect.Coverage. @@ -48,7 +49,7 @@ End Coverage. Import Coverage. -Redirect "tmp" Check peano_eqb_OK : forall n m, Bool.reflect (n = m) (peano_eqb n m). -Redirect "tmp" Check seq_eqb_OK : forall A eqA (h : forall a1 a2 : A, Bool.reflect (a1 = a2) (eqA a1 a2)) l1 l2, Bool.reflect (l1 = l2) (seq_eqb A eqA l1 l2). -Redirect "tmp" Check ord_eqb_OK : forall n (o1 o2 : ord n), Bool.reflect (o1 = o2) (ord_eqb n n o1 o2). -Redirect "tmp" Check alias_eqb_OK : forall x y : alias, Bool.reflect (x = y) (alias_eqb x y). +Redirect "tmp" Check peano_eqb_OK : forall n m, Datatypes.reflect (n = m) (peano_eqb n m). +Redirect "tmp" Check seq_eqb_OK : forall A eqA (h : forall a1 a2 : A, Datatypes.reflect (a1 = a2) (eqA a1 a2)) l1 l2, Datatypes.reflect (l1 = l2) (seq_eqb A eqA l1 l2). +Redirect "tmp" Check ord_eqb_OK : forall n (o1 o2 : ord n), Datatypes.reflect (o1 = o2) (ord_eqb n n o1 o2). +Redirect "tmp" Check alias_eqb_OK : forall x y : alias, Datatypes.reflect (x = y) (alias_eqb x y). diff --git a/apps/derive/tests/test_eqbcorrect.v b/apps/derive/tests/test_eqbcorrect.v index 80550217c..fabb3a5b8 100644 --- a/apps/derive/tests/test_eqbcorrect.v +++ b/apps/derive/tests/test_eqbcorrect.v @@ -1,8 +1,8 @@ From elpi.apps Require Import derive.eqbcorrect. From elpi.apps.derive Require Import param1. (* FIXME, the clause is in param1 *) -From elpi.apps.derive.tests Require Import test_derive_stdlib test_eqType_ast test_tag test_fields test_eqb test_induction +From elpi.apps.derive.tests Require Import test_derive_corelib test_eqType_ast test_tag test_fields test_eqb test_induction test_param1 test_param1_trivial test_param1_functor. -Import test_derive_stdlib.Coverage +Import test_derive_corelib.Coverage test_eqType_ast.Coverage test_tag.Coverage test_fields.Coverage diff --git a/apps/derive/tests/test_eqcorrect.v b/apps/derive/tests/test_eqcorrect.v index ddd393cab..195526058 100644 --- a/apps/derive/tests/test_eqcorrect.v +++ b/apps/derive/tests/test_eqcorrect.v @@ -1,8 +1,8 @@ From elpi.apps Require Import derive.eqcorrect. -From elpi.apps Require Import test_derive_stdlib derive.tests.test_eq test_param1 test_param1_functor test_induction test_eqK. +From elpi.apps Require Import test_derive_corelib derive.tests.test_eq test_param1 test_param1_functor test_induction test_eqK. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import tests.test_eq.Coverage. Import test_param1.Coverage. Import test_param1_functor.Coverage. diff --git a/apps/derive/tests/test_fields.v b/apps/derive/tests/test_fields.v index ce174f992..1ce2e1c95 100644 --- a/apps/derive/tests/test_fields.v +++ b/apps/derive/tests/test_fields.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.fields. -From elpi.apps.derive.tests Require Import test_derive_stdlib test_eqType_ast test_tag. -Import test_derive_stdlib.Coverage test_eqType_ast.Coverage test_tag.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib test_eqType_ast test_tag. +Import test_derive_corelib.Coverage test_eqType_ast.Coverage test_tag.Coverage. Module Coverage. Elpi derive.fields empty. @@ -38,7 +38,7 @@ Elpi derive.fields val. End Coverage. Import Coverage. -Import PArith. +From elpi.core Require Import PosDef. Redirect "tmp" Check empty_fields_t : positive -> Type. Redirect "tmp" Check empty_fields : forall (n:empty), empty_fields_t (empty_tag n). diff --git a/apps/derive/tests/test_induction.v b/apps/derive/tests/test_induction.v index 5b73fc7bf..1f8f7716a 100644 --- a/apps/derive/tests/test_induction.v +++ b/apps/derive/tests/test_induction.v @@ -1,8 +1,8 @@ From elpi.apps Require Import derive.induction. -From elpi.apps Require Import test_derive_stdlib test_param1 test_param1_functor. +From elpi.apps Require Import test_derive_corelib test_param1 test_param1_functor. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import derive.param1. (* for is_eq *) Import test_param1.Coverage. Import test_param1_functor.Coverage. diff --git a/apps/derive/tests/test_isK.v b/apps/derive/tests/test_isK.v index 84033bcdd..fa4c8519a 100644 --- a/apps/derive/tests/test_isK.v +++ b/apps/derive/tests/test_isK.v @@ -1,6 +1,6 @@ -From elpi.apps Require Import test_derive_stdlib derive.isK. +From elpi.apps Require Import test_derive_corelib derive.isK. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. (* coverage *) Module Coverage. diff --git a/apps/derive/tests/test_lens.v b/apps/derive/tests/test_lens.v index 8467dd116..f59cae3b5 100644 --- a/apps/derive/tests/test_lens.v +++ b/apps/derive/tests/test_lens.v @@ -1,6 +1,6 @@ -From elpi.apps Require Import test_derive_stdlib derive.lens. +From elpi.apps Require Import test_derive_corelib derive.lens. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. (* coverage *) Module Coverage. diff --git a/apps/derive/tests/test_lens_laws.v b/apps/derive/tests/test_lens_laws.v index bbf841fdb..a2b251fe6 100644 --- a/apps/derive/tests/test_lens_laws.v +++ b/apps/derive/tests/test_lens_laws.v @@ -1,9 +1,9 @@ From elpi.apps Require Import derive.lens_laws. -From elpi.apps Require Import test_derive_stdlib test_lens. +From elpi.apps Require Import test_derive_corelib test_lens. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import test_lens.Coverage. (* coverage *) diff --git a/apps/derive/tests/test_map.v b/apps/derive/tests/test_map.v index 93c3be993..e056747f8 100644 --- a/apps/derive/tests/test_map.v +++ b/apps/derive/tests/test_map.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.map. -From elpi.apps.derive.tests Require Import test_derive_stdlib. -Import test_derive_stdlib.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib. +Import test_derive_corelib.Coverage. Module Coverage. diff --git a/apps/derive/tests/test_param1.v b/apps/derive/tests/test_param1.v index 66fae5c8f..d38412db2 100644 --- a/apps/derive/tests/test_param1.v +++ b/apps/derive/tests/test_param1.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.param1. -From elpi.apps.derive.tests Require Import test_derive_stdlib. -Import test_derive_stdlib.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib. +Import test_derive_corelib.Coverage. Module Coverage. diff --git a/apps/derive/tests/test_param1_congr.v b/apps/derive/tests/test_param1_congr.v index 73afec06a..61a02b6f6 100644 --- a/apps/derive/tests/test_param1_congr.v +++ b/apps/derive/tests/test_param1_congr.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.param1_congr. -From elpi.apps Require Import test_derive_stdlib test_param1. -Import test_derive_stdlib.Coverage. +From elpi.apps Require Import test_derive_corelib test_param1. +Import test_derive_corelib.Coverage. Import test_param1.Coverage. diff --git a/apps/derive/tests/test_param1_functor.v b/apps/derive/tests/test_param1_functor.v index 3960970fe..f41275e0d 100644 --- a/apps/derive/tests/test_param1_functor.v +++ b/apps/derive/tests/test_param1_functor.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.param1_functor. -From elpi.apps.derive.tests Require Import test_derive_stdlib test_param1. -Import test_derive_stdlib.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib test_param1. +Import test_derive_corelib.Coverage. Import test_param1.Coverage. Module Coverage. diff --git a/apps/derive/tests/test_param1_trivial.v b/apps/derive/tests/test_param1_trivial.v index 3761fee40..76923ff86 100644 --- a/apps/derive/tests/test_param1_trivial.v +++ b/apps/derive/tests/test_param1_trivial.v @@ -1,8 +1,8 @@ From elpi.apps Require Import derive.param1_trivial. -From elpi.apps Require Import test_derive_stdlib test_param1 test_param1_congr. +From elpi.apps Require Import test_derive_corelib test_param1 test_param1_congr. Import derive.param1. (* for is_eq *) -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Import test_param1.Coverage. Import test_param1_congr.Coverage. diff --git a/apps/derive/tests/test_projK.v b/apps/derive/tests/test_projK.v index b71559879..d49b9abf4 100644 --- a/apps/derive/tests/test_projK.v +++ b/apps/derive/tests/test_projK.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.projK. -From elpi.apps.derive.tests Require Import test_derive_stdlib. +From elpi.apps.derive.tests Require Import test_derive_corelib. -Import test_derive_stdlib.Coverage. +Import test_derive_corelib.Coverage. Module Coverage. Elpi derive.projK empty. diff --git a/apps/derive/tests/test_tag.v b/apps/derive/tests/test_tag.v index cac3f97ce..4f9b1a6c0 100644 --- a/apps/derive/tests/test_tag.v +++ b/apps/derive/tests/test_tag.v @@ -1,7 +1,7 @@ From elpi.apps Require Import derive.tag. -From elpi.apps.derive.tests Require Import test_derive_stdlib. -Import test_derive_stdlib.Coverage. +From elpi.apps.derive.tests Require Import test_derive_corelib. +Import test_derive_corelib.Coverage. Module Coverage. @@ -39,7 +39,7 @@ Elpi derive.tag val. End Coverage. Import Coverage. -Import PArith. +From elpi.core Require Import PosDef. Local Notation tag X := (X -> positive). diff --git a/apps/derive/theories/derive/EqdepFacts.v b/apps/derive/theories/derive/EqdepFacts.v new file mode 100644 index 000000000..7f25eb01b --- /dev/null +++ b/apps/derive/theories/derive/EqdepFacts.v @@ -0,0 +1,177 @@ +(* Borrowed from Stdlib.Logic.EqdepFacts *) + +Section Dependent_Equality. + +Variables (U : Type) (P : U -> Type). + +(** Dependent equality *) + +Inductive eq_dep (p : U) (x : P p) : forall q : U, P q -> Prop := + eq_dep_intro : eq_dep p x p x. +#[local] Hint Constructors eq_dep: core. + +Lemma eq_dep_sym (p q : U) (x : P p) (y : P q) : + eq_dep p x q y -> eq_dep q y p x. +Proof. destruct 1; auto. Qed. + +Scheme eq_indd := Induction for eq Sort Prop. + +Inductive eq_dep1 (p : U) (x : P p) (q : U) (y : P q) : Prop := + eq_dep1_intro : forall h : q = p, x = eq_rect _ _ y _ h -> eq_dep1 p x q y. + +Lemma eq_dep_dep1 (p q : U) (x : P p) (y : P q) : + eq_dep p x q y -> eq_dep1 p x q y. +Proof. +revert q x y; destruct 1. +apply eq_dep1_intro with (eq_refl p). +simpl; trivial. +Qed. + +End Dependent_Equality. + +Arguments eq_dep [U P] p x q _. +Arguments eq_dep1 [U P] p x q y. + +Section Equivalences. + +Variable U : Type. + +Definition Eq_rect_eq_on (p : U) (Q : U -> Type) (x : Q p) := + forall (h : p = p), x = eq_rect p Q x p h. +Definition Eq_rect_eq := forall p Q x, Eq_rect_eq_on p Q x. + +Definition Eq_dep_eq_on (P : U -> Type) (p : U) (x : P p) := + forall (y : P p), eq_dep p x p y -> x = y. +Definition Eq_dep_eq := forall P p x, Eq_dep_eq_on P p x. + +Definition UIP_on_ (x y : U) (p1 : x = y) := forall (p2 : x = y), p1 = p2. +Definition UIP_ := forall x y p1, UIP_on_ x y p1. + +Definition Streicher_K_on_ (x : U) (P : x = x -> Prop) := + P (eq_refl x) -> forall p : x = x, P p. +Definition Streicher_K_ := forall x P, Streicher_K_on_ x P. + +Lemma eq_rect_eq_on__eq_dep1_eq_on (p : U) (P : U -> Type) (y : P p) : + Eq_rect_eq_on p P y -> forall (x : P p), eq_dep1 p x p y -> x = y. +Proof. +intro eq_rect_eq. +simple destruct 1; intro. +rewrite <- eq_rect_eq; auto. +Qed. +Lemma eq_rect_eq__eq_dep1_eq : + Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y. +Proof. +exact (fun eq_rect_eq P p y x => + @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y). +Qed. + +Lemma eq_rect_eq_on__eq_dep_eq_on (p : U) (P : U -> Type) (x : P p) : + Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x. +Proof. +intros eq_rect_eq; red; intros y H. +symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq). +apply eq_dep_sym in H; apply eq_dep_dep1; trivial. +Qed. +Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. +Proof. +exact (fun eq_rect_eq P p x y => + @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y). +Qed. +Lemma eq_dep_eq_on__UIP_on (x y : U) (p1 : x = y) : + Eq_dep_eq_on (fun y => x = y) x eq_refl -> UIP_on_ x y p1. +Proof. +intro eq_dep_eq; red. +elim p1 using eq_indd. +intros p2; apply eq_dep_eq. +elim p2 using eq_indd. +apply eq_dep_intro. +Qed. +Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_. +Proof. +exact (fun eq_dep_eq x y p1 => + @eq_dep_eq_on__UIP_on x y p1 (eq_dep_eq _ _ _)). +Qed. + +Lemma Streicher_K_on__eq_rect_eq_on (p : U) (P : U -> Type) (x : P p) : + Streicher_K_on_ p (fun h => x = eq_rect _ P x _ h) -> Eq_rect_eq_on p P x. +Proof. +intro Streicher_K; red; intros. +apply Streicher_K. +reflexivity. +Qed. +Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq. +Proof. +exact (fun Streicher_K p P x => + @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)). +Qed. +End Equivalences. + +Arguments eq_dep U P p x q _ : clear implicits. + +Set Implicit Arguments. + +Section EqdepDec. + +Variable A : Type. + +Let comp (x y y' : A) (eq1 : x = y) (eq2 : x = y') : y = y' := + eq_ind _ (fun a => a = y') eq2 _ eq1. + +Remark trans_sym_eq (x y : A) (u : x = y) : comp u u = eq_refl y. +Proof. now case u. Qed. + +Variables (x : A) (eq_dec : forall y : A, x = y \/ x <> y). + +Let nu (y : A) (u : x = y) : x = y := + match eq_dec y with + | or_introl eqxy => eqxy + | or_intror neqxy => False_ind _ (neqxy u) + end. + +#[local] Lemma nu_constant (y:A) (u v:x = y) : nu u = nu v. +Proof. +unfold nu; destruct (eq_dec y) as [Heq|Hneq]; [reflexivity|]. +now case Hneq. +Qed. + +Let nu_inv (y : A) (v : x = y) : x = y := comp (nu (eq_refl x)) v. + +Remark nu_left_inv_on (y : A) (u : x = y) : nu_inv (nu u) = u. +Proof. case u; unfold nu_inv; apply trans_sym_eq. Qed. + +Theorem eq_proofs_unicity_on (y : A) (p1 p2 : x = y) : p1 = p2. +Proof. +elim (nu_left_inv_on p1). +elim (nu_left_inv_on p2). +now elim nu_constant with y p1 p2. +Qed. + +Theorem K_dec_on (P : x = x -> Prop) (H : P (eq_refl x)) (p : x = x) : P p. +Proof. now elim eq_proofs_unicity_on with x (eq_refl x) p. Qed. + +End EqdepDec. + +Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) : + forall P : x = x -> Prop, P (eq_refl x) -> forall p : x = x, P p. +Proof. exact (@K_dec_on A x (eq_dec x)). Qed. + +Section Eq_dec. + +Variables (A : Type) (eq_dec : forall x y : A, {x = y} + {x <> y}). + +Theorem K_dec_type (x : A) (P : x = x -> Prop) (H : P (eq_refl x)) (p : x = x) : + P p. +Proof. +elim p using K_dec; [|now trivial]. +now intros x0 y; case (eq_dec x0 y); [left|right]. +Qed. + +Theorem eq_rect_eq_dec : forall (p : A) (Q : A -> Type) (x : Q p) (h : p = p), + x = eq_rect p Q x p h. +Proof. exact (Streicher_K__eq_rect_eq A K_dec_type). Qed. + +Theorem eq_dep_eq_dec : forall (P : A->Type) (p : A) (x y : P p), + eq_dep A P p x p y -> x = y. +Proof. exact (eq_rect_eq__eq_dep_eq A eq_rect_eq_dec). Qed. + +End Eq_dec. diff --git a/apps/derive/theories/derive/bcongr.v b/apps/derive/theories/derive/bcongr.v index a52762a49..631abe2f0 100644 --- a/apps/derive/theories/derive/bcongr.v +++ b/apps/derive/theories/derive/bcongr.v @@ -8,7 +8,6 @@ From elpi.apps.derive.elpi Extra Dependency "bcongr.elpi" as bcongr. From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook. -From Coq Require Export Bool. From elpi Require Export elpi. From elpi.apps Require Export derive. From elpi.apps Require Export derive.projK. diff --git a/apps/derive/theories/derive/eq.v b/apps/derive/theories/derive/eq.v index 55ca01dec..8f3238034 100644 --- a/apps/derive/theories/derive/eq.v +++ b/apps/derive/theories/derive/eq.v @@ -6,11 +6,10 @@ From elpi.apps.derive.elpi Extra Dependency "eq.elpi" as eq. From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook. -From Coq Require Import Bool. From elpi Require Import elpi. From elpi.apps Require Import derive. -From Coq Require Import PrimInt63 PrimFloat. +From elpi.core Require Import PrimInt63 PrimFloat. Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63. Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64. diff --git a/apps/derive/theories/derive/eqK.v b/apps/derive/theories/derive/eqK.v index b0b9322b2..4078be992 100644 --- a/apps/derive/theories/derive/eqK.v +++ b/apps/derive/theories/derive/eqK.v @@ -8,18 +8,19 @@ From elpi.apps.derive.elpi Extra Dependency "eqK.elpi" as eqK. From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook. +From elpi.core Require Import Bool. (* remove when requiring Rocq >= 9.0 *) From elpi Require Import elpi. From elpi.apps Require Import derive. From elpi.apps Require Import derive.bcongr derive.eq derive.isK. Definition eq_axiom T eqb := - forall (x y : T), Bool.Bool.reflect (x = y) (eqb x y). + forall (x y : T), Datatypes.reflect (x = y) (eqb x y). Definition eq_axiom_at T eqb (x : T) := - forall y, Bool.Bool.reflect (x = y) (eqb x y). + forall y, Datatypes.reflect (x = y) (eqb x y). Definition eq_axiom_on T eqb (x y : T) := - Bool.Bool.reflect (x = y) (eqb x y). + Datatypes.reflect (x = y) (eqb x y). Register eq_axiom as elpi.derive.eq_axiom. Register eq_axiom_at as elpi.derive.eq_axiom_at. diff --git a/apps/derive/theories/derive/eqType_ast.v b/apps/derive/theories/derive/eqType_ast.v index 1aff8e359..bbe024410 100644 --- a/apps/derive/theories/derive/eqType_ast.v +++ b/apps/derive/theories/derive/eqType_ast.v @@ -1,5 +1,5 @@ From elpi Require Import elpi. -From Coq Require Import PrimInt63 PrimFloat. +From elpi.core Require Import PrimInt63 PrimFloat. From elpi.apps Require Import derive. From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType. diff --git a/apps/derive/theories/derive/eqb.v b/apps/derive/theories/derive/eqb.v index cdfe46db3..efa1ce8c0 100644 --- a/apps/derive/theories/derive/eqb.v +++ b/apps/derive/theories/derive/eqb.v @@ -1,7 +1,7 @@ From elpi Require Import elpi. From elpi.apps Require Import derive derive.param1. -From Coq Require Import ssrbool ssreflect Uint63. -From Coq Require Import PArith. +From elpi.core Require Import ssrbool ssreflect PrimInt63. +From elpi.core Require Import PosDef. From elpi.apps.derive.elpi Extra Dependency "fields.elpi" as fields. From elpi.apps.derive.elpi Extra Dependency "eqb.elpi" as eqb. diff --git a/apps/derive/theories/derive/eqb_core_defs.v b/apps/derive/theories/derive/eqb_core_defs.v index a02c89081..97424c324 100644 --- a/apps/derive/theories/derive/eqb_core_defs.v +++ b/apps/derive/theories/derive/eqb_core_defs.v @@ -1,12 +1,10 @@ -Require Import Eqdep_dec. -Require Import PArith. +From elpi.core Require Import PosDef. Require Import ssreflect ssrbool. +From elpi.apps.derive Require Import EqdepFacts. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Local Open Scope positive_scope. - Section Section. Context {A:Type}. @@ -31,6 +29,16 @@ Definition eqax_on (eqb : A -> A -> bool) (a1:A) := End Section. +Lemma pos_eq_dec : forall x y:positive, {x = y} + {x <> y}. +Proof. decide equality. Qed. + +Theorem UIP_dec (A : Type) (eq_dec : forall x y : A, {x = y} + {x <> y}) : + forall (x y : A) (p1 p2 : x = y), p1 = p2. +Proof. exact (eq_dep_eq__UIP A (eq_dep_eq_dec eq_dec)). Qed. + +Theorem bool_dec (b1 b2 : bool) : {b1 = b2} + {b1 <> b2}. +Proof. decide equality. Qed. + Section Section. Context {A B:Type}. @@ -51,13 +59,13 @@ Variable constructPB : forall a, constructB (fieldsB a) = Some a. Variable eqb_fields : forall t, fields_tA t -> fields_tB t -> bool. -Definition eqb_body (t1:positive) (f1:fields_tA t1) (x2:B) := +Definition eqb_body (t1:positive) (f1:fields_tA t1) (x2:B) := let t2 := tagB x2 in - match Pos.eq_dec t2 t1 with - | left heq => + match pos_eq_dec t2 t1 with + | left heq => let f2 : fields_tB t2 := fieldsB x2 in @eqb_fields t1 f1 (match heq with eq_refl => f2 end) - | right _ => false + | right _ => false end. #[global] Arguments eqb_body _ _ _ /. @@ -90,21 +98,21 @@ Proof. move=> hf a2 hb. suff : Some a1 = Some a2 by move=> [->]. rewrite -(constructP a2); move: hb; rewrite /eqb_body. - case: Pos.eq_dec => // heq. + case: pos_eq_dec => // heq. move: (tag a2) heq (fields a2) => t2 ?; subst t2 => f2 /=; apply hf. Qed. Definition eqb_fields_refl_on (a:A) := eqb_fields (fields a) (fields a). -Lemma eqb_body_refl a : - eqb_fields_refl_on a -> +Lemma eqb_body_refl a : + eqb_fields_refl_on a -> eqb_body fields eqb_fields (fields a) a. Proof. pose h := constructP. (* dummy dependence to have the same type as eqb_body_correct *) rewrite /eqb_body => hf. - case: Pos.eq_dec => // heq. - have -> /= := Eqdep_dec.UIP_dec Pos.eq_dec heq eq_refl; apply hf. + case: pos_eq_dec => // heq. + have -> /= := UIP_dec pos_eq_dec heq eq_refl; apply hf. Qed. Inductive blist := bnil | bcons (b : bool) (bs : blist). diff --git a/apps/derive/theories/derive/eqbcorrect.v b/apps/derive/theories/derive/eqbcorrect.v index 14b2b102e..cea2a188a 100644 --- a/apps/derive/theories/derive/eqbcorrect.v +++ b/apps/derive/theories/derive/eqbcorrect.v @@ -1,4 +1,4 @@ -From Coq Require Import ssreflect ssrfun ssrbool Eqdep_dec. +From elpi.core Require Import ssreflect ssrfun ssrbool. From elpi Require Import elpi. From elpi.apps Require Import derive. From elpi.apps.derive Require Import induction param1_functor param1_trivial eqb_core_defs tag fields eqb. @@ -22,7 +22,7 @@ Ltac solver_irrelevant := match goal with | p1 : ?x = true , p2 : ?x = true |- _ => let top := fresh "x" in - have top := @Eqdep_dec.UIP_dec bool Bool.bool_dec _ _ p1 p2; + have top := @eqb_core_defs.UIP_dec bool eqb_core_defs.bool_dec _ _ p1 p2; subst p1 end. @@ -35,11 +35,14 @@ Ltac eqb_refl_on__solver := repeat ((apply /andP; split) || reflexivity || assumption). End exports. +From elpi.core Require Uint63Axioms. + Lemma uint63_eqb_correct i : eqb_correct_on PrimInt63.eqb i. -Proof. by move=> j; case: (Uint63.eqb_spec i j); case: PrimInt63.eqb. Qed. +Proof. exact: Uint63Axioms.eqb_correct. Qed. Lemma uint63_eqb_refl i : eqb_refl_on PrimInt63.eqb i. -Proof. by case: (Uint63.eqb_spec i i) => _ H; exact: H. Qed. +Proof. exact: Uint63Axioms.eqb_refl. Qed. + Elpi Db derive.eqbcorrect.db lp:{{ @@ -93,7 +96,6 @@ Elpi Accumulate lp:{{ }}. - (* hook into derive *) Elpi Accumulate derive File eqbcorrect. Elpi Accumulate derive Db derive.eqbcorrect.db. diff --git a/apps/derive/theories/derive/eqcorrect.v b/apps/derive/theories/derive/eqcorrect.v index ac0901d93..3c0353849 100644 --- a/apps/derive/theories/derive/eqcorrect.v +++ b/apps/derive/theories/derive/eqcorrect.v @@ -11,12 +11,15 @@ From elpi Require Import elpi. From elpi.apps Require Import derive. From elpi.apps Require Import derive.eq derive.induction derive.eqK derive.param1. -From Coq Require Import ssreflect Uint63. +From elpi.core Require Import ssreflect PrimInt63. +From elpi.core Require Uint63Axioms. Lemma uint63_eq_correct i : is_uint63 i -> eq_axiom_at PrimInt63.int PrimInt63.eqb i. Proof. -move=> _ j; case: (Uint63.eqb_spec i j); case: PrimInt63.eqb => [-> // _|_ abs]; - [ by constructor | by constructor=> /abs ]. +move=> _ j; have [] : (eqb i j) = true <-> i = j. + split; first exact: Uint63Axioms.eqb_correct. + by move=> ->; rewrite Uint63Axioms.eqb_refl. +by case: PrimInt63.eqb => [-> // _| _ abs]; constructor=> // /abs. Qed. Register uint63_eq_correct as elpi.derive.uint63_eq_correct. diff --git a/apps/derive/theories/derive/fields.v b/apps/derive/theories/derive/fields.v index 439f81d64..973ee2d7d 100644 --- a/apps/derive/theories/derive/fields.v +++ b/apps/derive/theories/derive/fields.v @@ -1,6 +1,6 @@ From elpi Require Import elpi. From elpi.apps Require Import derive. -From Coq Require Import PArith. +From elpi.core Require Import PosDef. From elpi.apps Require Export derive.eqType_ast derive.tag. From elpi.apps.derive.elpi Extra Dependency "fields.elpi" as fields. From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType. diff --git a/apps/derive/theories/derive/param1.v b/apps/derive/theories/derive/param1.v index efb406967..5536da7c3 100644 --- a/apps/derive/theories/derive/param1.v +++ b/apps/derive/theories/derive/param1.v @@ -41,7 +41,7 @@ Class reali {X : Type} {XR : X -> Type} (x : X) (xR : XR x) := Reali {}. Register store_reali as param1.store_reali. -From Coq Require Import PrimInt63 PrimFloat. +From elpi.core Require Import PrimInt63 PrimFloat. Inductive is_uint63 : PrimInt63.int -> Type := uint63 (i : PrimInt63.int) : is_uint63 i. Register is_uint63 as elpi.derive.is_uint63. diff --git a/apps/derive/theories/derive/tag.v b/apps/derive/theories/derive/tag.v index f692194c5..ad3911bbd 100644 --- a/apps/derive/theories/derive/tag.v +++ b/apps/derive/theories/derive/tag.v @@ -1,6 +1,6 @@ From elpi Require Import elpi. From elpi.apps Require Import derive. -From Coq Require Import PArith. +From elpi.core Require Import PosDef. From elpi.apps.derive.elpi Extra Dependency "tag.elpi" as tag. From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook. From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook. diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune new file mode 100644 index 000000000..8c31d8a88 --- /dev/null +++ b/apps/eltac/tests-stdlib/dune @@ -0,0 +1,6 @@ +(coq.theory + (package coq-elpi-tests-stdlib) + (name elpi_apps_eltac_tests_stdlib) + (theories elpi elpi.apps.eltac elpi_stdlib)) + +(include_subdirs qualified) diff --git a/apps/eltac/tests/test_injection.v b/apps/eltac/tests-stdlib/test_injection.v similarity index 100% rename from apps/eltac/tests/test_injection.v rename to apps/eltac/tests-stdlib/test_injection.v diff --git a/apps/eltac/tests/test_apply.v b/apps/eltac/tests/test_apply.v index 24a93007f..b0f24ebaa 100644 --- a/apps/eltac/tests/test_apply.v +++ b/apps/eltac/tests/test_apply.v @@ -5,7 +5,9 @@ Proof. eltac.apply H. Qed. +Axiom add_comm : forall x y, x + y = y + x. + Goal (3 + 4 = 4 + 3). Proof. - eltac.apply PeanoNat.Nat.add_comm. -Qed. \ No newline at end of file + eltac.apply add_comm. +Qed. diff --git a/apps/eltac/tests/test_rewrite.v b/apps/eltac/tests/test_rewrite.v index 2c5425456..8bfcc4a2e 100644 --- a/apps/eltac/tests/test_rewrite.v +++ b/apps/eltac/tests/test_rewrite.v @@ -1,12 +1,15 @@ From elpi.apps Require Import eltac.rewrite. +Axiom add_comm : forall x y, x + y = y + x. +Axiom mul_comm : forall x y, x * y = y * x. + Goal (forall x : nat, 1 + x = x + 1) -> forall y, 2 * ((y+y) + 1) = ((y + y)+1) * 2. Proof. intro H. intro x. eltac.rewrite H. - eltac.rewrite PeanoNat.Nat.mul_comm. + eltac.rewrite mul_comm. exact eq_refl. Defined. @@ -37,8 +40,8 @@ Defined. Goal forall n, 2 * n = n * 2. Proof. intro n. - Fail eltac.rewrite PeanoNat.Nat.add_comm. - eltac.rewrite PeanoNat.Nat.add_comm "strong". + Fail eltac.rewrite add_comm. + eltac.rewrite add_comm "strong". Abort. End Example_rewrite. diff --git a/apps/locker/elpi/dune b/apps/locker/elpi/dune index 5f258ae21..989469a31 100644 --- a/apps/locker/elpi/dune +++ b/apps/locker/elpi/dune @@ -10,9 +10,7 @@ (action (with-stdout-to %{target} (progn - (echo "Require Import String.\nOpen Scope string_scope.\nLocal Definition _hash := \"\n") - (run coq_elpi_shafile %{deps}) - (echo "\".\n"))))) + (run coq_elpi_shafile %{deps}))))) (install (files diff --git a/apps/locker/tests/test_locker.v b/apps/locker/tests/test_locker.v index 0314a425d..9d06c9951 100644 --- a/apps/locker/tests/test_locker.v +++ b/apps/locker/tests/test_locker.v @@ -1,4 +1,4 @@ -From Coq Require Import ssreflect. +From elpi.core Require Import ssreflect. From elpi.apps Require Import locker. (* ----------------------- *) diff --git a/apps/locker/theories/locker.v b/apps/locker/theories/locker.v index 0520aba34..c5a4ad3f1 100644 --- a/apps/locker/theories/locker.v +++ b/apps/locker/theories/locker.v @@ -4,7 +4,7 @@ ------------------------------------------------------------------------- *) From elpi.apps.locker.elpi Extra Dependency "locker.elpi" as locker. -From Coq Require Import ssreflect. +From elpi.core Require Import ssreflect. From elpi Require Import elpi. (** [lock] locks a definition on an opaque key diff --git a/apps/tc/elpi/dune b/apps/tc/elpi/dune index 5e9205d56..b975a85b4 100644 --- a/apps/tc/elpi/dune +++ b/apps/tc/elpi/dune @@ -10,9 +10,7 @@ (action (with-stdout-to %{target} (progn - (echo "Require Import String.\nOpen Scope string_scope.\nLocal Definition _hash := \"\n") - (run coq_elpi_shafile %{deps}) - (echo "\".\n"))))) + (run coq_elpi_shafile %{deps}))))) (install (files diff --git a/apps/tc/examples/dune b/apps/tc/examples/dune index 70efd6993..7b78708c1 100644 --- a/apps/tc/examples/dune +++ b/apps/tc/examples/dune @@ -1,5 +1,5 @@ (coq.theory (name elpi.apps.tc.examples) - (theories elpi elpi.apps.tc)) + (theories elpi elpi.apps.tc elpi_stdlib)) (include_subdirs qualified) diff --git a/apps/tc/examples/tutorial.v b/apps/tc/examples/tutorial.v index fa780cb10..40735d185 100644 --- a/apps/tc/examples/tutorial.v +++ b/apps/tc/examples/tutorial.v @@ -1,4 +1,4 @@ -Require Import Bool. +From elpi_stdlib Require Import Bool. From elpi.apps Require Import tc. Class Eqb (T: Type) := { @@ -93,4 +93,5 @@ Module Backtrack. End Backtrack. TC.Print_instances. -TC.Get_class_info DecidableClass.Decidable. +(* Require Stdlib *) +(* TC.Get_class_info DecidableClass.Decidable. *) diff --git a/apps/tc/tests/bench/bench_inj.py b/apps/tc/tests-stdlib/bench/bench_inj.py similarity index 96% rename from apps/tc/tests/bench/bench_inj.py rename to apps/tc/tests-stdlib/bench/bench_inj.py index 95f1862e7..9a44376ab 100644 --- a/apps/tc/tests/bench/bench_inj.py +++ b/apps/tc/tests-stdlib/bench/bench_inj.py @@ -89,7 +89,7 @@ def buildTree(len): def writeFile(fileName: str, composeLen: int, isCoq: bool): PREAMBLE = f"""\ -From elpi.apps.tc.tests Require Import {"stdppInjClassic" if isCoq else "stdppInj"}. +From elpi_apps_tc_tests_stdlib Require Import {"stdppInjClassic" if isCoq else "stdppInj"}. {"" if isCoq else 'Elpi TC.Solver. Set TC Time Refine. Set TC Time Instance Search. Set TC Time Build Query. Set Debug "elpitime".'} """ GOAL = buildTree(composeLen) @@ -130,4 +130,4 @@ def loopTreeDepth(file_name: str, maxHeight: int, makeCoq=True, onlyOne=False): height = int(sys.argv[1]) loopTreeDepth(file_name, height, makeCoq=not ( "-nocoq" in sys.argv), onlyOne=("-onlyOne" in sys.argv)) - #writeFile(file_name, 1, False) \ No newline at end of file + #writeFile(file_name, 1, False) diff --git a/apps/tc/tests/bench/bench_inj.v b/apps/tc/tests-stdlib/bench/bench_inj.v similarity index 71% rename from apps/tc/tests/bench/bench_inj.v rename to apps/tc/tests-stdlib/bench/bench_inj.v index f549414b8..43dde51ab 100644 --- a/apps/tc/tests/bench/bench_inj.v +++ b/apps/tc/tests-stdlib/bench/bench_inj.v @@ -1,3 +1,3 @@ -From elpi.apps.tc.tests Require Import stdppInj. +From elpi_apps_tc_tests_stdlib Require Import stdppInj. Elpi TC.Solver. Set TC Time Refine. Set TC Time Instance Search. Set Debug "elpitime". Goal Inj eq eq((compose f f )). Time apply _. Qed. diff --git a/apps/tc/tests/bigTest.v b/apps/tc/tests-stdlib/bigTest.v similarity index 99% rename from apps/tc/tests/bigTest.v rename to apps/tc/tests-stdlib/bigTest.v index 7fa8f976f..89de2c8b3 100644 --- a/apps/tc/tests/bigTest.v +++ b/apps/tc/tests-stdlib/bigTest.v @@ -11,10 +11,11 @@ These two functions being defined both in [Coq.Bool] and in [Coq.Peano], we must export [Coq.Peano] later than any export of [Coq.Bool]. *) (* We also want to ensure that notations from [Coq.Utf8] take precedence over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *) -From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. -From Coq Require Import Permutation. +From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid. +From elpi_stdlib Require Export Bool List Peano Utf8 Permutation. +From elpi_stdlib Require Export Program.Basics Program.Syntax. + Export ListNotations. -From Coq.Program Require Export Basics Syntax. TC.AddAllClasses. TC.AddAllInstances. @@ -933,7 +934,7 @@ Section prod_setoid. Global Instance pair_proper : Proper ((≡) ==> (≡) ==> (≡@{A*B})) pair := _. Elpi Accumulate TC.Solver lp:{{ - shorten tc-elpi.apps.tc.tests.bigTest.{tc-Inj2}. + shorten tc-elpi_apps_tc_tests_stdlib.bigTest.{tc-Inj2}. % shorten tc-bigTest.{tc-Inj2}. :after "lastHook" tc-Inj2 A B C RA RB RC F S :- @@ -1058,7 +1059,7 @@ Global Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr Elpi Accumulate TC.Solver lp:{{ - shorten tc-elpi.apps.tc.tests.bigTest.{tc-Inj}. + shorten tc-elpi_apps_tc_tests_stdlib.bigTest.{tc-Inj}. % shorten tc-bigTest.{tc-Inj}. :after "lastHook" tc-Inj A B R1 R2 S C :- diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune new file mode 100644 index 000000000..91824cb3d --- /dev/null +++ b/apps/tc/tests-stdlib/dune @@ -0,0 +1,7 @@ +(coq.theory + (package coq-elpi-tests-stdlib) + (name elpi_apps_tc_tests_stdlib) + (flags :standard -async-proofs-cache force) + (theories elpi elpi.apps.tc elpi.apps.tc.tests elpi_stdlib)) + +(include_subdirs qualified) diff --git a/apps/tc/tests/eqSimplDef.v b/apps/tc/tests-stdlib/eqSimplDef.v similarity index 100% rename from apps/tc/tests/eqSimplDef.v rename to apps/tc/tests-stdlib/eqSimplDef.v diff --git a/apps/tc/tests/stdppInj.v b/apps/tc/tests-stdlib/stdppInj.v similarity index 95% rename from apps/tc/tests/stdppInj.v rename to apps/tc/tests-stdlib/stdppInj.v index 5ca615ad5..a427f9330 100644 --- a/apps/tc/tests/stdppInj.v +++ b/apps/tc/tests-stdlib/stdppInj.v @@ -1,9 +1,11 @@ (* Test inspired from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/base.v *) -From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. -From Coq Require Import Permutation. +From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid. +From elpi_stdlib Require Export List Peano Utf8 Permutation. +From elpi_stdlib Require Export Program.Basics Program.Syntax. + Export ListNotations. -From Coq.Program Require Export Basics Syntax. + From elpi.apps Require Import tc. Elpi TC Solver Override TC.Solver All. @@ -165,7 +167,7 @@ Section prod_setoid. Context `{Equiv A, Equiv B}. Elpi Accumulate TC.Solver lp:{{ - shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj2}. + shorten tc-elpi_apps_tc_tests_stdlib.stdppInj.{tc-Inj2}. % shorten tc-stdppInj.{tc-Inj2}. tc-Inj2 A B C RA RB RC F S :- RC = app [global {coq.locate "equiv"} | _], @@ -210,7 +212,7 @@ End sum_relation. Global Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡). Elpi Accumulate TC.Solver lp:{{ - shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. + shorten tc-elpi_apps_tc_tests_stdlib.stdppInj.{tc-Inj}. % shorten tc-stdppInj.{tc-Inj}. tc-Inj A B RA {{@equiv (sum _ _) (@sum_equiv _ _ _ _)}} S C :- tc-Inj A B RA {{sum_relation _ _}} S C. @@ -223,7 +225,7 @@ Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) : Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope. Elpi Accumulate TC.Solver lp:{{ - shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. + shorten tc-elpi_apps_tc_tests_stdlib.stdppInj.{tc-Inj}. tc-Inj A B RA RB F X :- F = fun _ _ _, G = {{@compose _ _ _ _ _}}, @@ -238,7 +240,7 @@ Global Instance h: Inj eq eq f. Qed. Elpi Accumulate TC.Solver lp:{{ - shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. + shorten tc-elpi_apps_tc_tests_stdlib.stdppInj.{tc-Inj}. :after "lastHook" tc-Inj A B RA RB F S :- F = (fun _ _ _), !, @@ -263,4 +265,4 @@ Qed. Goal Inj eq eq (fun (x: nat) => (compose id id) (id x)). apply (compose_inj eq eq); apply _. -Qed. \ No newline at end of file +Qed. diff --git a/apps/tc/tests/stdppInjClassic.v b/apps/tc/tests-stdlib/stdppInjClassic.v similarity index 97% rename from apps/tc/tests/stdppInjClassic.v rename to apps/tc/tests-stdlib/stdppInjClassic.v index 1bc27ad74..3eb0555ad 100644 --- a/apps/tc/tests/stdppInjClassic.v +++ b/apps/tc/tests-stdlib/stdppInjClassic.v @@ -1,8 +1,10 @@ (* File inspired from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/base.v *) -From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. -From Coq Require Import Permutation. +From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid. +From elpi_stdlib Require Export List Peano Utf8 Permutation. +From elpi_stdlib Require Export Program.Basics Program.Syntax. + Export ListNotations. -From Coq.Program Require Export Basics Syntax. + Notation length := Datatypes.length. Global Generalizable All Variables. @@ -216,4 +218,4 @@ Qed. *) Goal Inj eq eq (fun (x: nat) => (compose id id) (id x)). apply (compose_inj eq eq); apply _. -Qed. \ No newline at end of file +Qed. diff --git a/apps/tc/tests/test_commands_API.v b/apps/tc/tests-stdlib/test_commands_API.v similarity index 94% rename from apps/tc/tests/test_commands_API.v rename to apps/tc/tests-stdlib/test_commands_API.v index 090c6660c..e392af6b1 100644 --- a/apps/tc/tests/test_commands_API.v +++ b/apps/tc/tests-stdlib/test_commands_API.v @@ -1,5 +1,5 @@ From elpi.apps Require Import tc. -From elpi.apps.tc.tests Require Import eqSimplDef. +From elpi_apps_tc_tests_stdlib Require Import eqSimplDef. Elpi Command len_test. Elpi Accumulate Db tc.db. diff --git a/apps/tc/tests/test_import/f1.v b/apps/tc/tests-stdlib/test_import/f1.v similarity index 69% rename from apps/tc/tests/test_import/f1.v rename to apps/tc/tests-stdlib/test_import/f1.v index de8f271bc..40ad764d6 100644 --- a/apps/tc/tests/test_import/f1.v +++ b/apps/tc/tests-stdlib/test_import/f1.v @@ -1,4 +1,4 @@ From elpi.apps Require Export tc. -From Coq Require Export Morphisms. +From elpi.core Require Export Morphisms. Elpi TC Solver Override TC.Solver Rm Proper ProperProxy. diff --git a/apps/tc/tests-stdlib/test_import/f2.v b/apps/tc/tests-stdlib/test_import/f2.v new file mode 100644 index 000000000..aa9cffaed --- /dev/null +++ b/apps/tc/tests-stdlib/test_import/f2.v @@ -0,0 +1 @@ +From elpi_apps_tc_tests_stdlib.test_import Require Import f1. diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index 5610909d9..759112545 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -2,8 +2,6 @@ From elpi.apps Require Import tc. Elpi TC Solver Override TC.Solver All. -Require Import Bool. - (* TODO: How to add the #[deterministic] pragma in front of the class? *) (* #[deterministic] Class A (T : Type) := {succ : T -> T}. *) Class A (T : Type) := {succ : T -> T}. @@ -70,4 +68,4 @@ Proof. Import S. apply _. Fail apply _. -Abort. \ No newline at end of file +Abort. diff --git a/apps/tc/tests/indt_to_inst.v b/apps/tc/tests/indt_to_inst.v index f567fd7b9..df37b3611 100644 --- a/apps/tc/tests/indt_to_inst.v +++ b/apps/tc/tests/indt_to_inst.v @@ -1,4 +1,4 @@ -From Coq Require Export List. +From elpi.core Require Export ListDef. From elpi.apps Require Export tc. Global Generalizable All Variables. @@ -29,4 +29,4 @@ Module B. NoDup_elements2 (X : C) : NoDup (elements X) }. -End B. \ No newline at end of file +End B. diff --git a/apps/tc/tests/injTest.v b/apps/tc/tests/injTest.v index 52d44ed87..61e723bcb 100644 --- a/apps/tc/tests/injTest.v +++ b/apps/tc/tests/injTest.v @@ -1,5 +1,5 @@ From elpi.apps Require Import tc. -From Coq Require Import Morphisms RelationClasses List Bool Setoid Peano Utf8. +From elpi.core Require Import Morphisms RelationClasses ListDef Setoid. Generalizable All Variables. Elpi TC Solver Override TC.Solver All. @@ -8,8 +8,8 @@ Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) := inj x y : S (f x) (f y) -> R x y. Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) - (S : relation C) (f : A → B → C) : Prop := - inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2. + (S : relation C) (f : A -> B -> C) : Prop := + inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) -> R1 x1 y1 /\ R2 x2 y2. (* Elpi TC Solver Override TC.Solver Only Inj Inj2. *) @@ -65,7 +65,7 @@ Goal forall (T1 T2 : Type) (f: T1 -> T2), Qed. Elpi TC Solver Override TC.Solver All. -Local Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 ff} y : Inj R1 R3 (λ x, ff x y). +Local Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 ff} y : Inj R1 R3 (fun x => ff x y). Admitted. Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 ff} x : Inj R2 R3 (ff x). @@ -114,4 +114,4 @@ Proof. intros T x y z H. unfold z, y in H. apply _. -Qed. \ No newline at end of file +Qed. diff --git a/apps/tc/tests/test_import/f2.v b/apps/tc/tests/test_import/f2.v deleted file mode 100644 index efa2686e9..000000000 --- a/apps/tc/tests/test_import/f2.v +++ /dev/null @@ -1 +0,0 @@ -From elpi.apps.tc.tests.test_import Require Import f1. \ No newline at end of file diff --git a/apps/tc/tests/test_pending_mode.v b/apps/tc/tests/test_pending_mode.v index 9639a611a..527f15ac0 100644 --- a/apps/tc/tests/test_pending_mode.v +++ b/apps/tc/tests/test_pending_mode.v @@ -1,5 +1,4 @@ From elpi Require Import tc. -Require Import Bool. Module m1. Elpi TC.Pending_mode +. @@ -115,7 +114,7 @@ Module simplEq. Global Instance eqU : MyEqb unit := { eqb x y := true }. Global Instance eqB : MyEqb bool := { eqb x y := if x then y else negb y }. Global Instance eqP {A B} `{MyEqb A} `{MyEqb B} : MyEqb (A * B) := { - eqb x y := (fst x == fst y) && (snd x == snd y) }. + eqb x y := andb (fst x == fst y) (snd x == snd y) }. Fail Goal exists T: Type, forall n m : T, eqb n m = false. Goal forall n m : bool, eqb n m = false. Abort. diff --git a/coq-elpi.opam b/coq-elpi.opam index a8212b972..bad76eacb 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -18,14 +18,15 @@ depends: [ "dune" {>= "3.13"} "ocaml" {>= "4.10.0"} "elpi" {>= "2.0.7" & < "2.1.0~"} - "coq" {>= "8.20+rc1" & < "8.21~"} + ("coq" {>= "8.20+rc1" & < "8.21~"} + | "rocq-core" {>= "9.0+rc1" & < "9.1~"} & "coq-core") "ppx_optcomp" "ocaml-lsp-server" {with-dev-setup} "odoc" {with-doc} + "coq-stdlib" {with-doc} ] build: [ ["dune" "subst"] {dev} - [ make "elpi/dune"] [ "dune" "build" diff --git a/dune-project b/dune-project index 1967ac1ea..f615477be 100644 --- a/dune-project +++ b/dune-project @@ -40,3 +40,9 @@ (synopsis "Technical package to run tests") (description "Do not install") (depends coq-elpi)) + +(package + (name coq-elpi-tests-stdlib) + (synopsis "Technical package to run tests depending on Stdlib") + (description "Do not install") + (depends coq-elpi coq-stdlib)) diff --git a/elpi/dune.in b/elpi/dune similarity index 57% rename from elpi/dune.in rename to elpi/dune index f541c7392..fb14a6ddd 100644 --- a/elpi/dune.in +++ b/elpi/dune @@ -1,7 +1,6 @@ (coq.theory (name elpi_elpi) ; FIXME - (package coq-elpi) - @@STDLIB_THEORY@@) + (package coq-elpi)) (rule (target dummy.v) @@ -10,9 +9,7 @@ (action (with-stdout-to %{target} (progn - (echo "Require Import String.\nOpen Scope string_scope.\nLocal Definition _hash := \"\n") - (run coq_elpi_shafile %{deps}) - (echo "\".\n"))))) + (run coq_elpi_shafile %{deps}))))) (install (files diff --git a/elpi/elpi_elaborator.elpi b/elpi/elpi_elaborator.elpi index 0e01658c0..7ac65c33f 100644 --- a/elpi/elpi_elaborator.elpi +++ b/elpi/elpi_elaborator.elpi @@ -310,8 +310,8 @@ of (global GR as X) T X :- coq.env.typeof GR T1, unify-leq T1 T. of (pglobal GR I as X) T X :- (@uinstance! I => coq.env.typeof GR T1), unify-leq T1 T. -of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T. -of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T. +of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:num.int63.type }} T. +of (primitive (float64 _) as X) T X :- unify-leq {{ lib:num.float.type }} T. of (primitive (pstring _) as X) T X :- unify-leq {{ lib:elpi.pstring }} T. of (uvar as X) T Y :- !, evar X T Y. diff --git a/etc/shafile.ml b/etc/shafile.ml index 27f66aae0..4a266535f 100644 --- a/etc/shafile.ml +++ b/etc/shafile.ml @@ -1,3 +1,7 @@ +let mk_ident = + String.map (function '.' | '/' | '-' -> '_' | c -> c) + let () = Sys.argv |> Array.iter (fun file -> - Printf.printf "%s: %s\n" file @@ Digest.to_hex @@ Digest.file file) \ No newline at end of file + Printf.printf "Definition %s := 0x%s.\n" + (mk_ident file) @@ Digest.to_hex @@ Digest.file file) diff --git a/examples-stdlib/dune b/examples-stdlib/dune new file mode 100644 index 000000000..96a3ac4b8 --- /dev/null +++ b/examples-stdlib/dune @@ -0,0 +1,7 @@ +(coq.theory + (package coq-elpi-tests-stdlib) + (name elpi_examples_stdlib) + (plugins coq-elpi.elpi) + (theories elpi elpi_stdlib)) + +; (include_subdirs qualified) diff --git a/examples/example_open_terms.v b/examples-stdlib/example_open_terms.v similarity index 100% rename from examples/example_open_terms.v rename to examples-stdlib/example_open_terms.v diff --git a/examples/example_reflexive_tactic.v b/examples-stdlib/example_reflexive_tactic.v similarity index 100% rename from examples/example_reflexive_tactic.v rename to examples-stdlib/example_reflexive_tactic.v diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v index 90a75ed76..a070cd55e 100644 --- a/examples/tutorial_coq_elpi_tactic.v +++ b/examples/tutorial_coq_elpi_tactic.v @@ -1042,7 +1042,7 @@ Elpi Accumulate default lp:{{ }}. -From Coq Require Import Uint63. +From elpi.core Require Import PrimInt63. Open Scope uint63_scope. Fail Definition baz : list nat := default 1. (* .fails *) diff --git a/tests-stdlib/dune b/tests-stdlib/dune new file mode 100644 index 000000000..3793ba99d --- /dev/null +++ b/tests-stdlib/dune @@ -0,0 +1,7 @@ +(coq.theory + (package coq-elpi-tests-stdlib) + (name elpi_tests_stdlib) + (plugins coq-elpi.elpi) + (theories elpi elpi_stdlib)) + +; (include_subdirs qualified) diff --git a/tests/test_API_env.v b/tests-stdlib/test_API_env.v similarity index 98% rename from tests/test_API_env.v rename to tests-stdlib/test_API_env.v index 2d1f4391a..d60655fdb 100644 --- a/tests/test_API_env.v +++ b/tests-stdlib/test_API_env.v @@ -1,5 +1,5 @@ From elpi Require Import elpi. -From Coq Require Vector. +From elpi_stdlib Require Vector. (****** env **********************************) Elpi Command test. @@ -333,7 +333,7 @@ Elpi Query lp:{{ End HOAS. -From Coq Require Ranalysis5. +From elpi_stdlib Require Ranalysis5. Elpi Query lp:{{ @@ -372,7 +372,7 @@ Elpi Query lp:{{ Set Printing Universes. Print Module Test. Check Test.f. -From Coq Require Import ZArith. +From elpi_stdlib Require Import ZArith. Elpi Query lp:{{ coq.locate-module "N2Z" MP, diff --git a/tests/test_open_terms.v b/tests-stdlib/test_open_terms.v similarity index 99% rename from tests/test_open_terms.v rename to tests-stdlib/test_open_terms.v index a15cfc780..3600951e1 100644 --- a/tests/test_open_terms.v +++ b/tests-stdlib/test_open_terms.v @@ -1,6 +1,5 @@ -Require Import Arith List FunctionalExtensionality. +From elpi_stdlib Require Import ZArith Arith List FunctionalExtensionality. From elpi Require Import elpi. -Require Import ZArith. Lemma ring_example x : x + 1 = 1 + x. Proof. ring. Qed. diff --git a/tests/test_quotation.v b/tests-stdlib/test_quotation.v similarity index 97% rename from tests/test_quotation.v rename to tests-stdlib/test_quotation.v index 0f1de7764..e4cef5ec7 100644 --- a/tests/test_quotation.v +++ b/tests-stdlib/test_quotation.v @@ -29,7 +29,7 @@ Elpi Query lp:{{ coq.say BO1. }}. -Require Vector. +From elpi_stdlib Require Vector. Elpi Query lp:{{ T = {{ fun v : Vector.t nat 2 => @@ -92,7 +92,6 @@ Fail Elpi Query lp:{{ std.do! [ Fail Check hd. Fail Elpi File boom lp:{{ p :- X = {{ hd }}. }}. -From elpi.tests Extra Dependency "boom.elpi" as boom2. Import List. Check hd. Elpi File boom lp:{{ p :- X = {{ hd }}. }}. diff --git a/tests/test_API.v b/tests/test_API.v index a275bbf73..fea48ee13 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -1,5 +1,4 @@ From elpi Require Import elpi. -From Coq Require Vector. Elpi Command test.API. diff --git a/tests/test_API2.v b/tests/test_API2.v index b1b44cd72..03011ba03 100644 --- a/tests/test_API2.v +++ b/tests/test_API2.v @@ -80,7 +80,7 @@ main [] :- !, coq.say {coq.float->float64 1.2}. }}. -From Coq Require Import PrimFloat Uint63. +From elpi.core Require Import PrimFloat PrimInt63. Open Scope uint63_scope. diff --git a/tests/test_API_typecheck.v b/tests/test_API_typecheck.v index 73236f031..acb3d1473 100644 --- a/tests/test_API_typecheck.v +++ b/tests/test_API_typecheck.v @@ -1,6 +1,6 @@ From elpi Require Import elpi. -Require Import List. +From elpi.core Require Import ListDef. Elpi Command typecheck. diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index dd1275d59..9f513c62b 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -124,11 +124,10 @@ main [trm T] :- }}. -From Coq Require Import PrimInt63. -Open Scope int63_scope. +From elpi.core Require Import PrimInt63. Elpi primitive (PrimInt63.add 2000000003333002 1). -From Coq Require Import PrimFloat. +From elpi.core Require Import PrimFloat. Open Scope float_scope. Elpi primitive (2.4e13 + 1). End Pint. diff --git a/tests/test_elaborator.v b/tests/test_elaborator.v index 8e0f746f5..7443f8403 100644 --- a/tests/test_elaborator.v +++ b/tests/test_elaborator.v @@ -1,3 +1,5 @@ +From elpi.core Require Import PrimFloat. + From elpi_elpi Extra Dependency "elpi_elaborator.elpi" as elab. From elpi Require Import elpi. @@ -150,10 +152,8 @@ Elpi Query lp:{{get-option "of:coerce" tt => }}. (* primitive *) -From Coq Require Import Uint63. +From elpi.core Require Import PrimInt63. Elpi Query lp:{{ of {{ 99%uint63 }} T X }}. -From Coq Require Import Floats. Elpi Query lp:{{ of {{ 99.3e4%float }} T X }}. -Elpi Query lp:{{ whd1 {{ (99 + 1)%uint63 }} {{ 100%uint63 }} }}. -Elpi Query lp:{{ not(whd1 {{ (99 + _)%uint63 }} _) }}. - +Elpi Query lp:{{ whd1 {{ PrimInt63.add 99 1 }} {{ 100%uint63 }} }}. +Elpi Query lp:{{ not(whd1 {{ PrimInt63.add 99 _ }} _) }}. diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v index 9710e23b6..8ee29a3e4 100644 --- a/tests/test_ltac3.v +++ b/tests/test_ltac3.v @@ -1,6 +1,5 @@ - From elpi Require Export elpi. -From Coq Require Import ssreflect ssrfun ssrbool. +From elpi.core Require Import ssreflect ssrfun ssrbool. Ltac ltac_foo := cut True; [ idtac | abstract (exact I) ]. diff --git a/tests/test_synterp.v b/tests/test_synterp.v index f96b48642..cff650f62 100644 --- a/tests/test_synterp.v +++ b/tests/test_synterp.v @@ -1,4 +1,3 @@ -From Coq Require Import Bool. From elpi Require Import elpi. Elpi Command foo. diff --git a/theories-stdlib/Arith.v.in b/theories-stdlib/Arith.v.in new file mode 100644 index 000000000..04920cbde --- /dev/null +++ b/theories-stdlib/Arith.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export Arith. +#[skip="8.20"] From Stdlib Require Export Arith. + diff --git a/theories-stdlib/Bool.v.in b/theories-stdlib/Bool.v.in new file mode 100644 index 000000000..915ccaa12 --- /dev/null +++ b/theories-stdlib/Bool.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export Bool. +#[skip="8.20"] From Stdlib Require Export Bool. diff --git a/theories-stdlib/FunctionalExtensionality.v.in b/theories-stdlib/FunctionalExtensionality.v.in new file mode 100644 index 000000000..63a2e73ef --- /dev/null +++ b/theories-stdlib/FunctionalExtensionality.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export FunctionalExtensionality. +#[skip="8.20"] From Stdlib Require Export FunctionalExtensionality. + diff --git a/theories-stdlib/List.v.in b/theories-stdlib/List.v.in new file mode 100644 index 000000000..190fe8031 --- /dev/null +++ b/theories-stdlib/List.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export List. +#[skip="8.20"] From Stdlib Require Export List. + diff --git a/theories-stdlib/Peano.v.in b/theories-stdlib/Peano.v.in new file mode 100644 index 000000000..291744c89 --- /dev/null +++ b/theories-stdlib/Peano.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export Peano. +#[skip="8.20"] From Stdlib Require Export Peano. + diff --git a/theories-stdlib/Permutation.v.in b/theories-stdlib/Permutation.v.in new file mode 100644 index 000000000..7f221d6da --- /dev/null +++ b/theories-stdlib/Permutation.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export Permutation. +#[skip="8.20"] From Stdlib Require Export Permutation. + diff --git a/theories-stdlib/Program/Basics.v.in b/theories-stdlib/Program/Basics.v.in new file mode 100644 index 000000000..d5ebbebd3 --- /dev/null +++ b/theories-stdlib/Program/Basics.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq.Program Require Export Basics. +#[skip="8.20"] From Stdlib.Program Require Export Basics. + diff --git a/theories-stdlib/Program/Syntax.v.in b/theories-stdlib/Program/Syntax.v.in new file mode 100644 index 000000000..d3228e5ab --- /dev/null +++ b/theories-stdlib/Program/Syntax.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq.Program Require Export Syntax. +#[skip="8.20"] From Stdlib.Program Require Export Syntax. + diff --git a/theories-stdlib/Program/dune b/theories-stdlib/Program/dune new file mode 100644 index 000000000..5d2f6304e --- /dev/null +++ b/theories-stdlib/Program/dune @@ -0,0 +1,15 @@ +(rule + (target Basics.v) + (deps + (glob_files Basics.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Syntax.v) + (deps + (glob_files Syntax.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) \ No newline at end of file diff --git a/theories-stdlib/Ranalysis5.v.in b/theories-stdlib/Ranalysis5.v.in new file mode 100644 index 000000000..174608623 --- /dev/null +++ b/theories-stdlib/Ranalysis5.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export Ranalysis5. +#[skip="8.20"] From Stdlib Require Export Ranalysis5. + diff --git a/theories-stdlib/Utf8.v.in b/theories-stdlib/Utf8.v.in new file mode 100644 index 000000000..2a760eeb6 --- /dev/null +++ b/theories-stdlib/Utf8.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export Utf8. +#[skip="8.20"] From Stdlib Require Export Utf8. + diff --git a/theories-stdlib/Vector.v.in b/theories-stdlib/Vector.v.in new file mode 100644 index 000000000..6a43407f1 --- /dev/null +++ b/theories-stdlib/Vector.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export Vector. +#[skip="8.20"] From Stdlib Require Export Vector. + diff --git a/theories-stdlib/ZArith.v.in b/theories-stdlib/ZArith.v.in new file mode 100644 index 000000000..30b96df26 --- /dev/null +++ b/theories-stdlib/ZArith.v.in @@ -0,0 +1,3 @@ +#[only="8.20"] From Coq Require Export ZArith. +#[skip="8.20"] From Stdlib Require Export ZArith. + diff --git a/theories-stdlib/dune.in b/theories-stdlib/dune.in new file mode 100644 index 000000000..e9406839c --- /dev/null +++ b/theories-stdlib/dune.in @@ -0,0 +1,87 @@ +(coq.theory + (name elpi_stdlib) + (plugins coq-elpi.elpi) + (package coq-elpi-tests-stdlib) + (theories elpi_elpi elpi @@STDLIB@@)) + +(rule + (target Bool.v) + (deps + (glob_files Bool.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Vector.v) + (deps + (glob_files Vector.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Arith.v) + (deps + (glob_files Arith.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target ZArith.v) + (deps + (glob_files ZArith.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target FunctionalExtensionality.v) + (deps + (glob_files FunctionalExtensionality.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target List.v) + (deps + (glob_files List.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Ranalysis5.v) + (deps + (glob_files Ranalysis5.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Utf8.v) + (deps + (glob_files Utf8.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Peano.v) + (deps + (glob_files Peano.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Permutation.v) + (deps + (glob_files Permutation.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(include_subdirs qualified) \ No newline at end of file diff --git a/theories/attic/dune b/theories/attic/dune new file mode 100644 index 000000000..ff757cb8c --- /dev/null +++ b/theories/attic/dune @@ -0,0 +1 @@ +(include_subdirs no) diff --git a/theories/core/Bool.v.in b/theories/core/Bool.v.in new file mode 100644 index 000000000..4b42a1344 --- /dev/null +++ b/theories/core/Bool.v.in @@ -0,0 +1,4 @@ +#[only="8.20"] From Coq Require Export Bool. +#[only="8.20"] Module Datatypes. +#[only="8.20"] Notation reflect := Bool.reflect. +#[only="8.20"] End Datatypes. diff --git a/theories/core/ListDef.v.in b/theories/core/ListDef.v.in new file mode 100644 index 000000000..e58a29ebb --- /dev/null +++ b/theories/core/ListDef.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export List. +#[skip="8.20"] From Corelib Require Export ListDef. diff --git a/theories/core/Morphisms.v.in b/theories/core/Morphisms.v.in new file mode 100644 index 000000000..db7584add --- /dev/null +++ b/theories/core/Morphisms.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export Morphisms. +#[skip="8.20"] From Corelib Require Export Morphisms. diff --git a/theories/core/PosDef.v.in b/theories/core/PosDef.v.in new file mode 100644 index 000000000..6936f997e --- /dev/null +++ b/theories/core/PosDef.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export PArith. +#[skip="8.20"] From Corelib Require Export PosDef. diff --git a/theories/core/PrimFloat.v.in b/theories/core/PrimFloat.v.in new file mode 100644 index 000000000..dffc6212d --- /dev/null +++ b/theories/core/PrimFloat.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export Floats. +#[skip="8.20"] From Corelib Require Export PrimFloat. diff --git a/theories/core/PrimInt63.v.in b/theories/core/PrimInt63.v.in new file mode 100644 index 000000000..d41d5f1a4 --- /dev/null +++ b/theories/core/PrimInt63.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export Uint63. +#[skip="8.20"] From Corelib Require Export PrimInt63. diff --git a/theories/core/RelationClasses.v.in b/theories/core/RelationClasses.v.in new file mode 100644 index 000000000..abd53e718 --- /dev/null +++ b/theories/core/RelationClasses.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export RelationClasses. +#[skip="8.20"] From Corelib Require Export RelationClasses. diff --git a/theories/core/Setoid.v.in b/theories/core/Setoid.v.in new file mode 100644 index 000000000..3a7a630ea --- /dev/null +++ b/theories/core/Setoid.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export Setoid. +#[skip="8.20"] From Corelib Require Export Setoid. diff --git a/theories/core/Uint63Axioms.v.in b/theories/core/Uint63Axioms.v.in new file mode 100644 index 000000000..f99fd0c02 --- /dev/null +++ b/theories/core/Uint63Axioms.v.in @@ -0,0 +1,4 @@ +#[only="8.20"] From Coq Require Export Uint63. +#[skip="8.20"] From Corelib Require Export Uint63Axioms. +Definition eqb_correct := eqb_correct. +Definition eqb_refl := eqb_refl. diff --git a/theories/core/dune b/theories/core/dune new file mode 100644 index 000000000..7f82b0a5e --- /dev/null +++ b/theories/core/dune @@ -0,0 +1,98 @@ +; remove this directory when requiring Rocq >= 9.0 +; and replace all "From elpi.core" by "From Corelib" + +(rule + (target Bool.v) + (deps + (glob_files Bool.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target ListDef.v) + (deps + (glob_files ListDef.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Morphisms.v) + (deps + (glob_files Morphisms.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target PosDef.v) + (deps + (glob_files PosDef.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target PrimInt63.v) + (deps + (glob_files PrimInt63.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target PrimFloat.v) + (deps + (glob_files PrimFloat.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target RelationClasses.v) + (deps + (glob_files RelationClasses.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Setoid.v) + (deps + (glob_files Setoid.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target Uint63Axioms.v) + (deps + (glob_files Uint63Axioms.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target ssreflect.v) + (deps + (glob_files ssreflect.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target ssrfun.v) + (deps + (glob_files ssrfun.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + +(rule + (target ssrbool.v) + (deps + (glob_files ssrbool.v.in)) + (action + (with-stdout-to %{target} + (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) diff --git a/theories/core/ssrbool.v.in b/theories/core/ssrbool.v.in new file mode 100644 index 000000000..25608d191 --- /dev/null +++ b/theories/core/ssrbool.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export ssrbool. +#[skip="8.20"] From Corelib Require Export ssrbool. diff --git a/theories/core/ssreflect.v.in b/theories/core/ssreflect.v.in new file mode 100644 index 000000000..b2e88a90d --- /dev/null +++ b/theories/core/ssreflect.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export ssreflect. +#[skip="8.20"] From Corelib Require Export ssreflect. diff --git a/theories/core/ssrfun.v.in b/theories/core/ssrfun.v.in new file mode 100644 index 000000000..ef69c165e --- /dev/null +++ b/theories/core/ssrfun.v.in @@ -0,0 +1,2 @@ +#[only="8.20"] From Coq Require Export ssrfun. +#[skip="8.20"] From Corelib Require Export ssrfun. diff --git a/theories/dune b/theories/dune index 4f3a60a6e..d72cbd288 100644 --- a/theories/dune +++ b/theories/dune @@ -12,4 +12,4 @@ (with-stdout-to %{target} (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) -; (include_subdirs qualified) +(include_subdirs qualified) diff --git a/theories/elpi.v.in b/theories/elpi.v.in index 89b0555cb..cb3bef5d1 100644 --- a/theories/elpi.v.in +++ b/theories/elpi.v.in @@ -41,15 +41,17 @@ Register Coq.Init.Datatypes.andb as elpi.andb. Register Coq.Init.Datatypes.true as elpi.true. Register Coq.Init.Datatypes.false as elpi.false. -From Coq Require Bool. +#[only="8.20"] From Coq Require Bool. -Register Coq.Bool.Bool.reflect as elpi.reflect. -Register Coq.Bool.Bool.ReflectF as elpi.ReflectF. -Register Coq.Bool.Bool.ReflectT as elpi.ReflectT. +#[only="8.20"] Register Coq.Bool.Bool.reflect as elpi.reflect. +#[only="8.20"] Register Coq.Bool.Bool.ReflectF as elpi.ReflectF. +#[only="8.20"] Register Coq.Bool.Bool.ReflectT as elpi.ReflectT. +#[skip="8.20"] Register Corelib.Init.Datatypes.reflect as elpi.reflect. +#[skip="8.20"] Register Corelib.Init.Datatypes.ReflectF as elpi.ReflectF. +#[skip="8.20"] Register Corelib.Init.Datatypes.ReflectT as elpi.ReflectT. -From Coq Require PrimFloat PrimInt63. -From Coq Require PrimString. +#[only="8.20"] From Coq Require PrimString. +#[skip="8.20"] From Corelib Require PrimString. -Register Coq.Floats.PrimFloat.float as elpi.float64. -Register Coq.Numbers.Cyclic.Int63.PrimInt63.int as elpi.uint63. -Register Coq.Strings.PrimString.string as elpi.pstring. +#[only="8.20"] Register Coq.Strings.PrimString.string as elpi.pstring. +#[skip="8.20"] Register Corelib.Strings.PrimString.string as elpi.pstring. diff --git a/theories/wip/dune b/theories/wip/dune new file mode 100644 index 000000000..ff757cb8c --- /dev/null +++ b/theories/wip/dune @@ -0,0 +1 @@ +(include_subdirs no)