feat: use lake manifest to determine mathlib dependency (#88)

Add test to verify mathlib dependency was detected on `lake new
mathlibdep math`

Closes #82

.github/functional_tests/auto_config_false/action.yml

@@ -22,6 +22,7 @@ runs:
     - name: create lake package
       run: |
         lake init autoconfigtest
+        lake update
       shell: bash
 
     - name: "run `lean-action` with `auto-config: false`" 

.github/functional_tests/auto_config_true/action.yml

@@ -21,6 +21,7 @@ runs:
     - name: create lake package
       run: |
         lake init autoconfigtest
+        lake update
       shell: bash
 
     - name: create successful dummy test

.github/functional_tests/lake_check_test_failure/action.yml

@@ -20,6 +20,7 @@ runs:
     - name: create lake package
       run: |
         lake init dummytest
+        lake update
       shell: bash
 
     - name: "run `lean-action` with `test: true`" 

.github/functional_tests/lake_init_failure/action.yml

@@ -18,6 +18,7 @@ runs:
     - name: create lake package with `lake init`
       run: |
         lake init failingpackage
+        lake update
       shell: bash
 
     - name: introduce a syntax error in `lakefile.lean`

.github/functional_tests/lake_init_success/action.yml

@@ -21,6 +21,7 @@ runs:
     - name: create lake package with `lake init ${{ inputs.lake-init-arguments }}`
       run: |
         lake init ${{ inputs.lake-init-arguments }}
+        lake update
       shell: bash
 
     - name: "run `lean-action`"

.github/functional_tests/lake_lint_failure/action.yml

@@ -18,6 +18,7 @@ runs:
     - name: create lake package
       run: |
         lake init dummylint
+        lake update
       shell: bash 
 
     - name: create failing dummy lint driver

.github/functional_tests/lake_lint_success/action.yml

@@ -18,6 +18,7 @@ runs:
     - name: create lake package
       run: |
         lake init dummylint
+        lake update
       shell: bash
 
     - name: create successful dummy lint

.github/functional_tests/lake_test_failure/action.yml

@@ -18,6 +18,7 @@ runs:
     - name: create lake package
       run: |
         lake init dummytest
+        lake update
       shell: bash 
 
     - name: create failing dummy test

.github/functional_tests/lake_test_success/action.yml

@@ -18,6 +18,7 @@ runs:
     - name: create lake package
       run: |
         lake init dummytest
+        lake update
       shell: bash
 
     - name: create successful dummy test

.github/functional_tests/mathlib_dependency/action.yml

@@ -0,0 +1,45 @@
+name: 'Mathlib Dependency Test'
+description: 'Run `lean-action` on Lake package generated by `lake init mathlibdep math` and verify that the mathlb dependecy is detected'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
+runs: 
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package with `lake init mathlibdep math`
+      run: |
+        lake init mathlibdep math
+        lake update
+      shell: bash
+
+    - name: "run `lean-action`"
+      id: lean-action
+      uses: ./
+      with:
+        use-github-cache: false
+
+    - name: verify `lake build` success
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+
+    - name: verify lean-action detected mathlib dependecy
+      env:
+        OUTPUT_NAME: "detected-mathlib"
+        EXPECTED_VALUE: "true"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.detected-mathlib }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/functional_tests/subdirectory_lake_package/action.yml

@@ -22,6 +22,7 @@ runs:
         mkdir a_subdirectory
         cd a_subdirectory
         lake init subdirpackage
+        lake update
       shell: bash
 
     - name: "run `lean-action`" 

.github/workflows/functional_tests.yml

@@ -61,6 +61,14 @@ jobs:
       - uses: ./.github/functional_tests/auto_config_false
         with:
           toolchain: ${{ env.toolchain }}
+
+  detect-mathlib:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/mathlib_dependency
+        with:
+          toolchain: ${{ env.toolchain }}
 
   lake-test-success:
     runs-on: ubuntu-latest

action.yml

@@ -100,6 +100,11 @@ outputs:
       The status of the `lake lint` step.
       Allowed values: "SUCCESS" | "FAILURE" | "NOT_RUN".
     value: ${{ steps.set-output-parameters.outputs.lint-status }}
+  detected-mathlib:
+    description: |
+      If lean-action detected a mathlib dependency equals "true"
+      otherwise equals "false".
+    value: ${{ steps.detect-mathlib.outputs.detected-mathlib }}
 
 runs:
   using: "composite"
@@ -122,6 +127,7 @@ runs:
         : Configure Lean Action
         ${{ github.action_path }}/scripts/config.sh
       shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
 
     - uses: actions/cache@v4
       if: ${{ inputs.use-github-cache == 'true' }}
@@ -143,7 +149,7 @@ runs:
 
     - name: get mathlib cache
       # only get the cache if Mathlib was detected by detect-mathlib step or if the user explicitly set mathlib-cache to true
-      if: ${{ steps.detect-mathlib.outputs.DETECTED_MATHLIB == 'true' || inputs.use-mathlib-cache == 'true' }}
+      if: ${{ steps.detect-mathlib.outputs.detected-mathlib == 'true' || inputs.use-mathlib-cache == 'true' }}
       run: |
         : Get Mathlib Cache
         echo "::group::Mathlib Cache"

scripts/config.sh

@@ -7,6 +7,13 @@ echo "::group::Configure lean-action"
 # Get the directory of the script to read the step summaries md files
 SCRIPT_DIR="$(dirname "$(readlink -f "$0")")"
 
+# Verify that a lake-manifest.json exist
+if [ ! -f lake-manifest.json ]; then
+  echo "::error::No lake-manifest.json found. Run lake update to generate manifest"
+  echo "::error::Exiting with status 1"
+  exit 1
+fi
+
 # If the user specifies `build: true`, then run `lake build`.
 if [ "$BUILD" = "true" ]; then
     echo "build: true -> will run lake build"

scripts/detect_mathlib.sh

@@ -4,20 +4,14 @@
 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
-  # 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."
+mathlib_repo_url="https://github.com/leanprover-community/mathlib4"
+# Check if lake-manifest.json contain the mathlib dependency pattern
+if [ -f lake-manifest.json ] && grep -q "$mathlib_repo_url" 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 lake-manifest.json. Using Mathlib cache."
 else
-  echo "DETECTED_MATHLIB=false" >>"$GITHUB_OUTPUT"
+  echo "detected-mathlib=false" >>"$GITHUB_OUTPUT"
   echo "Project is not downstream of Mathlib. Skipping Mathlib cache."
 fi