feat: add support for lean4checker

Add an input and corresponding step for checking the enviornment
with lean4checker.

Note, currently this only works for projects which use toolchain/v4.7.0.

action.yml

@@ -39,6 +39,14 @@ inputs:
       If check-reservoir-elibility input is not provided, the action will not check for reservoir eligibility.
     required: false
     default: "false"
+  lean4checker:
+    description: |
+      Check environment with lean4checker
+      Allowed values: "true" or "false".
+      If lean4checker input is not provided, the action will not check environment with lean4checker.
+    required: false
+    default: "false"
+
 runs:
   using: "composite"
   steps:
@@ -97,3 +105,8 @@ runs:
           "${{ github.event.repository.stargazers_count }}"\
           "${{ github.event.repository.license.spdx_id }}"
       shell: bash
+
+    - name: check environment with lean4checker
+      if: ${{ inputs.lean4checker == 'true' }}
+      run: ${{ github.action_path }}/scripts/run_lean4checker.sh
+      shell: bash

scripts/run_lean4checker.sh

@@ -0,0 +1,19 @@
+echo "Checking environment with lean4checker"
+
+
+# clone lean4checker
+echo "Cloning and building lean4checker"
+git clone https://github.com/leanprover/lean4checker
+cd lean4checker
+git config --global advice.detachedHead false # turn off git warning about detached head
+git checkout toolchain/v4.7.0
+cp ../lean-toolchain .
+
+# build lean4checker and test lean4checker
+lake build
+./test.sh
+cd ..
+
+# run lean4checker
+echo "Running lean4checker"
+lake env lean4checker/.lake/build/bin/lean4checker