Use GitHub Actions to check that building succeeds #11
Conversation
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
Coda-Coda
force-pushed
the
build-with-GitHub-Actions
branch
from
7ad842f to
3110dc9
Compare
added 2 commits
October 11, 2024 13:28
The idea is that `elan` should be used to install `lean` rather than directly using Nix, because of issues with packaging `mathlib` such as discussed here: leanprover/lean4#5122.
Runs automatically for pull requests to `main` or pushes to `main`. Uses Nix to obtain the packages declared in `shell.nix` (`elan` and `stack`). Caches Lean toolchain and Lean packages, retrieving Mathlib via `lake exe cache get` if not already in the GitHub Actions cache.
Coda-Coda
force-pushed
the
build-with-GitHub-Actions
branch
from
3110dc9 to
099f6e0
Compare
|
Switched to |
andreiburdusa
approved these changes
Oct 15, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hi, this adds a GitHub Action which runs
lake buildandstack build.It will run automatically for pull requests to
mainor pushes tomain.It uses Nix to obtain the build inputs declared in
flake.nix(currentlyelanandstack).It caches the Lean toolchain and Lean packages (important especially since
mathlibtakes about 1 hour to build through GitHub Actions). It gets Mathlib usinglake exe cache getif there is not GitHub Actions cache hit. [Note: I previously didn't realise getting Mathlib like this was possible, hence the new commit force-pushed].The aim is to just check that
lake buildandstack build(invc) are successful.For this, it also adds a
flake.nixwith adevShellincludingelanandstack. The idea is to useelanto installleanrather than directly using Nix due to complications packagingmathlibin Nix such as discussed in leanprover/lean4#5122 and keeping the setup instructions unchanged.I've experimented with this in the
add-CI-2branch of my fork.This is the first run (7m58s): https://github.com/Coda-Coda/Nethermind-Clear/actions/runs/11208110827.
This is the next run (6m9s), after a minor test edit to
EVMState.leanto test out rebuilding: https://github.com/Coda-Coda/Nethermind-Clear/actions/runs/11208261568.The caching seems to be working as expected, giving a slightly faster build time.
I noticed that there was an old
blank.ymlfile seemingly from a previous approach to using GitHub Actions: https://github.com/NethermindEth/Clear/blob/2ac080b162279dd99813c08ce937dab05cdea3a4/.github/workflows/blank.yml. It may be helpful to add aspects of that in, however this pull request takes a simpler approach. [Note: thelake exe cache getidea was taken fromblank.yml].