leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

Setup CI mdbook test using very latest build artifacts from lean4 repo #18

Closed lovettchris closed 3 years ago

lovettchris commented 3 years ago

This uses a github action named "action-download-artifact" to download the "Linux release" build artifact from the latest lean4 CI build and sets it as the default elan toolchain and installs mdbook and runs "mdbook test" to verify this latest lean4 build still works with the code snippets in the book.