From dd08393edf67c0be4ca09496419f831b8404a3d9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Oct 2023 10:38:07 +0200 Subject: [PATCH 01/12] ci: re-enable nix --- .github/workflows/nix-action-coq-8.18.yml | 1213 +++++++++++++++++++++ .nix/config.nix | 5 +- 2 files changed, 1215 insertions(+), 3 deletions(-) create mode 100644 .github/workflows/nix-action-coq-8.18.yml diff --git a/.github/workflows/nix-action-coq-8.18.yml b/.github/workflows/nix-action-coq-8.18.yml new file mode 100644 index 000000000..7d08d1256 --- /dev/null +++ b/.github/workflows/nix-action-coq-8.18.yml @@ -0,0 +1,1213 @@ +jobs: + addition-chains: + needs: + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target addition-chains + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"addition-chains\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "paramcoq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "addition-chains" + category-theory: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target category-theory + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"category-theory\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "category-theory" + coq-elpi: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target coq-elpi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --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.18" + --argstr job "coq-elpi" + coquelicot: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target coquelicot + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coquelicot" + hierarchy-builder: + needs: + - coq-elpi + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target hierarchy-builder + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + interval: + needs: + - coquelicot + - mathcomp-ssreflect + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target interval + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "flocq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "interval" + mathcomp: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - mathcomp-field + - mathcomp-character + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp" + mathcomp-algebra: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-algebra + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + mathcomp-analysis: + needs: + - mathcomp-classical + - mathcomp-field + - mathcomp-bigenough + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-classical" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-analysis" + mathcomp-bigenough: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-bigenough" + mathcomp-character: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - mathcomp-field + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-character + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-character\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-character" + mathcomp-classical: + needs: + - mathcomp-algebra + - hierarchy-builder + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-classical" + mathcomp-field: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-field + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-field\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-field" + mathcomp-fingroup: + needs: + - mathcomp-ssreflect + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-fingroup + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-fingroup\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + mathcomp-solvable: + needs: + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-solvable + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-solvable\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-solvable" + mathcomp-ssreflect: + needs: + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-ssreflect + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + odd-order: + needs: + - mathcomp-character + - mathcomp-ssreflect + - mathcomp-fingroup + - mathcomp-algebra + - mathcomp-solvable + - mathcomp-field + - mathcomp + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target odd-order + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "odd-order" + trakt: + needs: + - coq-elpi + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target trakt + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"trakt\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "trakt" +name: Nix CI for bundle coq-8.18 +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.nix/config.nix b/.nix/config.nix index ead6869ee..d39bea2e4 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -1,11 +1,10 @@ { format = "1.0.0"; attribute = "coq-elpi"; - default-bundle = "coq-8.17"; + default-bundle = "coq-8.18"; bundles = { - "coq-8.17".coqPackages = { - coq.override.version = "8.17"; + "coq-8.18".coqPackages = { hierarchy-builder.override.version = "master"; hierarchy-builder-shim.job = false; From 6d792e90de19cebd88c2d2613607512a551fcc5a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 13 Oct 2023 14:57:30 +0200 Subject: [PATCH 02/12] update toolbox --- .nix/coq-nix-toolbox.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index ff29c1895..de2cac5a4 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"e2a21e50cd134b50c7e590b66ad14ec4905e16cd" +"95c6764e932cd20d037ad13fead23f2540f0ac7c" From c06b2701eb865a6d8710b059c3c2a0469cf832c4 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 13 Oct 2023 14:59:14 +0200 Subject: [PATCH 03/12] regen action --- .github/workflows/nix-action-coq-8.18.yml | 255 +++++++++++++++------- 1 file changed, 174 insertions(+), 81 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.18.yml b/.github/workflows/nix-action-coq-8.18.yml index 7d08d1256..2fbc8f05c 100644 --- a/.github/workflows/nix-action-coq-8.18.yml +++ b/.github/workflows/nix-action-coq-8.18.yml @@ -1,4 +1,68 @@ jobs: + Verdi: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target Verdi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"Verdi\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: Cheerios' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "Cheerios" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: InfSeqExt' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "InfSeqExt" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "Verdi" addition-chains: needs: - mathcomp-ssreflect @@ -43,8 +107,8 @@ jobs: name: Checking presence of CI target addition-chains run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"addition-chains\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -69,7 +133,7 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "addition-chains" - category-theory: + autosubst: needs: - mathcomp-ssreflect runs-on: ubuntu-latest @@ -108,11 +172,11 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target category-theory + name: Checking presence of CI target autosubst run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.18\" --argstr job \"category-theory\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.18\" --argstr job \"autosubst\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -121,14 +185,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "equations" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "category-theory" + --argstr job "autosubst" coq-elpi: needs: [] runs-on: ubuntu-latest @@ -170,8 +230,8 @@ jobs: name: Checking presence of CI target coq-elpi run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -222,8 +282,8 @@ jobs: name: Checking presence of CI target coquelicot run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -236,9 +296,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "coquelicot" - hierarchy-builder: + deriving: needs: - - coq-elpi + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -275,28 +335,26 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target hierarchy-builder + name: Checking presence of CI target deriving run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.18\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.18\" --argstr job \"deriving\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "coq-elpi" + --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "hierarchy-builder" - interval: + --argstr job "deriving" + hierarchy-builder: needs: - - coquelicot - - mathcomp-ssreflect - - mathcomp-fingroup + - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -333,39 +391,23 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target interval + name: Checking presence of CI target hierarchy-builder run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.18\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.18\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coquelicot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "coquelicot" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: flocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "flocq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' + name: 'Building/fetching previous CI target: coq-elpi' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "mathcomp-fingroup" + --argstr job "coq-elpi" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "interval" + --argstr job "hierarchy-builder" mathcomp: needs: - mathcomp-ssreflect @@ -414,8 +456,8 @@ jobs: name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -496,8 +538,8 @@ jobs: name: Checking presence of CI target mathcomp-algebra run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -563,8 +605,8 @@ jobs: name: Checking presence of CI target mathcomp-analysis run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -631,8 +673,8 @@ jobs: name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -692,8 +734,8 @@ jobs: name: Checking presence of CI target mathcomp-character run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-character\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -730,7 +772,6 @@ jobs: needs: - mathcomp-algebra - hierarchy-builder - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -770,8 +811,8 @@ jobs: name: Checking presence of CI target mathcomp-classical run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -784,10 +825,6 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" - --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -838,8 +875,8 @@ jobs: name: Checking presence of CI target mathcomp-field run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-field\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -911,8 +948,8 @@ jobs: name: Checking presence of CI target mathcomp-fingroup run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-fingroup\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -974,8 +1011,8 @@ jobs: name: Checking presence of CI target mathcomp-solvable run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-solvable\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -1042,8 +1079,8 @@ jobs: name: Checking presence of CI target mathcomp-ssreflect run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -1104,8 +1141,8 @@ jobs: name: Checking presence of CI target odd-order run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -1142,6 +1179,62 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "odd-order" + reglang: + needs: + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target reglang + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"reglang\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "reglang" trakt: needs: - coq-elpi @@ -1184,8 +1277,8 @@ jobs: name: Checking presence of CI target trakt run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq-8.18\" --argstr job \"trakt\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" From 539cb4fc67b215894a73d182a767a6dfa9f78ee1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Oct 2023 11:02:20 +0200 Subject: [PATCH 04/12] Update coq-nix-toolbox.nix --- .nix/coq-nix-toolbox.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index de2cac5a4..8fb619add 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"95c6764e932cd20d037ad13fead23f2540f0ac7c" +"cef6668e637efb2941cbda0ac0f0a435730fa3c1" From b164a15f7974b1ed2387f5a2d80efe45b2ee83b1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Oct 2023 11:03:36 +0200 Subject: [PATCH 05/12] Create overlay MC-classical --- .nix/ coq-overlays/mathcomp-classical /default.nix | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 .nix/ coq-overlays/mathcomp-classical /default.nix diff --git a/.nix/ coq-overlays/mathcomp-classical /default.nix b/.nix/ coq-overlays/mathcomp-classical /default.nix new file mode 100644 index 000000000..193265f29 --- /dev/null +++ b/.nix/ coq-overlays/mathcomp-classical /default.nix @@ -0,0 +1,2 @@ +{ mathcomp-analysis, version ? null }: +mathcomp-analysis.classical.override {inherit version;} From b5a6c60ccd2b8958daf1ad54774aa09fea0c4db0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Oct 2023 13:42:38 +0200 Subject: [PATCH 06/12] Update .nix/config.nix --- .nix/config.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/.nix/config.nix b/.nix/config.nix index d39bea2e4..86a920d7e 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -6,6 +6,7 @@ "coq-8.18".coqPackages = { hierarchy-builder.override.version = "master"; + coq.override.version = "8.18"; hierarchy-builder-shim.job = false; mathcomp.override.version = "master"; From da189c61c1bcb8572368d18bae55c5476815ee17 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 19 Oct 2023 16:37:53 +0100 Subject: [PATCH 07/12] wip --- src/coq_elpi_HOAS.ml | 3 +- src/coq_elpi_arg_HOAS.ml | 3 + src/coq_elpi_arg_HOAS.mli | 6 ++ src/coq_elpi_glob_quotation.ml | 3 +- src/coq_elpi_programs.mli | 1 + src/coq_elpi_vernacular.ml | 99 +++++++++++++++++++----------- src/coq_elpi_vernacular.mli | 2 +- src/coq_elpi_vernacular_syntax.mlg | 4 +- 8 files changed, 80 insertions(+), 41 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 8c65bd859..5b4783904 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -793,7 +793,8 @@ let from_env_keep_univ_of_sigma ~env0 ~env sigma0 = let uctx = UState.demote_global_univs env uctx in from_env_sigma env (Evd.from_ctx uctx) - let init () = from_env (Global.env ()) + let init () = + if !Flags.in_synterp_phase then from_env_sigma Environ.empty_env Evd.empty else from_env (Global.env ()) let engine : coq_engine S.component = S.declare ~name:"coq-elpi:evmap-constraint-type" diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 4f122d67b..96582a479 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -786,6 +786,9 @@ let handle_template_polymorphism = function | Some false -> Some false | Some true -> err Pp.(str "#[universes(template)] is not supported") +let in_elpi_cmd_synterp ~depth ?calldepth coq_ctx state (x : Cmd.raw) = + in_elpi_int_arg ~depth state 1 + let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) = let open Cmd in let hyps = [] in diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli index 98540e482..c2fdfae93 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/coq_elpi_arg_HOAS.mli @@ -122,6 +122,12 @@ val in_elpi_cmd : raw:bool -> Cmd.top -> Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals +val in_elpi_cmd_synterp : + depth:int -> ?calldepth:int -> + Coq_elpi_HOAS.empty Coq_elpi_HOAS.coq_context -> + Elpi.API.State.t -> + Cmd.raw -> + Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geninterp.Val.t diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index bd1e2fbb4..7985063b3 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -61,7 +61,8 @@ let is_restricted_name = let glob_environment : Environ.env S.component = S.declare ~name:"coq-elpi:glob-environment" - ~pp:(fun _ _ -> ()) ~init:Global.env ~start:(fun _ -> Global.env ()) + ~pp:(fun _ _ -> ()) ~init:(fun () -> if !Flags.in_synterp_phase then Environ.empty_env else Global.env ()) + ~start:(fun _ -> if !Flags.in_synterp_phase then Environ.empty_env else Global.env ()) let push_env state name = let open Context.Rel.Declaration in diff --git a/src/coq_elpi_programs.mli b/src/coq_elpi_programs.mli index 63879f2fe..733c731b9 100644 --- a/src/coq_elpi_programs.mli +++ b/src/coq_elpi_programs.mli @@ -86,6 +86,7 @@ module Code : sig val hash : 'db t -> int val cache : 'db t -> bool val eq : ('db -> 'db -> bool) -> 'db t -> 'db t -> bool + val snoc_opt : cunit -> 'db t option -> 'db t end val code : qualified_name -> Chunk.t Code.t diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 5a1f86503..a270ea123 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -108,28 +108,26 @@ let recache_chunk b h1 h2 p src = uncache b h1 compiler_cache_chunk; cache_chunk b h2 p src -let get_and_compile name = - let src = code name in - let prog = - let rec compile_code src = - let h = Code.hash src in - try - lookup_code 0 h src - with Not_found -> - match src with - | Code.Base { base = (k,u) } -> - let elpi = ensure_initialized () in - let prog = assemble_units ~elpi [u] in - cache_code 0 h prog src - | Code.Snoc { prev; source } -> - let base = compile_code prev in - let prog = extend_w_units ~base [snd source] in - if Code.cache src then cache_code 0 h prog src else prog - | Code.Snoc_db { prev; chunks } -> - let base = compile_code prev in - let prog = compile_chunk (Code.hash prev) base chunks in - prog - and compile_chunk bh base src = +let compile src = + let rec compile_code src = + let h = Code.hash src in + try + lookup_code 0 h src + with Not_found -> + match src with + | Code.Base { base = (k,u) } -> + let elpi = ensure_initialized () in + let prog = assemble_units ~elpi [u] in + cache_code 0 h prog src + | Code.Snoc { prev; source } -> + let base = compile_code prev in + let prog = extend_w_units ~base [snd source] in + if Code.cache src then cache_code 0 h prog src else prog + | Code.Snoc_db { prev; chunks } -> + let base = compile_code prev in + let prog = compile_chunk (Code.hash prev) base chunks in + prog + and compile_chunk bh base src = (* DBs have to be re-based on top of base, hence bh *) let h = Chunk.hash src in try @@ -143,12 +141,16 @@ let get_and_compile name = let base = compile_chunk bh base prev in let prog = extend_w_units ~base (List.rev_map snd source_rev) in recache_chunk bh (Chunk.hash prev) h prog src - in - let prog = compile_code src in - let new_hash = Code.hash src in - let old_hash = try SLMap.find name !programs_tip with Not_found -> 0 in - programs_tip := SLMap.add name new_hash !programs_tip; - recache_code 0 old_hash new_hash prog src in + in + compile_code src + +let get_and_compile name = + let src = code name in + let prog = compile src in + let new_hash = Code.hash src in + let old_hash = try SLMap.find name !programs_tip with Not_found -> 0 in + programs_tip := SLMap.add name new_hash !programs_tip; + let prog = recache_code 0 old_hash new_hash prog src in let raw_args = match get_nature name with | Command { raw_args } -> raw_args @@ -305,6 +307,24 @@ let run_program loc name ~atts args = run_and_print ~print:false ~static_check:false name program (`Fun query) ;; +let run_program_synterp loc name ~atts code _args = + match code with + | None -> () + | Some code -> + let program = compile (Code.snoc_opt code None) in + let loc = Coq_elpi_utils.of_coq_loc loc in + let query ~depth state = + let state, args, gls = EU.map_acc + (Coq_elpi_arg_HOAS.in_elpi_cmd_synterp ~depth Coq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state)) + state [] in + let state, q = atts2impl loc ~depth state atts (ET.mkApp mainc (EU.list_to_lp_list args) []) in + let state = API.State.set Coq_elpi_builtins.tactic_mode state false in + let state = API.State.set Coq_elpi_builtins.invocation_site_loc state loc in + state, (loc, q), gls in + + run_and_print ~print:false ~static_check:false name program (`Fun query) + ;; + let mk_trace_opts start stop preds = [ "-trace-on" ; "-trace-at"; "run"; string_of_int start; string_of_int stop @@ -453,7 +473,12 @@ let loc_merge l1 l2 = try Loc.merge l1 l2 with Failure _ -> l1 -let cache_program (nature,p,p_str) = +type synterp_code = (Elpi.API.Ast.Loc.t * string) option + +let cache_program (nature,p,p_str,synterp_code) = + let synterp_code = synterp_code |> Option.map (fun (loc,s) -> + let elpi = ensure_initialized () in + unit_from_string ~elpi loc s) in match nature with | Command _ -> let ext = @@ -476,7 +501,9 @@ let cache_program (nature,p,p_str) = (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyNil))))) - (fun loc0 args loc1 ?loc ~atts () -> Vernacextend.vtdefault (fun () -> + (fun loc0 args loc1 ?loc ~atts () -> + run_program_synterp (Option.default (loc_merge loc0 loc1) loc) p ~atts synterp_code args; + Vernacextend.vtdefault (fun () -> run_program (Option.default (loc_merge loc0 loc1) loc) p ~atts args)) in Egramml.extend_vernac_command_grammar ~undoable:true ext @@ -487,20 +514,20 @@ let cache_program (nature,p,p_str) = CErrors.user_err Pp.(str "elpi: Only commands and tactics can be exported") let subst_program = function - | _, (Command _, _, _) -> CErrors.user_err Pp.(str"elpi: No functors yet") - | _, (Tactic,_,_ as x) -> x - | _, (Program _,_,_) -> assert false + | _, (Command _,_,_,_) -> CErrors.user_err Pp.(str"elpi: No functors yet") + | _, (Tactic,_,_,_ as x) -> x + | _, (Program _,_,_,_) -> assert false -let in_exported_program : nature * qualified_name * string -> Libobject.obj = +let in_exported_program : nature * qualified_name * string * synterp_code -> Libobject.obj = let open Libobject in declare_object @@ { (global_object_nodischarge "ELPI-EXPORTED" ~cache:cache_program ~subst:(Some subst_program)) with object_stage = Summary.Stage.Synterp } -let export_command p = +let export_command p synterp_code = let p_str = String.concat "." p in let nature = get_nature p in - Lib.add_leaf (in_exported_program (nature,p,p_str)) + Lib.add_leaf (in_exported_program (nature,p,p_str,synterp_code)) let skip ~atts:(skip,only) f x = let m rex = Str.string_match rex Coq_config.version 0 in diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index 64a132d82..8ecdf6eb2 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -49,7 +49,7 @@ val run_in_program : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> u val run_tactic : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Geninterp.interp_sign -> Tac.top list -> unit Proofview.tactic val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Geninterp.interp_sign -> unit Proofview.tactic -val export_command : qualified_name -> unit +val export_command : qualified_name -> (Elpi.API.Ast.Loc.t * string) option -> unit val atts2impl : Elpi.API.Ast.Loc.t -> depth:int -> Elpi.API.State.t -> Attributes.vernac_flags -> diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 4c7c8e4fc..d3a7ee806 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -231,8 +231,8 @@ VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([ | #[ atts = any_attribute ] [ "Elpi" "Query" qualified_name(p) elpi_string(s) ] -> { let () = ignore_unknown_attributes atts in EV.run_in_program ~program:(snd p) s } -| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } SYNTERP AS _ { - EV.export_command (snd p) +| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) elpi_string_opt(synterp_code) ] => { Vernacextend.(VtSideff ([],VtNow)) } SYNTERP AS _ { + EV.export_command (snd p) synterp_code } -> { let () = ignore_unknown_attributes atts in () From ee1f82e53f3431cba997734876531d5d9428b4af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Oct 2023 14:33:30 +0200 Subject: [PATCH 08/12] port to elpi 1.18.0 --- coq-elpi.opam | 2 +- src/coq_elpi_HOAS.ml | 16 ++++++++-------- src/coq_elpi_arg_HOAS.ml | 10 +++++----- src/coq_elpi_builtins.ml | 14 +++++++------- src/coq_elpi_glob_quotation.ml | 17 ++++++++--------- src/coq_elpi_name_quotation.ml | 18 +++++++++++------- src/coq_elpi_programs.ml | 2 +- src/coq_elpi_utils.ml | 9 +++++++++ src/coq_elpi_utils.mli | 7 +++++++ 9 files changed, 57 insertions(+), 38 deletions(-) diff --git a/coq-elpi.opam b/coq-elpi.opam index 5fb2abfba..b672b177e 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -14,7 +14,7 @@ build: [ [ make "build" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAML install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ] depends: [ "stdlib-shims" - "elpi" {>= "1.16.5" & < "1.18.0~"} + "elpi" {>= "1.18.0" & < "1.19.0~"} "coq" {>= "8.18" & < "8.19~" } "dot-merlin-reader" {with-dev} "ocaml-lsp-server" {with-dev} diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 5b4783904..60e1951af 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -89,8 +89,8 @@ module UM = F.Map(struct let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr UnivNames.pr_with_global_universes x) end) -let um = S.declare ~name:"coq-elpi:evar-univ-map" - ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x) +let um = S.declare_component ~name:"coq-elpi:evar-univ-map" ~descriptor:interp_state + ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x) () let constraint_leq u1 u2 = @@ -794,11 +794,11 @@ let from_env_keep_univ_of_sigma ~env0 ~env sigma0 = from_env_sigma env (Evd.from_ctx uctx) let init () = - if !Flags.in_synterp_phase then from_env_sigma Environ.empty_env Evd.empty else from_env (Global.env ()) + from_env (Global.env ()) let engine : coq_engine S.component = - S.declare ~name:"coq-elpi:evmap-constraint-type" - ~pp:pp_coq_engine ~init ~start:(fun _ -> init()) + S.declare_component ~name:"coq-elpi:evmap-constraint-type" ~descriptor:interp_state + ~pp:pp_coq_engine ~init ~start:(fun _ -> init()) () end let () = pre_engine := Some CoqEngine_HOAS.engine @@ -1447,7 +1447,7 @@ let prepend_removals l = let removals, rest = List.partition (function RmEvar _ -> true | _ -> false) l in removals @ rest -let () = E.set_extra_goals_postprocessing (fun l state -> +let () = E.set_extra_goals_postprocessing ~descriptor:interp_hoas (fun l state -> generate_actual_goals state (prepend_removals (cancel_opposites Evar.Set.empty (removals_of Evar.Set.empty l) l))) @@ -1648,8 +1648,8 @@ module UIM = F.Map(struct let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr UnivNames.pr_with_global_universes x) end) -let uim = S.declare ~name:"coq-elpi:evar-univ-instance-map" - ~pp:UIM.pp ~init:(fun () -> UIM.empty) ~start:(fun x -> x) +let uim = S.declare_component ~name:"coq-elpi:evar-univ-instance-map" ~descriptor:interp_state + ~pp:UIM.pp ~init:(fun () -> UIM.empty) ~start:(fun x -> x) () let in_coq_poly_gref ~depth ~origin ~failsafe s t i = let open API.Conversion in diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 96582a479..4cfe50ac8 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -25,7 +25,7 @@ let push_inductive_in_intern_env intern_env name params arity user_impls = let env = Global.env () in let sigma = Evd.from_env env in let sigma, ty = Pretyping.understand_tcc env sigma ~expected_type:Pretyping.IsType (Coq_elpi_utils.mk_gforall arity params) in - Constrintern.compute_internalization_env env sigma ~impls:intern_env + ty, Constrintern.compute_internalization_env env sigma ~impls:intern_env Constrintern.Inductive [name] [ty] [user_impls] let intern_tactic_constr = Ltac_plugin.Tacintern.intern_constr @@ -34,9 +34,9 @@ let intern_global_constr { Ltac_plugin.Tacintern.genv = env } ~intern_env t = let sigma = Evd.from_env env in Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t -let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ~intern_env t = +let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ~intern_env ?(expty=Pretyping.IsType) t = let sigma = Evd.from_env env in - Constrintern.intern_gen Pretyping.IsType env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t + Constrintern.intern_gen expty env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t let intern_global_context { Ltac_plugin.Tacintern.genv = env } ~intern_env ctx = Constrintern.intern_context env ~bound_univs:UnivNames.empty_binders intern_env ctx @@ -293,10 +293,10 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform let glob_sign_params = push_glob_ctx allparams glob_sign in let arity = intern_global_constr_ty ~intern_env glob_sign_params indexes in let glob_sign_params_self = push_name glob_sign_params (Names.Name name) in - let intern_env = push_inductive_in_intern_env intern_env name allparams arity user_impls in + let indty, intern_env = push_inductive_in_intern_env intern_env name allparams arity user_impls in let constructors = List.map (fun (id,ty) -> id.CAst.v, - intern_global_constr_ty glob_sign_params_self ~intern_env ty) constructors in + intern_global_constr_ty ~expty:(Pretyping.OfType indty) glob_sign_params_self ~intern_env ty) constructors in { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly } let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ebb75198c..599743b00 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -100,14 +100,14 @@ let pr_econstr_env options env sigma t = if options.hoas_holes = Some Heuristic then aux () expr else expr in Ppconstr.pr_constr_expr_n env sigma options.pplevel expr) -let tactic_mode = State.declare ~name:"coq-elpi:tactic-mode" +let tactic_mode : bool State.component = State.declare_component ~name:"coq-elpi:tactic-mode" ~descriptor:interp_state ~pp:(fun fmt x -> Format.fprintf fmt "%b" x) ~init:(fun () -> false) - ~start:(fun x -> x) -let invocation_site_loc = State.declare ~name:"coq-elpi:invocation-site-loc" + ~start:(fun x -> x) () +let invocation_site_loc : API.Ast.Loc.t State.component = State.declare_component ~name:"coq-elpi:invocation-site-loc" ~descriptor:interp_state ~pp:(fun fmt x -> Format.fprintf fmt "%a" API.Ast.Loc.pp x) ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)") - ~start:(fun x -> x) + ~start:(fun x -> x) () let abstract__grab_global_env_keep_sigma api thunk = (); (fun state -> let state, result, gls = thunk state in @@ -195,15 +195,15 @@ let constr2lp_closed ~depth hyps constraints state t = let constr2lp_closed_ground ~depth hyps constraints state t = constr2lp_closed_ground ~depth hyps constraints state t -let clauses_for_later = - State.declare ~name:"coq-elpi:clauses_for_later" +let clauses_for_later : _ State.component = + State.declare_component ~name:"coq-elpi:clauses_for_later" ~descriptor:interp_state ~init:(fun () -> []) ~start:(fun x -> x) ~pp:(fun fmt l -> List.iter (fun (dbname, code,vars,scope) -> Format.fprintf fmt "db:%s code:%a scope:%a\n" (String.concat "." dbname) - Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l) + Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l) () ;; let term = { diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 7985063b3..a164de375 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -26,10 +26,10 @@ let get_elpi_code_appArg = ref (fun _ -> assert false) let get_ctx, set_ctx, _update_ctx = let bound_vars = - S.declare ~name:"coq-elpi:glob-quotation-bound-vars" + S.declare_component ~name:"coq-elpi:glob-quotation-bound-vars" ~descriptor:interp_state ~init:(fun () -> None) ~pp:(fun fmt -> function Some (x,_) -> () | None -> ()) - ~start:(fun x -> x) + ~start:(fun x -> x) () in S.(get bound_vars, set bound_vars, update bound_vars) @@ -60,9 +60,9 @@ let is_restricted_name = let glob_environment : Environ.env S.component = - S.declare ~name:"coq-elpi:glob-environment" - ~pp:(fun _ _ -> ()) ~init:(fun () -> if !Flags.in_synterp_phase then Environ.empty_env else Global.env ()) - ~start:(fun _ -> if !Flags.in_synterp_phase then Environ.empty_env else Global.env ()) + S.declare_component ~name:"coq-elpi:glob-environment" ~descriptor:interp_state + ~pp:(fun _ _ -> ()) ~init:(fun () -> Global.env ()) + ~start:(fun _ -> Global.env ()) () let push_env state name = let open Context.Rel.Declaration in @@ -401,10 +401,9 @@ let coq_quotation ~depth state loc src = (* Install the quotation *) -let () = Q.set_default_quotation coq_quotation -let () = Q.register_named_quotation ~name:"coq" coq_quotation - -let () = API.Quotation.register_named_quotation ~name:"gref" +let () = Q.set_default_quotation coq_quotation ~descriptor:interp_quotations +let () = Q.register_named_quotation ~name:"coq" coq_quotation ~descriptor:interp_quotations +let () = API.Quotation.register_named_quotation ~name:"gref" ~descriptor:interp_quotations (fun ~depth state _loc src -> let gr = locate_gref src in let state, gr, gls = gref.API.Conversion.embed ~depth state gr in diff --git a/src/coq_elpi_name_quotation.ml b/src/coq_elpi_name_quotation.ml index a1cf1cc01..0cd7d2e09 100644 --- a/src/coq_elpi_name_quotation.ml +++ b/src/coq_elpi_name_quotation.ml @@ -3,6 +3,7 @@ (* ------------------------------------------------------------------------- *) module API = Elpi.API +open Coq_elpi_utils open Coq_elpi_HOAS open Names @@ -11,11 +12,14 @@ let to_name src = else in_elpi_name (Name.Name (Id.of_string src)) (* Install the quotation *) -let () = API.Quotation.register_named_quotation ~name:"name" - (fun ~depth state _loc src -> state, to_name src) -;; +let () = + let f ~depth state _loc src = state, to_name src in + API.Quotation.register_named_quotation ~descriptor:interp_quotations ~name:"name" f; + API.Quotation.register_named_quotation ~descriptor:synterp_quotations ~name:"name" f -let () = API.Quotation.declare_backtick ~name:"Name.t" - (fun state s -> - let src = String.sub s 1 (String.length s - 2) in - state, to_name src) +let () = + let f state s = + let src = String.sub s 1 (String.length s - 2) in + state, to_name src in + API.Quotation.declare_backtick ~descriptor:interp_quotations ~name:"Name.t" f; + API.Quotation.declare_backtick ~descriptor:synterp_quotations ~name:"Name.t" f diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index f2793efb4..2a0b869bb 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -337,7 +337,7 @@ fun ?cwd ~unit:file () -> ;; let init () = - let e = API.Setup.init ~builtins:[coq_builtins;elpi_builtins] ~file_resolver () in + let e = API.Setup.init ~state:interp_state ~hoas:interp_hoas ~quotations:interp_quotations ~builtins:[coq_builtins;elpi_builtins] ~file_resolver () in elpi := Some e; e ;; diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 3a63fc9a4..73961f47c 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -4,6 +4,15 @@ module API = Elpi.API +let synterp_quotations = API.Quotation.new_quotations_descriptor () +let synterp_hoas = API.RawData.new_hoas_descriptor () +let synterp_state = API.State.new_state_descriptor () + +let interp_quotations = API.Quotation.new_quotations_descriptor () +let interp_hoas = API.RawData.new_hoas_descriptor () +let interp_state = API.State.new_state_descriptor () + + let of_coq_loc l = { API.Ast.Loc.source_name = (match l.Loc.fname with Loc.InFile {file} -> file | Loc.ToplevelInput -> "(stdin)"); diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index f2bd1e5dd..03c351e37 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -2,6 +2,13 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) +val synterp_hoas : Elpi.API.Setup.hoas_descriptor +val synterp_quotations : Elpi.API.Setup.quotations_descriptor +val synterp_state : Elpi.API.Setup.state_descriptor + +val interp_hoas : Elpi.API.Setup.hoas_descriptor +val interp_quotations : Elpi.API.Setup.quotations_descriptor +val interp_state : Elpi.API.Setup.state_descriptor val to_coq_loc : Elpi.API.Ast.Loc.t -> Loc.t val of_coq_loc : Loc.t -> Elpi.API.Ast.Loc.t From a0e085173293b9db73e8c7d5b5933c93873104da Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Oct 2023 15:01:44 +0200 Subject: [PATCH 09/12] init 2 runtimes --- coq-builtin-parsing-phase.elpi | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 coq-builtin-parsing-phase.elpi diff --git a/coq-builtin-parsing-phase.elpi b/coq-builtin-parsing-phase.elpi new file mode 100644 index 000000000..f76402e9d --- /dev/null +++ b/coq-builtin-parsing-phase.elpi @@ -0,0 +1,33 @@ + + +% -- Misc --------------------------------------------------------- + +% [coq.info ...] Prints an info message +external type coq.info variadic any prop. + +% [coq.notice ...] Prints a notice message +external type coq.notice variadic any prop. + +% [coq.say ...] Prints a notice message +external type coq.say variadic any prop. + +% [coq.warn ...] Prints a generic warning message +external type coq.warn variadic any prop. + +% [coq.warning Category Name ...] +% Prints a warning message with a Name and Category which can be used +% to silence this warning or turn it into an error. See coqc -w command +% line option +external type coq.warning string -> string -> variadic any prop. + +% [coq.error ...] Prints and *aborts* the program. It is a fatal error for +% Elpi and Ltac +external type coq.error variadic any prop. + +% [coq.version VersionString Major Minor Patch] Fetches the version of Coq, +% as a string and as 3 numbers +external pred coq.version o:string, o:int, o:int, o:int. + + + + From d364a62a6241f9b2fc08ce9f520af46049ec7f6f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Oct 2023 15:29:46 +0100 Subject: [PATCH 10/12] wip --- coq-builtin.elpi | 8 +- src/coq_elpi_builtins.ml | 66 ++++++++------ src/coq_elpi_builtins.mli | 5 +- src/coq_elpi_programs.ml | 170 +++++++++++++++++++++++-------------- src/coq_elpi_programs.mli | 12 +-- src/coq_elpi_vernacular.ml | 18 ++-- 6 files changed, 169 insertions(+), 110 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index fa4f798d4..a6c87febb 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -577,10 +577,6 @@ typeabbrev modpath (ctype "modpath"). typeabbrev modtypath (ctype "modtypath"). -% -- Environment: read ------------------------------------------------ - -% Note: The type [term] is defined in coq-HOAS.elpi - % Result of coq.locate-all kind located type. type loc-gref gref -> located. @@ -601,6 +597,10 @@ external pred coq.locate-all i:id, o:list located. % It's a fatal error if Name cannot be located. external pred coq.locate i:id, o:gref. +% -- Environment: read ------------------------------------------------ + +% Note: The type [term] is defined in coq-HOAS.elpi + % [coq.env.typeof GR Ty] reads the type Ty of a global reference. % Supported attributes: % - @uinstance! I (default: fresh instance I) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 599743b00..9b3f5e779 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1249,13 +1249,8 @@ let eta_contract env sigma t = (*****************************************************************************) (*****************************************************************************) - -let coq_builtins = +let coq_header_builtins = let open API.BuiltIn in - let open Pred in - let open Notation in - let open CConv in - let pp ~depth = P.term depth in [LPCode {|% Coq terms as the object language of elpi and basic API to access Coq % license: GNU Lesser General Public License Version 2.1 or later @@ -1271,6 +1266,7 @@ let coq_builtins = LPCode Coq_elpi_builtins_HOAS.code; MLData Coq_elpi_HOAS.record_field_att; MLData Coq_elpi_HOAS.coercion_status; + LPCode {| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% builtins %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -1280,8 +1276,16 @@ let coq_builtins = % The marker *E* means *experimental*, i.e. use at your own risk, it may change % substantially or even disappear in future versions. |}; + ] - LPDoc "-- Misc ---------------------------------------------------------"; +let coq_misc_builtins = + let open API.BuiltIn in + let open Pred in + let open Notation in + let open CConv in + let pp ~depth = P.term depth in + [ + LPDoc "-- Misc ---------------------------------------------------------"; MLCode(Pred("coq.info", VariadicIn(unit_ctx, !> B.any, "Prints an info message"), @@ -1371,28 +1375,28 @@ line option|}))), let major, minor, patch = coq_version_parser version in !: version +! major +! minor +! patch)), DocAbove); - LPCode {| + ] + +let coq_locate_builtins = + let open API.BuiltIn in + let open Pred in + let open Notation in + [ LPCode {| % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % API for objects belonging to the logic % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%|}; - LPDoc "-- Environment: names -----------------------------------------------"; - LPDoc {|To make the API more precise we use different data types for the names of global objects. + LPDoc "-- Environment: names -----------------------------------------------"; + LPDoc {|To make the API more precise we use different data types for the names of global objects. Note: [ctype \"bla\"] is an opaque data type and by convention it is written [@bla].|}; - - MLData constant; - MLData inductive; - MLData constructor; - MLData gref; - MLData id; - MLData modpath; - MLData modtypath; - ] @ - - [ - LPDoc "-- Environment: read ------------------------------------------------"; - LPDoc "Note: The type [term] is defined in coq-HOAS.elpi"; - - MLData located; + + MLData constant; + MLData inductive; + MLData constructor; + MLData gref; + MLData id; + MLData modpath; + MLData modtypath; + MLData located; MLCode(Pred("coq.locate-all", In(id, "Name", @@ -1430,7 +1434,17 @@ eg "lib:core.bool.true". It's a fatal error if Name cannot be located.|})), (fun s _ ~depth:_ -> !: (locate_gref s))), DocAbove); - +] + +let coq_rest_builtins = + let open API.BuiltIn in + let open Pred in + let open Notation in + let open CConv in + let pp ~depth = P.term depth in + [ + LPDoc "-- Environment: read ------------------------------------------------"; + LPDoc "Note: The type [term] is defined in coq-HOAS.elpi"; MLCode(Pred("coq.env.typeof", In(gref, "GR", diff --git a/src/coq_elpi_builtins.mli b/src/coq_elpi_builtins.mli index eb717489c..19224676b 100644 --- a/src/coq_elpi_builtins.mli +++ b/src/coq_elpi_builtins.mli @@ -5,7 +5,10 @@ open Elpi.API open Coq_elpi_utils -val coq_builtins : BuiltIn.declaration list +val coq_header_builtins : BuiltIn.declaration list +val coq_misc_builtins : BuiltIn.declaration list +val coq_locate_builtins : BuiltIn.declaration list +val coq_rest_builtins : BuiltIn.declaration list (* Clauses to be added to elpi programs when the execution is over *) diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index 2a0b869bb..0fd512b10 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -239,21 +239,79 @@ type program = { dbs : SLSet.t; } -let program_name : nature SLMap.t ref = - Summary.ref ~stage:Summary.Stage.Synterp ~name:"elpi-programs-synterp" SLMap.empty +module type Stage = sig val stage : Summary.Stage.t val in_stage : string -> string end +module SourcesStorage(S : Stage) = struct + open S let program_src : program SLMap.t ref = - Summary.ref ~name:"elpi-programs" SLMap.empty + Summary.ref ~stage ~name:(in_stage "elpi-programs-src") SLMap.empty -let program_exists name = SLMap.mem name !program_name +let db_name_src : db SLMap.t ref = + Summary.ref ~stage ~name:(in_stage "elpi-db-src") SLMap.empty -let db_name : SLSet.t ref = Summary.ref ~stage:Summary.Stage.Synterp ~name:"elpi-db-synterp" SLSet.empty -let db_name_src : db SLMap.t ref = Summary.ref ~name:"elpi-db" SLMap.empty -let db_exists name = SLSet.mem name !db_name - -(* Setup called *) + (* Setup called *) let elpi = Stdlib.ref None +end + +module Synterp = struct + module S = struct let stage = Summary.Stage.Synterp let in_stage x = x ^ "-synterp" end + open S + include SourcesStorage(S) + + let program_name : nature SLMap.t ref = + Summary.ref ~stage ~name:(in_stage "elpi-programs") SLMap.empty + let program_exists name = SLMap.mem name !program_name + + let get_nature p = + try SLMap.find p !program_name + with Not_found -> + CErrors.user_err + Pp.(str "No Elpi Program named " ++ pr_qualified_name p) + + let in_program_name : qualified_name * nature -> Libobject.obj = + let open Libobject in + declare_object @@ { (superglobal_object_nodischarge "ELPI_synterp" + ~cache:(fun (name,nature) -> + program_name := SLMap.add name nature !program_name) + ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) + with object_stage = Summary.Stage.Synterp } + + let declare_program name nature = + let obj = in_program_name (name,nature) in + Lib.add_leaf obj + + let db_name : SLSet.t ref = Summary.ref ~stage ~name:(in_stage "elpi-dbs") SLSet.empty + let db_exists name = SLSet.mem name !db_name + + + let in_db_name : qualified_name -> Libobject.obj = + let open Libobject in + declare_object @@ { + (superglobal_object_nodischarge "ELPI-DB_synterp" + ~cache:(fun name -> db_name := SLSet.add name !db_name) + ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) + with + object_stage = Summary.Stage.Synterp } + let declare_db program = + ignore @@ Lib.add_leaf (in_db_name program) + + let declare_program (loc,qualid) nature = + if program_exists qualid || db_exists qualid then + CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") + else + declare_program qualid nature + + let declare_db (loc,qualid) = + if program_exists qualid || db_exists qualid then + CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") + else + declare_db qualid + +end +module Interp = SourcesStorage(struct let stage = Summary.Stage.Interp let in_stage x = x ^ "-interp" end) + + let elpi_builtins = API.BuiltIn.declare ~file_name:"elpi-builtin.elpi" @@ -270,10 +328,23 @@ let elpi_builtins = [] ) -let coq_builtins = +let coq_interp_builtins = API.BuiltIn.declare ~file_name:"coq-builtin.elpi" - Coq_elpi_builtins.coq_builtins + begin + Coq_elpi_builtins.coq_header_builtins @ + Coq_elpi_builtins.coq_misc_builtins @ + Coq_elpi_builtins.coq_locate_builtins @ + Coq_elpi_builtins.coq_rest_builtins + end + +let coq_synterp_builtins = + API.BuiltIn.declare + ~file_name:"coq-builtin-parsing-phase.elpi" + begin + Coq_elpi_builtins.coq_misc_builtins + end + let file_resolver = let error_cannot_resolve dp file = @@ -337,8 +408,14 @@ fun ?cwd ~unit:file () -> ;; let init () = - let e = API.Setup.init ~state:interp_state ~hoas:interp_hoas ~quotations:interp_quotations ~builtins:[coq_builtins;elpi_builtins] ~file_resolver () in - elpi := Some e; + let e = API.Setup.init ~state:interp_state ~hoas:interp_hoas ~quotations:interp_quotations ~builtins:[coq_interp_builtins;elpi_builtins] ~file_resolver () in + Interp.elpi := Some e; + e +;; + +let init_synterp () = + let e = API.Setup.init ~state:synterp_state ~hoas:synterp_hoas ~quotations:synterp_quotations ~builtins:[coq_synterp_builtins;elpi_builtins] ~file_resolver () in + Synterp.elpi := Some e; e ;; @@ -346,23 +423,22 @@ let ensure_initialized = let init = lazy (init ()) in fun () -> Lazy.force init ;; +let ensure_initialized_synterp = + let init = lazy (init_synterp ()) in + fun () -> Lazy.force init +;; let document_builtins () = - API.BuiltIn.document_file coq_builtins; + API.BuiltIn.document_file coq_interp_builtins; + API.BuiltIn.document_file coq_synterp_builtins; API.BuiltIn.document_file ~header:"% Generated file, do not edit" elpi_builtins (* We load pervasives and coq-lib once and forall at the beginning *) -let get_nature p = - try SLMap.find p !program_name - with Not_found -> - CErrors.user_err - Pp.(str "No Elpi Program named " ++ pr_qualified_name p) - let get ?(fail_if_not_exists=false) p = let _elpi = ensure_initialized () in - let nature = get_nature p in + let nature = Synterp.get_nature p in try - let { sources_rev; units; dbs } = SLMap.find p !program_src in + let { sources_rev; units; dbs } = SLMap.find p !Interp.program_src in units, dbs, Some nature, Some sources_rev with Not_found -> if fail_if_not_exists then @@ -377,20 +453,12 @@ let code n : Chunk.t Code.t = | None -> CErrors.user_err Pp.(str "Unknown Program " ++ str (show_qualified_name n)) | Some sources -> sources |> Code.map (fun name -> try - let { sources_rev } : db = SLMap.find name !db_name_src in + let { sources_rev } : db = SLMap.find name !Interp.db_name_src in sources_rev with Not_found -> CErrors.user_err Pp.(str "Unknown Db " ++ str (show_qualified_name name))) -let in_program_name : qualified_name * nature -> Libobject.obj = - let open Libobject in - declare_object @@ { (superglobal_object_nodischarge "ELPI_synterp" - ~cache:(fun (name,nature) -> - program_name := SLMap.add name nature !program_name) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) - with object_stage = Summary.Stage.Synterp } - let append_to_prog name src = let units, dbs, _, prog = get name in let units, dbs, prog = @@ -411,15 +479,11 @@ let in_program : qualified_name * src -> Libobject.obj = let open Libobject in declare_object @@ superglobal_object_nodischarge "ELPI" ~cache:(fun (name,src_ast) -> - program_src := - SLMap.add name (append_to_prog name src_ast) !program_src) + Interp.program_src := + SLMap.add name (append_to_prog name src_ast) !Interp.program_src) ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))) -let declare_program name nature = - let obj = in_program_name (name,nature) in - Lib.add_leaf obj - let init_program name u = let obj = in_program (name, u) in Lib.add_leaf obj @@ -432,7 +496,7 @@ let add_to_program name v = let append_to_db name kname c = try - let (db : db) = SLMap.find name !db_name_src in + let (db : db) = SLMap.find name !Interp.db_name_src in if Names.KNset.mem kname db.units then db else { sources_rev = Chunk.snoc c db.sources_rev; units = Names.KNset.add kname db.units } with Not_found -> @@ -452,7 +516,7 @@ type snippet = { let in_db : Names.Id.t -> snippet -> Libobject.obj = let open Libobject in let cache ((_,kn),{ program = name; code = p; _ }) = - db_name_src := SLMap.add name (append_to_db name kn p) !db_name_src in + Interp.db_name_src := SLMap.add name (append_to_db name kn p) !Interp.db_name_src in let import i (_,s as o) = if Int.equal i 1 || s.scope = Coq_elpi_utils.SuperGlobal then cache o in declare_named_object @@ { (default_object "ELPI-DB") with classify_function = (fun { scope; program; _ } -> @@ -470,18 +534,6 @@ let in_db : Names.Id.t -> snippet -> Libobject.obj = else Some o); } -let in_db_name : qualified_name -> Libobject.obj = - let open Libobject in - declare_object @@ { - (superglobal_object_nodischarge "ELPI-DB_synterp" - ~cache:(fun name -> db_name := SLSet.add name !db_name) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) - with - object_stage = Summary.Stage.Synterp } - -let declare_db program = - ignore @@ Lib.add_leaf (in_db_name program) - let accum = ref 0 let add_to_db program code vars scope = ignore @@ Lib.add_leaf @@ -525,24 +577,12 @@ let tactic_init () = | None -> CErrors.user_err Pp.(str "Elpi TacticTemplate was not called") | Some ast -> ast -let declare_program (loc,qualid) nature = - if program_exists qualid || db_exists qualid then - CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") - else - declare_program qualid nature - let init_program (loc,qualid) (init : src) = if Global.sections_are_opened () then CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") else init_program qualid init -let declare_db (loc,qualid) = - if program_exists qualid || db_exists qualid then - CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") - else - declare_db qualid - let init_db (loc,qualid) (init : cunit) = if Global.sections_are_opened () then CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") @@ -597,12 +637,12 @@ let printer () = | Some l -> snd l let accumulate p (v : src list) = - if not (program_exists p) then + if not (Synterp.program_exists p) then CErrors.user_err Pp.(str "No Elpi Program named " ++ pr_qualified_name p); v |> List.iter (add_to_program p) let accumulate_to_db p v vs ~scope = - if not (db_exists p) then + if not (Synterp.db_exists p) then CErrors.user_err Pp.(str "No Elpi Db " ++ pr_qualified_name p); add_to_db p v vs scope diff --git a/src/coq_elpi_programs.mli b/src/coq_elpi_programs.mli index 733c731b9..8f9b0b8f5 100644 --- a/src/coq_elpi_programs.mli +++ b/src/coq_elpi_programs.mli @@ -23,12 +23,15 @@ and src_string = { } type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } -val get_nature : qualified_name -> nature - -val declare_program : program_name -> nature -> unit +module Synterp : sig + val db_exists : qualified_name -> bool + val declare_db : program_name -> unit + val declare_program : program_name -> nature -> unit + val get_nature : qualified_name -> nature +end + val init_program : program_name -> src -> unit -val declare_db : program_name -> unit val init_db : program_name -> cunit -> unit val set_current_program : qualified_name -> unit @@ -44,7 +47,6 @@ val load_command : string -> unit val load_tactic : string -> unit val document_builtins : unit -> unit val ensure_initialized : unit -> Setup.elpi -val db_exists : qualified_name -> bool val checker : unit -> Compile.compilation_unit list val printer : unit -> Compile.compilation_unit val tactic_init : unit -> src diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index a270ea123..c7767f86f 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -23,14 +23,14 @@ let document_builtins = document_builtins module Synterp = struct let create_command ?(raw_args=false) n = - declare_program n (Command { raw_args }) + Synterp.declare_program n (Command { raw_args }) let create_tactic n = - declare_program n Tactic + Synterp.declare_program n Tactic let create_program ?(raw_args=false) n = - declare_program n (Program { raw_args }) + Synterp.declare_program n (Program { raw_args }) - let create_db n = declare_db n + let create_db n = Synterp.declare_db n end let create_command n = @@ -152,7 +152,7 @@ let get_and_compile name = programs_tip := SLMap.add name new_hash !programs_tip; let prog = recache_code 0 old_hash new_hash prog src in let raw_args = - match get_nature name with + match Coq_elpi_programs.Synterp.get_nature name with | Command { raw_args } -> raw_args | Program { raw_args } -> raw_args | Tactic -> true in @@ -450,7 +450,7 @@ let accumulate_files ?(program=current_program()) s = let accumulate_string ?(program=current_program()) (loc,s) = let elpi = ensure_initialized () in let new_ast = unit_from_string ~elpi loc s in - if db_exists program then + if Coq_elpi_programs.Synterp.db_exists program then accumulate_to_db program [new_ast] [] ~scope:Coq_elpi_utils.Regular else accumulate program [EmbeddedString { sloc = loc; sdata = s; sast = new_ast}] @@ -458,14 +458,14 @@ let accumulate_string ?(program=current_program()) (loc,s) = let accumulate_db ?(program=current_program()) name = let _ = ensure_initialized () in - if db_exists name then accumulate program [Database name] + if Coq_elpi_programs.Synterp.db_exists name then accumulate program [Database name] else CErrors.user_err Pp.(str "Db " ++ pr_qualified_name name ++ str" not found") let accumulate_to_db db (loc,s) = let elpi = ensure_initialized () in let new_ast = unit_from_string ~elpi loc s in - if db_exists db then accumulate_to_db db [new_ast] + if Coq_elpi_programs.Synterp.db_exists db then accumulate_to_db db [new_ast] else CErrors.user_err Pp.(str "Db " ++ pr_qualified_name db ++ str" not found") @@ -526,7 +526,7 @@ let in_exported_program : nature * qualified_name * string * synterp_code -> Lib let export_command p synterp_code = let p_str = String.concat "." p in - let nature = get_nature p in + let nature = Coq_elpi_programs.Synterp.get_nature p in Lib.add_leaf (in_exported_program (nature,p,p_str,synterp_code)) let skip ~atts:(skip,only) f x = From a939d7d60de2cc6e123ad9dd84c333176dbbdc49 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Oct 2023 16:34:12 +0100 Subject: [PATCH 11/12] wip --- src/coq_elpi_programs.ml | 623 +++++++++++++++++++++----------------- src/coq_elpi_programs.mli | 71 +++-- 2 files changed, 380 insertions(+), 314 deletions(-) diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index 0fd512b10..72b38105f 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -231,6 +231,15 @@ type db = { type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } let current_program = Summary.ref ~name:"elpi-cur-program-name" None +let set_current_program n = + current_program := Some n + +let current_program () = + match !current_program with + | None -> CErrors.user_err Pp.(str "No current Elpi Program") + | Some x -> x + + type program = { @@ -239,78 +248,14 @@ type program = { dbs : SLSet.t; } -module type Stage = sig val stage : Summary.Stage.t val in_stage : string -> string end -module SourcesStorage(S : Stage) = struct - open S - -let program_src : program SLMap.t ref = - Summary.ref ~stage ~name:(in_stage "elpi-programs-src") SLMap.empty - -let db_name_src : db SLMap.t ref = - Summary.ref ~stage ~name:(in_stage "elpi-db-src") SLMap.empty - - (* Setup called *) -let elpi = Stdlib.ref None - -end - -module Synterp = struct - module S = struct let stage = Summary.Stage.Synterp let in_stage x = x ^ "-synterp" end - open S - include SourcesStorage(S) - - let program_name : nature SLMap.t ref = - Summary.ref ~stage ~name:(in_stage "elpi-programs") SLMap.empty - let program_exists name = SLMap.mem name !program_name - - let get_nature p = - try SLMap.find p !program_name - with Not_found -> - CErrors.user_err - Pp.(str "No Elpi Program named " ++ pr_qualified_name p) - - let in_program_name : qualified_name * nature -> Libobject.obj = - let open Libobject in - declare_object @@ { (superglobal_object_nodischarge "ELPI_synterp" - ~cache:(fun (name,nature) -> - program_name := SLMap.add name nature !program_name) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) - with object_stage = Summary.Stage.Synterp } - - let declare_program name nature = - let obj = in_program_name (name,nature) in - Lib.add_leaf obj - - let db_name : SLSet.t ref = Summary.ref ~stage ~name:(in_stage "elpi-dbs") SLSet.empty - let db_exists name = SLSet.mem name !db_name - - - let in_db_name : qualified_name -> Libobject.obj = - let open Libobject in - declare_object @@ { - (superglobal_object_nodischarge "ELPI-DB_synterp" - ~cache:(fun name -> db_name := SLSet.add name !db_name) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) - with - object_stage = Summary.Stage.Synterp } - let declare_db program = - ignore @@ Lib.add_leaf (in_db_name program) - - let declare_program (loc,qualid) nature = - if program_exists qualid || db_exists qualid then - CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") - else - declare_program qualid nature - - let declare_db (loc,qualid) = - if program_exists qualid || db_exists qualid then - CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") - else - declare_db qualid - -end -module Interp = SourcesStorage(struct let stage = Summary.Stage.Interp let in_stage x = x ^ "-interp" end) +type snippet = { + program : qualified_name; + code :cunit list; + scope : Coq_elpi_utils.clause_scope; + vars : Names.Id.t list; +} +(**********************************************************************) let elpi_builtins = API.BuiltIn.declare @@ -407,38 +352,62 @@ fun ?cwd ~unit:file () -> else legacy_resolver ?cwd ~unit:file () ;; -let init () = - let e = API.Setup.init ~state:interp_state ~hoas:interp_hoas ~quotations:interp_quotations ~builtins:[coq_interp_builtins;elpi_builtins] ~file_resolver () in - Interp.elpi := Some e; - e -;; +module type Programs = sig -let init_synterp () = - let e = API.Setup.init ~state:synterp_state ~hoas:synterp_hoas ~quotations:synterp_quotations ~builtins:[coq_synterp_builtins;elpi_builtins] ~file_resolver () in - Synterp.elpi := Some e; - e -;; + val db_exists : qualified_name -> bool + val program_exists : qualified_name -> bool + val declare_db : program_name -> unit + val declare_program : program_name -> nature -> unit + val get_nature : qualified_name -> nature + + val init_program : program_name -> src -> unit + val init_db : program_name -> cunit -> unit + + val accumulate : qualified_name -> src list -> unit + val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit + val load_checker : string -> unit + val load_printer : string -> unit + val load_command : string -> unit + val load_tactic : string -> unit + + val ensure_initialized : unit -> API.Setup.elpi + + val checker : unit -> API.Compile.compilation_unit list + val printer : unit -> API.Compile.compilation_unit + val tactic_init : unit -> src + val command_init : unit -> src + + val code : qualified_name -> Chunk.t Code.t + +end + + +module type Stage = sig + val stage : Summary.Stage.t + val in_stage : string -> string + val init : unit -> API.Setup.elpi +end +module SourcesStorage(S : Stage) = struct + open S + +let program_src : program SLMap.t ref = + Summary.ref ~stage ~name:(in_stage "elpi-programs-src") SLMap.empty + +let db_name_src : db SLMap.t ref = + Summary.ref ~stage ~name:(in_stage "elpi-db-src") SLMap.empty + + (* Setup called *) +let elpi = Stdlib.ref None let ensure_initialized = - let init = lazy (init ()) in - fun () -> Lazy.force init -;; -let ensure_initialized_synterp = - let init = lazy (init_synterp ()) in + let init = lazy (let e = S.init () in elpi := Some e; e) in fun () -> Lazy.force init -;; -let document_builtins () = - API.BuiltIn.document_file coq_interp_builtins; - API.BuiltIn.document_file coq_synterp_builtins; - API.BuiltIn.document_file ~header:"% Generated file, do not edit" elpi_builtins - -(* We load pervasives and coq-lib once and forall at the beginning *) -let get ?(fail_if_not_exists=false) p = +let get get_nature ?(fail_if_not_exists=false) p = let _elpi = ensure_initialized () in - let nature = Synterp.get_nature p in + let nature = get_nature p in try - let { sources_rev; units; dbs } = SLMap.find p !Interp.program_src in + let { sources_rev; units; dbs } = SLMap.find p !program_src in units, dbs, Some nature, Some sources_rev with Not_found -> if fail_if_not_exists then @@ -447,204 +416,284 @@ let get ?(fail_if_not_exists=false) p = else Names.KNset.empty, SLSet.empty, None, None -let code n : Chunk.t Code.t = - let _,_,_,sources = get n in - match sources with - | None -> CErrors.user_err Pp.(str "Unknown Program " ++ str (show_qualified_name n)) - | Some sources -> sources |> Code.map (fun name -> - try - let { sources_rev } : db = SLMap.find name !Interp.db_name_src in - sources_rev - with - Not_found -> - CErrors.user_err Pp.(str "Unknown Db " ++ str (show_qualified_name name))) - -let append_to_prog name src = - let units, dbs, _, prog = get name in - let units, dbs, prog = - match src with - (* undup *) - | File { fast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog - | EmbeddedString { sast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog - | Database n when SLSet.mem n dbs -> units, dbs, prog - (* add *) - | File { fast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog) - | EmbeddedString { sast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog) - | Database n -> units, SLSet.add n dbs, Some (Code.snoc_db_opt n prog) - in - let prog = Option.get prog in - { units; dbs; sources_rev = prog } - -let in_program : qualified_name * src -> Libobject.obj = - let open Libobject in - declare_object @@ superglobal_object_nodischarge "ELPI" - ~cache:(fun (name,src_ast) -> - Interp.program_src := - SLMap.add name (append_to_prog name src_ast) !Interp.program_src) - ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))) - - -let init_program name u = - let obj = in_program (name, u) in - Lib.add_leaf obj -;; - -let add_to_program name v = - let obj = in_program (name, v) in - Lib.add_leaf obj -;; - -let append_to_db name kname c = - try - let (db : db) = SLMap.find name !Interp.db_name_src in - if Names.KNset.mem kname db.units then db - else { sources_rev = Chunk.snoc c db.sources_rev; units = Names.KNset.add kname db.units } - with Not_found -> - match c with - | [] -> assert false - | [base] -> - { sources_rev = Chunk.Base { hash = hash_cunit base; base }; units = Names.KNset.singleton kname } - | _ -> assert false - -type snippet = { - program : qualified_name; - code :cunit list; - scope : Coq_elpi_utils.clause_scope; - vars : Names.Id.t list; -} + let append_to_prog get_nature name src = + let units, dbs, _, prog = get get_nature name in + let units, dbs, prog = + match src with + (* undup *) + | File { fast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog + | EmbeddedString { sast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog + | Database n when SLSet.mem n dbs -> units, dbs, prog + (* add *) + | File { fast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog) + | EmbeddedString { sast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog) + | Database n -> units, SLSet.add n dbs, Some (Code.snoc_db_opt n prog) + in + let prog = Option.get prog in + { units; dbs; sources_rev = prog } + + let in_program get_nature : qualified_name * src -> Libobject.obj = + let open Libobject in + declare_object @@ superglobal_object_nodischarge (in_stage "ELPI") + ~cache:(fun (name,src_ast) -> + program_src := + SLMap.add name (append_to_prog get_nature name src_ast) !program_src) + ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"))) + + + let init_program get_nature name u = + let obj = in_program get_nature (name, u) in + Lib.add_leaf obj + ;; + + let add_to_program get_nature name v = + let obj = in_program get_nature (name, v) in + Lib.add_leaf obj -let in_db : Names.Id.t -> snippet -> Libobject.obj = - let open Libobject in - let cache ((_,kn),{ program = name; code = p; _ }) = - Interp.db_name_src := SLMap.add name (append_to_db name kn p) !Interp.db_name_src in - let import i (_,s as o) = if Int.equal i 1 || s.scope = Coq_elpi_utils.SuperGlobal then cache o in - declare_named_object @@ { (default_object "ELPI-DB") with - classify_function = (fun { scope; program; _ } -> - match scope with - | Coq_elpi_utils.Local -> Dispose - | Coq_elpi_utils.Regular -> Substitute - | Coq_elpi_utils.Global -> Keep - | Coq_elpi_utils.SuperGlobal -> Keep); - load_function = import; - cache_function = cache; - subst_function = (fun (_,o) -> o); - open_function = simple_open import; - discharge_function = (fun (({ scope; program; vars; } as o)) -> - if scope = Coq_elpi_utils.Local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None - else Some o); - } + let code get_nature n : Chunk.t Code.t = + let _,_,_,sources = get get_nature n in + match sources with + | None -> CErrors.user_err Pp.(str "Unknown Program " ++ str (show_qualified_name n)) + | Some sources -> sources |> Code.map (fun name -> + try + let { sources_rev } : db = SLMap.find name !db_name_src in + sources_rev + with + Not_found -> + CErrors.user_err Pp.(str "Unknown Db " ++ str (show_qualified_name name))) + + let append_to_db name kname c = + try + let (db : db) = SLMap.find name !db_name_src in + if Names.KNset.mem kname db.units then db + else { sources_rev = Chunk.snoc c db.sources_rev; units = Names.KNset.add kname db.units } + with Not_found -> + match c with + | [] -> assert false + | [base] -> + { sources_rev = Chunk.Base { hash = hash_cunit base; base }; units = Names.KNset.singleton kname } + | _ -> assert false + + let in_db : Names.Id.t -> snippet -> Libobject.obj = + let open Libobject in + let cache ((_,kn),{ program = name; code = p; _ }) = + db_name_src := SLMap.add name (append_to_db name kn p) !db_name_src in + let import i (_,s as o) = if Int.equal i 1 || s.scope = Coq_elpi_utils.SuperGlobal then cache o in + declare_named_object @@ { (default_object (in_stage "ELPI-DB")) with + classify_function = (fun { scope; program; _ } -> + match scope with + | Coq_elpi_utils.Local -> Dispose + | Coq_elpi_utils.Regular -> Substitute + | Coq_elpi_utils.Global -> Keep + | Coq_elpi_utils.SuperGlobal -> Keep); + load_function = import; + cache_function = cache; + subst_function = (fun (_,o) -> o); + open_function = simple_open import; + discharge_function = (fun (({ scope; program; vars; } as o)) -> + if scope = Coq_elpi_utils.Local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None + else Some o); + } + + let accum = ref 0 + let add_to_db program code vars scope = + ignore @@ Lib.add_leaf + (in_db (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum)) { program; code; scope; vars }) + + (* templates *) + let lp_command_ast = Summary.ref ~name:(in_stage "elpi-lp-command") None + let in_lp_command_src : src -> Libobject.obj = + let open Libobject in + declare_object { (default_object (in_stage "ELPI-LP-COMMAND")) with + load_function = (fun _ x -> lp_command_ast := Some x); + } + let load_command s = + let elpi = ensure_initialized () in + let ast = File { + fname = s; + fast = unit_from_file ~elpi s + } in + lp_command_ast := Some ast; + Lib.add_leaf (in_lp_command_src ast) + let command_init () = + match !lp_command_ast with + | None -> CErrors.user_err Pp.(str "Elpi CommandTemplate was not called") + | Some ast -> ast + + let lp_tactic_ast = Summary.ref ~name:(in_stage "elpi-lp-tactic") None + let in_lp_tactic_ast : src -> Libobject.obj = + let open Libobject in + declare_object { (default_object (in_stage "ELPI-LP-TACTIC")) with + load_function = (fun _ x -> lp_tactic_ast := Some x); + } + let load_tactic s = + let elpi = ensure_initialized () in + let ast = File { + fname = s; + fast = unit_from_file ~elpi s + } in + lp_tactic_ast := Some ast; + Lib.add_leaf (in_lp_tactic_ast ast) + let tactic_init () = + match !lp_tactic_ast with + | None -> CErrors.user_err Pp.(str "Elpi TacticTemplate was not called") + | Some ast -> ast + + let init_program get_nature (loc,qualid) (init : src) = + if Global.sections_are_opened () then + CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") + else + init_program get_nature qualid init + + let init_db (loc,qualid) (init : cunit) = + if Global.sections_are_opened () then + CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") + else if match Global.current_modpath () with Names.ModPath.MPdot (Names.ModPath.MPfile _,_) -> true | _ -> false then + CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside modules") + else + add_to_db qualid [init] [] Coq_elpi_utils.SuperGlobal + ;; + + let lp_checker_ast = Summary.ref ~name:(in_stage "elpi-lp-checker") None + let in_lp_checker_ast : cunit list -> Libobject.obj = + let open Libobject in + declare_object { (default_object (in_stage "ELPI-LP-CHECKER")) with + load_function = (fun _ x -> lp_checker_ast := Some x); + } + + let load_checker s = + let elpi = ensure_initialized () in + let basic_checker = unit_from_string ~elpi (Elpi.API.Ast.Loc.initial "(elpi-checker)") Elpi.Builtin_checker.code in + let coq_checker = unit_from_file ~elpi s in + let p = [basic_checker;coq_checker] in + Lib.add_leaf (in_lp_checker_ast p) + let checker () = + match !lp_checker_ast with + | None -> CErrors.user_err Pp.(str "Elpi Checker was not called") + | Some l -> List.map snd l + + let lp_printer_ast = Summary.ref ~name:(in_stage "elpi-lp-printer") None + let in_lp_printer_ast : cunit -> Libobject.obj = + let open Libobject in + declare_object { (default_object (in_stage "ELPI-LP-PRINTER")) with + load_function = (fun _ x -> lp_printer_ast := Some x); + } + let load_printer s = + let elpi = ensure_initialized () in + let ast = unit_from_file ~elpi s in + lp_printer_ast := Some ast; + Lib.add_leaf (in_lp_printer_ast ast) + let printer () = + match !lp_printer_ast with + | None -> CErrors.user_err Pp.(str "Elpi Printer was not called") + | Some l -> snd l + + let accumulate get_nature program_exists p (v : src list) = + if not (program_exists p) then + CErrors.user_err Pp.(str "No Elpi Program named " ++ pr_qualified_name p); + v |> List.iter (add_to_program get_nature p) + + let accumulate_to_db db_exists p v vs ~scope = + if not (db_exists p) then + CErrors.user_err Pp.(str "No Elpi Db " ++ pr_qualified_name p); + add_to_db p v vs scope + +end -let accum = ref 0 -let add_to_db program code vars scope = - ignore @@ Lib.add_leaf - (in_db (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum)) { program; code; scope; vars }) +module Synterp : Programs = struct + module S = struct + let stage = Summary.Stage.Synterp + let in_stage x = x ^ "-synterp" + let init () = + API.Setup.init ~state:synterp_state ~hoas:synterp_hoas ~quotations:synterp_quotations ~builtins:[coq_synterp_builtins;elpi_builtins] ~file_resolver () + end + open S + include SourcesStorage(S) -let lp_command_ast = Summary.ref ~name:"elpi-lp-command" None -let in_lp_command_src : src -> Libobject.obj = - let open Libobject in - declare_object { (default_object "ELPI-LP-COMMAND") with - load_function = (fun _ x -> lp_command_ast := Some x); - } -let load_command s = - let elpi = ensure_initialized () in - let ast = File { - fname = s; - fast = unit_from_file ~elpi s - } in - lp_command_ast := Some ast; - Lib.add_leaf (in_lp_command_src ast) -let command_init () = - match !lp_command_ast with - | None -> CErrors.user_err Pp.(str "Elpi CommandTemplate was not called") - | Some ast -> ast - -let lp_tactic_ast = Summary.ref ~name:"elpi-lp-tactic" None -let in_lp_tactic_ast : src -> Libobject.obj = - let open Libobject in - declare_object { (default_object "ELPI-LP-TACTIC") with - load_function = (fun _ x -> lp_tactic_ast := Some x); - } -let load_tactic s = - let elpi = ensure_initialized () in - let ast = File { - fname = s; - fast = unit_from_file ~elpi s - } in - lp_tactic_ast := Some ast; - Lib.add_leaf (in_lp_tactic_ast ast) -let tactic_init () = - match !lp_tactic_ast with - | None -> CErrors.user_err Pp.(str "Elpi TacticTemplate was not called") - | Some ast -> ast - -let init_program (loc,qualid) (init : src) = - if Global.sections_are_opened () then - CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") - else - init_program qualid init + let program_name : nature SLMap.t ref = + Summary.ref ~stage ~name:(in_stage "elpi-programs") SLMap.empty + let program_exists name = SLMap.mem name !program_name + + let get_nature p = + try SLMap.find p !program_name + with Not_found -> + CErrors.user_err + Pp.(str "No Elpi Program named " ++ pr_qualified_name p) + + let in_program_name : qualified_name * nature -> Libobject.obj = + let open Libobject in + declare_object @@ { (superglobal_object_nodischarge "ELPI_synterp" + ~cache:(fun (name,nature) -> + program_name := SLMap.add name nature !program_name) + ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) + with object_stage = Summary.Stage.Synterp } -let init_db (loc,qualid) (init : cunit) = - if Global.sections_are_opened () then - CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections") - else if match Global.current_modpath () with Names.ModPath.MPdot (Names.ModPath.MPfile _,_) -> true | _ -> false then - CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside modules") - else - add_to_db qualid [init] [] Coq_elpi_utils.SuperGlobal -;; + let declare_program name nature = + let obj = in_program_name (name,nature) in + Lib.add_leaf obj + + let db_name : SLSet.t ref = Summary.ref ~stage ~name:(in_stage "elpi-dbs") SLSet.empty + let db_exists name = SLSet.mem name !db_name + -let set_current_program n = - let _ = ensure_initialized () in - current_program := Some n + let in_db_name : qualified_name -> Libobject.obj = + let open Libobject in + declare_object @@ { + (superglobal_object_nodischarge "ELPI-DB_synterp" + ~cache:(fun name -> db_name := SLSet.add name !db_name) + ~subst:(Some (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet")))) + with + object_stage = Summary.Stage.Synterp } + let declare_db program = + ignore @@ Lib.add_leaf (in_db_name program) -let current_program () = - match !current_program with - | None -> CErrors.user_err Pp.(str "No current Elpi Program") - | Some x -> x + let declare_program (loc,qualid) nature = + if program_exists qualid || db_exists qualid then + CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") + else + declare_program qualid nature + + let declare_db (loc,qualid) = + if program_exists qualid || db_exists qualid then + CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists") + else + declare_db qualid + + let get = get get_nature + let init_program = init_program get_nature + let add_to_program = add_to_program get_nature + let code = code get_nature + let accumulate = accumulate get_nature program_exists + let accumulate_to_db = accumulate_to_db db_exists +end +module Interp : Programs = struct + include SourcesStorage(struct + let stage = Summary.Stage.Interp + let in_stage x = x ^ "-interp" + let init () = + API.Setup.init ~state:interp_state ~hoas:interp_hoas ~quotations:interp_quotations ~builtins:[coq_interp_builtins;elpi_builtins] ~file_resolver () + end) + + let get_nature = Synterp.get_nature + let program_exists = Synterp.program_exists + let db_exists = Synterp.db_exists + let declare_program (_,x) n = assert(program_exists x && n = get_nature x) + let declare_db (_,x) = assert(db_exists x) + let get = get get_nature + let init_program = init_program get_nature + let add_to_program = add_to_program get_nature + let code = code get_nature + let accumulate = accumulate get_nature program_exists + let accumulate_to_db = accumulate_to_db db_exists +end -let lp_checker_ast = Summary.ref ~name:"elpi-lp-checker" None -let in_lp_checker_ast : cunit list -> Libobject.obj = - let open Libobject in - declare_object { (default_object "ELPI-LP-CHECKER") with - load_function = (fun _ x -> lp_checker_ast := Some x); - } +let document_builtins () = + API.BuiltIn.document_file coq_interp_builtins; + API.BuiltIn.document_file coq_synterp_builtins; + API.BuiltIn.document_file ~header:"% Generated file, do not edit" elpi_builtins -let load_checker s = - let elpi = ensure_initialized () in - let basic_checker = unit_from_string ~elpi (Elpi.API.Ast.Loc.initial "(elpi-checker)") Elpi.Builtin_checker.code in - let coq_checker = unit_from_file ~elpi s in - let p = [basic_checker;coq_checker] in - Lib.add_leaf (in_lp_checker_ast p) -let checker () = - match !lp_checker_ast with - | None -> CErrors.user_err Pp.(str "Elpi Checker was not called") - | Some l -> List.map snd l - -let lp_printer_ast = Summary.ref ~name:"elpi-lp-printer" None -let in_lp_printer_ast : cunit -> Libobject.obj = - let open Libobject in - declare_object { (default_object "ELPI-LP-PRINTER") with - load_function = (fun _ x -> lp_printer_ast := Some x); - } -let load_printer s = - let elpi = ensure_initialized () in - let ast = unit_from_file ~elpi s in - lp_printer_ast := Some ast; - Lib.add_leaf (in_lp_printer_ast ast) -let printer () = - match !lp_printer_ast with - | None -> CErrors.user_err Pp.(str "Elpi Printer was not called") - | Some l -> snd l - -let accumulate p (v : src list) = - if not (Synterp.program_exists p) then - CErrors.user_err Pp.(str "No Elpi Program named " ++ pr_qualified_name p); - v |> List.iter (add_to_program p) - -let accumulate_to_db p v vs ~scope = - if not (Synterp.db_exists p) then - CErrors.user_err Pp.(str "No Elpi Db " ++ pr_qualified_name p); - add_to_db p v vs scope +(* We load pervasives and coq-lib once and forall at the beginning *) let group_clauses l = let rec aux acc l = @@ -659,7 +708,10 @@ let group_clauses l = in aux [] l +(* TODO :FIXME!!!!*) + let () = Coq_elpi_builtins.set_accumulate_to_db (fun clauses_to_add -> + let open Interp in let elpi = ensure_initialized () in let flags = cc_flags () in let clauses_to_add = clauses_to_add |> group_clauses |> @@ -670,6 +722,7 @@ let () = Coq_elpi_builtins.set_accumulate_to_db (fun clauses_to_add -> accumulate_to_db dbname units vs ~scope)) let () = Coq_elpi_builtins.set_accumulate_text_to_db (fun n txt -> + let open Interp in let elpi = ensure_initialized () in let loc = API.Ast.Loc.initial "(elpi.add_predicate)" in let u = unit_from_string ~elpi loc txt in diff --git a/src/coq_elpi_programs.mli b/src/coq_elpi_programs.mli index 8f9b0b8f5..9af5e7429 100644 --- a/src/coq_elpi_programs.mli +++ b/src/coq_elpi_programs.mli @@ -23,35 +23,9 @@ and src_string = { } type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } -module Synterp : sig - val db_exists : qualified_name -> bool - val declare_db : program_name -> unit - val declare_program : program_name -> nature -> unit - val get_nature : qualified_name -> nature -end - -val init_program : program_name -> src -> unit - -val init_db : program_name -> cunit -> unit - val set_current_program : qualified_name -> unit val current_program : unit -> qualified_name -val accumulate : qualified_name -> src list -> unit -val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit -val group_clauses : - (qualified_name * Ast.program * Names.variable list * clause_scope) list -> - (qualified_name * Ast.program list * Names.variable list * clause_scope) list -val load_checker : string -> unit -val load_printer : string -> unit -val load_command : string -> unit -val load_tactic : string -> unit -val document_builtins : unit -> unit -val ensure_initialized : unit -> Setup.elpi -val checker : unit -> Compile.compilation_unit list -val printer : unit -> Compile.compilation_unit -val tactic_init : unit -> src -val command_init : unit -> src -val combine_hash : int -> int -> int + module Chunk : sig type t = @@ -91,7 +65,8 @@ module Code : sig val snoc_opt : cunit -> 'db t option -> 'db t end -val code : qualified_name -> Chunk.t Code.t +module SLMap : Map.S with type key = qualified_name + val debug_vars : Compile.StrSet.t ref val cc_flags : unit -> Compile.flags val unit_from_file : elpi:Setup.elpi -> string -> cunit @@ -101,4 +76,42 @@ val extend_w_units : base:Compile.program -> Compile.compilation_unit list -> Co val parse_goal : elpi:Setup.elpi -> Ast.Loc.t -> string -> Ast.query val intern_unit : (string option * Compile.compilation_unit * Compile.flags) -> cunit -module SLMap : Map.S with type key = qualified_name +(* runtime *) + +module type Programs = sig + + val db_exists : qualified_name -> bool + val prgroam_exists : qualified_name -> bool + val declare_db : program_name -> unit + val declare_program : program_name -> nature -> unit + val get_nature : qualified_name -> nature + + val init_program : program_name -> src -> unit + val init_db : program_name -> cunit -> unit + + val accumulate : qualified_name -> src list -> unit + val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit + + val load_checker : string -> unit + val load_printer : string -> unit + val load_command : string -> unit + val load_tactic : string -> unit + + val ensure_initialized : unit -> Setup.elpi + + val checker : unit -> Compile.compilation_unit list + val printer : unit -> Compile.compilation_unit + val tactic_init : unit -> src + val command_init : unit -> src + + val code : qualified_name -> Chunk.t Code.t + +end + +module Synterp : Programs +module Interp : Programs + +val group_clauses : + (qualified_name * Ast.program * Names.variable list * clause_scope) list -> + (qualified_name * Ast.program list * Names.variable list * clause_scope) list +val document_builtins : unit -> unit From ab5fdf394d6b8f46caa5d21a349ed991cafd28f9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Nov 2023 12:57:18 +0100 Subject: [PATCH 12/12] fix nix --- .github/workflows/nix-action-coq-8.18.yml | 131 +++++++++++++++++++++- .nix/config.nix | 3 + .nix/coq-nix-toolbox.nix | 2 +- 3 files changed, 134 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.18.yml b/.github/workflows/nix-action-coq-8.18.yml index 2fbc8f05c..1a528864d 100644 --- a/.github/workflows/nix-action-coq-8.18.yml +++ b/.github/workflows/nix-action-coq-8.18.yml @@ -1,6 +1,7 @@ jobs: Verdi: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -65,6 +66,7 @@ jobs: --argstr job "Verdi" addition-chains: needs: + - coq - mathcomp-ssreflect - mathcomp-algebra - mathcomp-fingroup @@ -135,6 +137,7 @@ jobs: --argstr job "addition-chains" autosubst: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -189,10 +192,58 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "autosubst" - coq-elpi: + coq: needs: [] runs-on: ubuntu-latest steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + coq-elpi: + needs: + - coq + runs-on: ubuntu-latest + steps: - name: Determine which commit to initially checkout run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ @@ -242,6 +293,7 @@ jobs: --argstr job "coq-elpi" coquelicot: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -298,6 +350,7 @@ jobs: --argstr job "coquelicot" deriving: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -354,6 +407,7 @@ jobs: --argstr job "deriving" hierarchy-builder: needs: + - coq - coq-elpi runs-on: ubuntu-latest steps: @@ -410,6 +464,7 @@ jobs: --argstr job "hierarchy-builder" mathcomp: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -496,6 +551,7 @@ jobs: --argstr job "mathcomp" mathcomp-algebra: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -562,6 +618,7 @@ jobs: --argstr job "mathcomp-algebra" mathcomp-analysis: needs: + - coq - mathcomp-classical - mathcomp-field - mathcomp-bigenough @@ -633,6 +690,7 @@ jobs: --argstr job "mathcomp-analysis" mathcomp-bigenough: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -689,6 +747,7 @@ jobs: --argstr job "mathcomp-bigenough" mathcomp-character: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -770,7 +829,9 @@ jobs: --argstr job "mathcomp-character" mathcomp-classical: needs: + - coq - mathcomp-algebra + - mathcomp-finmap - hierarchy-builder runs-on: ubuntu-latest steps: @@ -821,6 +882,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" @@ -831,6 +896,7 @@ jobs: --argstr job "mathcomp-classical" mathcomp-field: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -907,6 +973,7 @@ jobs: --argstr job "mathcomp-field" mathcomp-fingroup: needs: + - coq - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -966,8 +1033,66 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" --argstr job "mathcomp-fingroup" + mathcomp-finmap: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-elpi + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepCheck + name: Checking presence of CI target mathcomp-finmap + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.18\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18" + --argstr job "mathcomp-finmap" mathcomp-solvable: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1039,6 +1164,7 @@ jobs: --argstr job "mathcomp-solvable" mathcomp-ssreflect: needs: + - coq - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1095,6 +1221,7 @@ jobs: --argstr job "mathcomp-ssreflect" odd-order: needs: + - coq - mathcomp-character - mathcomp-ssreflect - mathcomp-fingroup @@ -1181,6 +1308,7 @@ jobs: --argstr job "odd-order" reglang: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -1237,6 +1365,7 @@ jobs: --argstr job "reglang" trakt: needs: + - coq - coq-elpi runs-on: ubuntu-latest steps: diff --git a/.nix/config.nix b/.nix/config.nix index 86a920d7e..b9488e1f0 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -18,6 +18,9 @@ mathcomp-analysis.override.version = "hierarchy-builder"; mathcomp-analysis.job = true; + mathcomp-finmap.override.version = "2.0.0"; + mathcomp-finmap.job = true; + mathcomp-classical.override.version = "hierarchy-builder"; mathcomp-classical.job = true; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 8fb619add..5b6bf1f08 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"cef6668e637efb2941cbda0ac0f0a435730fa3c1" +"e7a39f47847edcde691d7bf8f423e4806a1b660f"