don't raise an error if the project don't use mathlib

[Seasawher]

Why is this Action set to error in mathlib-independent repositories?

    - name: Give up if not using mathlib
      if: steps.check-mathlib.outputs.uses_mathlib == 'false'
      run: |
        echo "This action requires the lean project to have mathlib as a dependency." 
        exit 1
      shell: bash

[oliver-butterley]

This is surely not optimal and I'm keen to hear suggestions.

I saw on several places on Zulip that running lake update on lean projects which aren't downstream of mathlib can cause problems. I don't know the precise details. Additionally the use case I had in mind was for people working on projects which use mathlib.

The current implementation is:

• Set the local lean-toolchain by compying the one in use by mathlib: curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
• Then run lake update Mathlib

This seems to work robustly for projects which depend on Mathlib but doesn't make sense for any others.

[Seasawher]

I saw on several places on Zulip that running lake update on lean projects which aren't downstream of mathlib can cause problems. I don't know the precise details. Additionally the use case I had in mind was for people working on projects which use mathlib.

I would like to know more about the details. I want to use the auto-update action for projects that do not depend on mathlib.