Skip to content

Commit

Permalink
feat: add logs of lake and lean version (#24)
Browse files Browse the repository at this point in the history
Elan installation now:
- reports the lake version
- reports the lean version

resolves #12
  • Loading branch information
oliver-butterley authored May 19, 2024
1 parent 0d2b90f commit ae16192
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 0 deletions.
1 change: 1 addition & 0 deletions scripts/detect_mathlib.sh
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ if grep -q "$dot_lean_pattern" lakefile.lean || grep -Pzq "$dot_toml_pattern" la
echo "DETECTED_MATHLIB=true" >> "$GITHUB_OUTPUT"
echo "Project is downstream of Mathlib. Using Mathlib cache."
else
echo "DETECTED_MATHLIB=false" >> "$GITHUB_OUTPUT"
echo "Project is not downstream of Mathlib. Skipping Mathlib cache."
fi

Expand Down
2 changes: 2 additions & 0 deletions scripts/install_elan.sh
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,7 @@ set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
"$HOME"/.elan/bin/lean --version
"$HOME"/.elan/bin/lake --version

echo "::endgroup::"

0 comments on commit ae16192

Please sign in to comment.