feat: use lake-manifest.json instead of lake file to detect mathlib d…

…ependency

scripts/detect_mathlib.sh

@@ -4,18 +4,11 @@
 echo "::group::Detect Mathlib Output"
 echo "Trying to detect if project is downstream of Mathlib."
 
-# define mathlib dependency patterns for lakefile.lean and lakefile.toml
-dot_lean_pattern="require mathlib"
-dot_toml_pattern="\[\[require\]\]\nname = \"mathlib\"\ngit = \"https://github.com/leanprover-community/mathlib4"
-# Check if lakefile.lean or lakefile.toml contain the mathlib dependency pattern
-if [ -f lakefile.lean ] && grep -q "$dot_lean_pattern" lakefile.lean; then
+# Check if lake-manifest.json contain the mathlib dependency pattern
+if [ -f lake-manifest.json ] && grep -q "mathlib" lake-manifest.json; then
   # Set the detected-mathlib variable to true and send it to the GitHub action output to be used in later steps
   echo "detected-mathlib=true" >>"$GITHUB_OUTPUT"
-  echo "Detected Mathlib dependency in lakfefile.lean. Using Mathlib cache."
-elif [ -f lakefile.toml ] && grep -Pzq "$dot_toml_pattern" lakefile.toml; then
-  # Set the detected-mathlib variable to true and send it to the GitHub action output to be used in later steps
-  echo "detected-mathlib=true" >>"$GITHUB_OUTPUT"
-  echo "Detected Mathlib dependency in lakfefile.toml. Using Mathlib cache."
+  echo "Detected Mathlib dependency in lake-manifest.json. Using Mathlib cache."
 else
   echo "detected-mathlib=false" >>"$GITHUB_OUTPUT"
   echo "Project is not downstream of Mathlib. Skipping Mathlib cache."