:sparkles: check mathlib is a dependency, ignore whitespace in file check

oliver-butterley / lean-update

The action attempts to update Lean and Mathlib. If an update is available then the updated version is tested. This allows for automatic committing of the updated project, opening PRs or opening issues.

MIT License

6 stars 2 forks source link

:sparkles: check mathlib is a dependency, ignore whitespace in file check #4

Closed oliver-butterley closed 6 months ago

oliver-butterley commented 6 months ago

Added features:

Check that the lean project has mathlib as a dependency before proceeding.
Check if lean-toolchain or lake-manifest.json have been modified directly, using bash script and without using another action as before.
Check if lean-toolchain or lake-manifest.json now ignores white space differences. (Closes issue #2 )
Updates lean-toolchain directly using curl prior to running lake update. (Closes issue #3 )

oliver-butterley commented 6 months ago

Fixes #3
Fixes #2