Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nix flake suppport and CI #43

Merged
merged 35 commits into from
Nov 26, 2024
Merged

Nix flake suppport and CI #43

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
1162f7c
Switching to the existing nix tooling.
sertel Mar 13, 2024
649c250
lib is not available yet.
sertel Mar 13, 2024
dfbc7c0
coqPackages already contains the proper coq version.
sertel Mar 13, 2024
ac20666
for flakes the src of the library must be flake input.
sertel Mar 13, 2024
204f6e9
the unpackPhase needs to be skipped too
sertel Mar 13, 2024
2916ecf
need to set the native build inputs for the shell to work.
sertel Mar 14, 2024
f4da62d
Indeed I do not need the nativeBuildInputs. That was a bug in the fla…
sertel Mar 15, 2024
51c3f2b
still testing
sertel Mar 15, 2024
cbfa5f5
src
sertel Mar 15, 2024
97012d9
no unpacking
sertel Mar 18, 2024
8daeca2
adding Coq itself to the propagated build inputs to hopefully enable …
sertel Mar 18, 2024
0c86617
adding the stdenv version for testing and debugging
sertel Mar 19, 2024
86dd442
no quotes
sertel Mar 20, 2024
51b7d41
the quotes around the path were the problem. now everything is workin…
sertel Mar 20, 2024
bdfd6ce
Merge branch 'SSProve:main' into nix
sertel Apr 11, 2024
8a0d34f
CI setup
sertel Apr 12, 2024
584532c
make the CI jobs manually executable.
sertel Apr 12, 2024
71124b3
fix.
sertel Apr 12, 2024
3ac61c8
forgotten fix.
sertel Apr 12, 2024
98bcf59
jobs generated against the SSProve package in nixpkgs
sertel May 3, 2024
bdc751a
enable workflows for main and manual execution.
sertel May 3, 2024
0e57e1c
use mathcomp-ssreflect as in the CI and run against master because it…
sertel May 3, 2024
6b4cee7
for some reason using ssreflect does not work.
sertel May 3, 2024
1882afa
forcing the job to load the most recent state of nixpkgs
sertel May 3, 2024
ed79bb2
after updating nixpkgs.
sertel May 3, 2024
b9ff63c
flake build
sertel May 4, 2024
c253bf7
fixing flake
sertel May 6, 2024
48e24b3
no cache
sertel May 6, 2024
fb11d22
minor
sertel May 8, 2024
e53690f
discovered and fixed inconsistencies in loading mathcomp dependencies.
sertel May 31, 2024
d52ae4c
documentation of Nix
sertel May 31, 2024
4a59d11
adding a comment on the use of Equations.
sertel Jun 4, 2024
9066771
Typo fix in README.md
sertel Jun 12, 2024
7a717b5
Quick start guide on project setup via Nix
sertel Aug 12, 2024
7366146
Merge branch 'SSProve:main' into main
sertel Nov 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions .github/workflows/flake-build.yml
View file
Open in desktop
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
281 changes: 281 additions & 0 deletions .github/workflows/nix-action-8.18.yml
View file
Open in desktop
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:
Loading
Loading