diff --git a/scripts/detect_mathlib.sh b/scripts/detect_mathlib.sh index c8d3ccf..b598350 100755 --- a/scripts/detect_mathlib.sh +++ b/scripts/detect_mathlib.sh @@ -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 diff --git a/scripts/install_elan.sh b/scripts/install_elan.sh index 4bbebe9..60bfb1c 100755 --- a/scripts/install_elan.sh +++ b/scripts/install_elan.sh @@ -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::"