Skip to content

Commit

Permalink
Add a GitHub Action to run lake build and stack build
Browse files Browse the repository at this point in the history
Runs automatically for pull requests to `main` or pushes to `main`.
Uses Nix to obtain the build inputs declared in `flake.nix` (`elan` and `stack`).
Caches Lean toolchain and Lean packages.
  • Loading branch information
Daniel Britten committed Oct 7, 2024
1 parent fdc1049 commit 3110dc9
Showing 1 changed file with 40 additions and 0 deletions.
40 changes: 40 additions & 0 deletions .github/workflows/main.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
name: Build

on:
push:
branches: [ main ]
pull_request:
branches: [ main ]

workflow_dispatch:

jobs:
build:
runs-on: ubuntu-latest

steps:
- uses: actions/[email protected]
- name: The Determinate Nix Installer
uses: DeterminateSystems/nix-installer-action@v14
- name: Magic Nix Cache
uses: DeterminateSystems/magic-nix-cache-action@v8
- name: Cache Lean toolchain
uses: actions/[email protected]
with:
path: ~/.elan/toolchains
key: ${{ runner.os }}-lean-toolchain-${{ hashFiles('lean-toolchain') }}
- name: Cache Lean packages
id: cache-lean-packages
uses: actions/[email protected]
with:
path: .lake/packages
key: ${{ runner.os }}-lean-packages-${{ hashFiles('lake-manifest.json') }}
- name: Retrieve or restore flake.nix build inputs
run: nix develop
- if: ${{ steps.cache-lean-packages.outputs.cache-hit != 'true' }}
name: Get Mathlib cache
run: nix develop --command bash -c "lake exe cache get"
- name: Build vc tool
run: nix develop --command bash -c "cd vc; stack --nix build"
- name: Build Lean files
run: nix develop --command bash -c "lake build"

0 comments on commit 3110dc9

Please sign in to comment.