From ee1f2b73c157788c9e165c73e74ec0b6c8e69146 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Tue, 10 Sep 2024 11:53:07 +0200 Subject: [PATCH 1/3] Fix for new coq-elpi resolver. --- structures.v => HB/structures.v | 0 Makefile.coq.local | 2 +- _CoqProject | 6 +++--- _CoqProject.test-suite | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) rename structures.v => HB/structures.v (100%) diff --git a/structures.v b/HB/structures.v similarity index 100% rename from structures.v rename to HB/structures.v diff --git a/Makefile.coq.local b/Makefile.coq.local index fdbf8849..564c569b 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -1,5 +1,5 @@ # Coq does not know about Elpi Accumulate File, so we declare the dependency here -structures.vo : $(wildcard HB/*.elpi HB/common/*.elpi) +HB/structures.vo : $(wildcard HB/*.elpi HB/common/*.elpi) clean:: $(SHOW)'CLEAN *.hb *.hb.old' diff --git a/_CoqProject b/_CoqProject index 057e9001..b2e67cab 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,7 +1,7 @@ -structures.v +HB/structures.v -arg -w -arg -elpi.accumulate-syntax -arg -w -arg +elpi.typecheck --Q . HB +-Q HB HB -R tests HB.tests --R examples HB.examples \ No newline at end of file +-R examples HB.examples diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index f59e999a..e24fb2b3 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -100,4 +100,4 @@ tests/saturate_on.v -R tests HB.tests -R examples HB.examples --Q . HB \ No newline at end of file +-Q HB HB From 645b8094aa6ceb360b60201e7289604c43bf51df Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Sep 2024 21:20:33 +0200 Subject: [PATCH 2/3] nix --- .nix/coq-nix-toolbox.nix | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 77c442a5..cbc87f74 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1,2 +1 @@ -"a8ab933c548cf9eac390a5dddaad7cf226758213" - +"85fe71740440d17baca09184b3829ab638a4bfe8" From 045044b7a00aabbc334af80f706abcf4737b6b26 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Sep 2024 13:28:50 +0200 Subject: [PATCH 3/3] nix --- .github/workflows/nix-action-coq-8.19.yml | 57 +++++++++++++++++++++++ .github/workflows/nix-action-coq-8.20.yml | 57 +++++++++++++++++++++++ .nix/coq-nix-toolbox.nix | 2 +- 3 files changed, 115 insertions(+), 1 deletion(-) diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml index 271b3815..7432f4c0 100644 --- a/.github/workflows/nix-action-coq-8.19.yml +++ b/.github/workflows/nix-action-coq-8.19.yml @@ -129,6 +129,63 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" --argstr job "async-test" + autosubst: + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + 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.19\" --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.19" + --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.19" + --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.19" + --argstr job "autosubst" coq: needs: [] runs-on: ubuntu-latest diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index 02bf9deb..e674c58b 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -1,4 +1,61 @@ jobs: + autosubst: + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.target_commit }} + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ + \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ + \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ + \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ + \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + 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.20\" --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.20" + --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.20" + --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.20" + --argstr job "autosubst" coq: needs: [] runs-on: ubuntu-latest diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index cbc87f74..02b5e945 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"85fe71740440d17baca09184b3829ab638a4bfe8" +"b472641a6662a06901b280845b1473e7d6b08ab5"