-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Loading status checks…
Merge pull request #43 from sertel/main
Nix flake suppport and CI
Showing
14 changed files
with
842 additions
and
66 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,27 @@ | ||
| name: Flake build | ||
|
|
||
| # Controls when the action will run. | ||
| on: | ||
| # Triggers the workflow on push or pull request events but only for the main branch | ||
| push: | ||
| branches: [ main ] | ||
| pull_request: | ||
| branches: [ main ] | ||
|
|
||
| # Allows you to run this workflow manually from the Actions tab | ||
| workflow_dispatch: | ||
|
|
||
| jobs: | ||
| # This workflow contains a single job called "build" | ||
| build: | ||
| # The type of runner that the job will run on | ||
| runs-on: ubuntu-latest | ||
|
|
||
| # Steps represent a sequence of tasks that will be executed as part of the job | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| - uses: cachix/install-nix-action@v25 | ||
| with: | ||
| github_access_token: ${{ secrets.GITHUB_TOKEN }} | ||
| - run: nix build | ||
| - run: nix flake check |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,281 @@ | ||
| jobs: | ||
| coq: | ||
| needs: [] | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Determine which commit to initially checkout | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ | ||
| \ }}\" >> $GITHUB_ENV\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.target_commit }} | ||
| - name: Determine which commit to test | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ | ||
| \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ | ||
| \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ | ||
| \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ | ||
| \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ | ||
| \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ | ||
| \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.tested_commit }} | ||
| - name: Cachix install | ||
| uses: cachix/install-nix-action@v20 | ||
| with: | ||
| nix_path: nixpkgs=channel:nixpkgs-unstable | ||
| - name: Cachix setup coq | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - 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 \"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 "8.18" --argstr | ||
| job "coq" | ||
| mathcomp: | ||
| needs: | ||
| - coq | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Determine which commit to initially checkout | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ | ||
| \ }}\" >> $GITHUB_ENV\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.target_commit }} | ||
| - name: Determine which commit to test | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ | ||
| \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ | ||
| \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ | ||
| \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ | ||
| \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ | ||
| \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ | ||
| \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.tested_commit }} | ||
| - name: Cachix install | ||
| uses: cachix/install-nix-action@v20 | ||
| with: | ||
| nix_path: nixpkgs=channel:nixpkgs-unstable | ||
| - name: Cachix setup coq | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - 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 \"8.18\" --argstr job \"mathcomp\" \\\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 "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 "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 "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 "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 "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 "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 "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 "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 "8.18" --argstr | ||
| job "mathcomp" | ||
| mathcomp-analysis: | ||
| needs: | ||
| - coq | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Determine which commit to initially checkout | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ | ||
| \ }}\" >> $GITHUB_ENV\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.target_commit }} | ||
| - name: Determine which commit to test | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ | ||
| \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ | ||
| \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ | ||
| \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ | ||
| \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ | ||
| \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ | ||
| \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.tested_commit }} | ||
| - name: Cachix install | ||
| uses: cachix/install-nix-action@v20 | ||
| with: | ||
| nix_path: nixpkgs=channel:nixpkgs-unstable | ||
| - name: Cachix setup coq | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - 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 \"8.18\" --argstr job \"mathcomp-analysis\" \\\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 "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 "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 "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 "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 "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 "8.18" --argstr | ||
| job "mathcomp-analysis" | ||
| ssprove: | ||
| needs: | ||
| - coq | ||
| - mathcomp-analysis | ||
| 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 | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - id: stepCheck | ||
| name: Checking presence of CI target ssprove | ||
| run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ | ||
| \ bundle \"8.18\" --argstr job \"ssprove\" \\\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 "8.18" --argstr | ||
| job "coq" | ||
| - 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 "8.18" --argstr | ||
| job "equations" | ||
| - 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 "8.18" --argstr | ||
| job "mathcomp-ssreflect" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: 'Building/fetching previous CI target: mathcomp-analysis' | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr | ||
| job "mathcomp-analysis" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: 'Building/fetching previous CI target: extructures' | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr | ||
| job "extructures" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: 'Building/fetching previous CI target: deriving' | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr | ||
| job "deriving" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: Building/fetching current CI target | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr | ||
| job "ssprove" | ||
| name: Nix CI for bundle 8.18 | ||
| 'on': | ||
| pull_request: | ||
| paths: | ||
| - .github/workflows/nix-action-8.18.yml | ||
| pull_request_target: | ||
| paths-ignore: | ||
| - .github/workflows/nix-action-8.18.yml | ||
| types: | ||
| - opened | ||
| - synchronize | ||
| - reopened | ||
| push: | ||
| branches: | ||
| - main | ||
| workflow_dispatch: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,281 @@ | ||
| jobs: | ||
| coq: | ||
| needs: [] | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Determine which commit to initially checkout | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ | ||
| \ }}\" >> $GITHUB_ENV\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.target_commit }} | ||
| - name: Determine which commit to test | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ | ||
| \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ | ||
| \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ | ||
| \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ | ||
| \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ | ||
| \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ | ||
| \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.tested_commit }} | ||
| - name: Cachix install | ||
| uses: cachix/install-nix-action@v20 | ||
| with: | ||
| nix_path: nixpkgs=channel:nixpkgs-unstable | ||
| - name: Cachix setup coq | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - 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 \"8.19\" --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 "8.19" --argstr | ||
| job "coq" | ||
| mathcomp: | ||
| needs: | ||
| - coq | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Determine which commit to initially checkout | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ | ||
| \ }}\" >> $GITHUB_ENV\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.target_commit }} | ||
| - name: Determine which commit to test | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ | ||
| \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ | ||
| \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ | ||
| \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ | ||
| \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ | ||
| \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ | ||
| \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.tested_commit }} | ||
| - name: Cachix install | ||
| uses: cachix/install-nix-action@v20 | ||
| with: | ||
| nix_path: nixpkgs=channel:nixpkgs-unstable | ||
| - name: Cachix setup coq | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - 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 \"8.19\" --argstr job \"mathcomp\" \\\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 "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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --argstr | ||
| job "mathcomp" | ||
| mathcomp-analysis: | ||
| needs: | ||
| - coq | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Determine which commit to initially checkout | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ | ||
| \ }}\" >> $GITHUB_ENV\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.target_commit }} | ||
| - name: Determine which commit to test | ||
| run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ | ||
| \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ | ||
| \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ | ||
| \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ | ||
| \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ | ||
| \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ | ||
| \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ | ||
| \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" | ||
| - name: Git checkout | ||
| uses: actions/checkout@v3 | ||
| with: | ||
| fetch-depth: 0 | ||
| ref: ${{ env.tested_commit }} | ||
| - name: Cachix install | ||
| uses: cachix/install-nix-action@v20 | ||
| with: | ||
| nix_path: nixpkgs=channel:nixpkgs-unstable | ||
| - name: Cachix setup coq | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - 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 \"8.19\" --argstr job \"mathcomp-analysis\" \\\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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --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 "8.19" --argstr | ||
| job "mathcomp-analysis" | ||
| ssprove: | ||
| needs: | ||
| - coq | ||
| - mathcomp-analysis | ||
| 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 | ||
| uses: cachix/cachix-action@v12 | ||
| with: | ||
| extraPullNames: coq-community, math-comp | ||
| name: coq | ||
| - id: stepCheck | ||
| name: Checking presence of CI target ssprove | ||
| run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ | ||
| \ bundle \"8.19\" --argstr job \"ssprove\" \\\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 "8.19" --argstr | ||
| job "coq" | ||
| - 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 "8.19" --argstr | ||
| job "equations" | ||
| - 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 "8.19" --argstr | ||
| job "mathcomp-ssreflect" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: 'Building/fetching previous CI target: mathcomp-analysis' | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr | ||
| job "mathcomp-analysis" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: 'Building/fetching previous CI target: extructures' | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr | ||
| job "extructures" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: 'Building/fetching previous CI target: deriving' | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr | ||
| job "deriving" | ||
| - if: steps.stepCheck.outputs.status == 'built' | ||
| name: Building/fetching current CI target | ||
| run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr | ||
| job "ssprove" | ||
| name: Nix CI for bundle 8.19 | ||
| 'on': | ||
| pull_request: | ||
| paths: | ||
| - .github/workflows/nix-action-8.19.yml | ||
| pull_request_target: | ||
| paths-ignore: | ||
| - .github/workflows/nix-action-8.19.yml | ||
| types: | ||
| - opened | ||
| - synchronize | ||
| - reopened | ||
| push: | ||
| branches: | ||
| - main | ||
| workflow_dispatch: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,81 @@ | ||
| { | ||
| ## DO NOT CHANGE THIS | ||
| format = "1.0.0"; | ||
| ## unless you made an automated or manual update | ||
| ## to another supported format. | ||
|
|
||
| ## The attribute to build from the local sources, | ||
| ## either using nixpkgs data or the overlays located in `.nix/coq-overlays` | ||
| ## Will determine the default main-job of the bundles defined below | ||
| attribute = "ssprove"; | ||
|
|
||
| ## If you want to select a different attribute (to build from the local sources as well) | ||
| ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument | ||
| # shell-attribute = "{{nix_name}}"; | ||
|
|
||
| ## Maybe the shortname of the library is different from | ||
| ## the name of the nixpkgs attribute, if so, set it here: | ||
| # pname = "{{shortname}}"; | ||
|
|
||
| ## Lists the dependencies, phrased in terms of nix attributes. | ||
| ## No need to list Coq, it is already included. | ||
| ## These dependencies will systematically be added to the currently | ||
| ## known dependencies, if any more than Coq. | ||
| ## /!\ Remove this field as soon as the package is available on nixpkgs. | ||
| ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. | ||
| # buildInputs = [ ]; | ||
|
|
||
| ## Indicate the relative location of your _CoqProject | ||
| ## If not specified, it defaults to "_CoqProject" | ||
| # coqproject = "_CoqProject"; | ||
|
|
||
| ## select an entry to build in the following `bundles` set | ||
| ## defaults to "default" | ||
| default-bundle = "8.19"; | ||
|
|
||
| ## write one `bundles.name` attribute set per | ||
| ## alternative configuration | ||
| ## When generating GitHub Action CI, one workflow file | ||
| ## will be created per bundle | ||
|
|
||
| ## It is not possible as of yet to the coq-nix-toolbox to use a | ||
| ## certain version. All jobs only run against the latest version. | ||
| ## To do this check as a CI job you either need to manually edit | ||
| ## the generated workflow or create branch off of version 0.1.0 | ||
| ## and add it there. | ||
| # bundles."8.17".coqPackages = { | ||
| # coq.override.version = "8.17"; | ||
| # mathcomp.override.version = "1.17.0"; | ||
| # mathcomp-analysis.override.version = "0.6.0"; | ||
| # }; | ||
| bundles."8.18".coqPackages = { | ||
| coq.override.version = "8.18"; | ||
| mathcomp.override.version = "2.1.0"; | ||
| mathcomp-analysis.override.version = "1.0.0"; | ||
| }; | ||
| bundles."8.19".coqPackages = { | ||
| coq.override.version = "8.19"; | ||
| mathcomp.override.version = "2.2.0"; | ||
| mathcomp-analysis.override.version = "1.0.0"; | ||
| }; | ||
|
|
||
| ## Cachix caches to use in CI | ||
| ## Below we list some standard ones | ||
| cachix.coq = {}; | ||
| cachix.math-comp = {}; | ||
| cachix.coq-community = {}; | ||
|
|
||
| ## If you have write access to one of these caches you can | ||
| ## provide the auth token or signing key through a secret | ||
| ## variable on GitHub. Then, you should give the variable | ||
| ## name here. For instance, coq-community projects can use | ||
| ## the following line instead of the one above: | ||
| # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN"; | ||
|
|
||
| ## Or if you have a signing key for a given Cachix cache: | ||
| # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY" | ||
|
|
||
| ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY | ||
| ## are the names of secret variables. They are set in | ||
| ## GitHub's web interface. | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| "544d3d77a4a0f4fef30ad7825d2a8d2255abb0e3" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| { | ||
| inputs = { | ||
| nixpkgs.url = github:nixos/nixpkgs; | ||
| flake-utils.url = github:numtide/flake-utils; | ||
|
|
||
| ssprove.url = github:ssprove/ssprove/nix; | ||
| ssprove.inputs.nixpkgs.follows = "nixpkgs"; | ||
| ssprove.inputs.flake-utils.follows = "flake-utils"; | ||
| }; | ||
| outputs = { self, nixpkgs, flake-utils | ||
| , ssprove }: | ||
| flake-utils.lib.eachDefaultSystem (system: | ||
| let | ||
| pkgs = nixpkgs.legacyPackages.${system}; | ||
| in { | ||
| devShell = pkgs.mkShell { | ||
| packages = [ssprove]; | ||
| shellHook = '' alias ll="ls -lasi" ''; | ||
| }; | ||
| } | ||
| ); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,30 @@ | ||
| { | ||
| inputs = { | ||
| nixpkgs.url = github:nixos/nixpkgs; | ||
| flake-utils.url = github:numtide/flake-utils; | ||
|
|
||
| ## We have start using Nix flakes only after version 0.2.0. | ||
| ## Hence, loading versions flake-style works best after | ||
| ## version 0.2.0. | ||
| # ssprove.url = github:ssprove/ssprove/nix; | ||
| # ssprove.inputs.nixpkgs.follows = "nixpkgs"; | ||
| # ssprove.inputs.flake-utils.follows = "flake-utils"; | ||
| }; | ||
| outputs = { self, nixpkgs, flake-utils | ||
| #, ssprove | ||
| }: | ||
| flake-utils.lib.eachDefaultSystem (system: | ||
| let | ||
| pkgs = nixpkgs.legacyPackages.${system}; | ||
| coqPackages = pkgs.coqPackages_8_17.overrideScope | ||
| (self: super:{ | ||
| ssprove = super.ssprove.override { version = "0.1.0"; }; | ||
| }); | ||
| in { | ||
| devShell = pkgs.mkShell { | ||
| packages = (with coqPackages; [ssprove]); | ||
| shellHook = '' alias ll="ls -lasi" ''; | ||
| }; | ||
| } | ||
| ); | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,4 @@ | ||
| fetchTarball { | ||
| url = https://github.com/NixOS/nixpkgs/archive/045a097bde2100af7301e50632a02d0425031042.tar.gz; | ||
| sha256 = "1gw6xkyzhc08q93dkb6p2s0c8b7vhj9nq5amwn5146ag38cp0j3l"; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| { config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, | ||
| update-nixpkgs ? false, ci-matrix ? false, | ||
| override ? {}, ocaml-override ? {}, global-override ? {}, | ||
| bundle ? null, job ? null, inNixShell ? null, src ? ./., | ||
| }@args: | ||
| let auto = fetchGit { | ||
| url = "https://github.com/coq-community/coq-nix-toolbox.git"; | ||
| ref = "master"; | ||
| rev = import .nix/coq-nix-toolbox.nix; | ||
| }; | ||
| in | ||
| import auto ({inherit src;} // args) |
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters