diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml new file mode 100644 index 0000000..49c2849 --- /dev/null +++ b/.github/workflows/functional_tests.yml @@ -0,0 +1,56 @@ +name: Functional Tests + +on: + pull_request: + branches: [main] + paths: + - "scripts/**" + - "action.yml" + - ".github/workflows/functional_tests.yml" + workflow_dispatch: + +jobs: + no-lake-test: + runs-on: ubuntu-latest + strategy: + matrix: + # run with and without `lake test' + lake-test: ["true", "false"] + # run for standalone package and one which depends on mathlib + lake-init-command: ["init standalone", "init mathdep math"] + steps: + # TODO: once `lean-action` supports just setup use it here + - name: install elan + run: | + 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 leanprover/lean4:v4.8.0-rc1 + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + + - uses: actions/checkout@v4 + + - name: create standalone project + run: | + lake ${{ matrix.lake-init-command }} + ls + + - name: create dummy test + if: ${{ matrix.lake-test == 'true' }} + run: | + { + echo "@[test_runner]" + echo "script dummy_test do" + echo " println! \"Running fake tests...\"" + echo " println! \"Fake tests passed!\"" + echo " return 0" + } >> lakefile.lean + + - name: ls and pwd + run: | + ls + pwd + + - name: "run `lean-action` with on `lake ${{matrix.lake-init-command}}` with test: ${{ matrix.lake-test }}" + uses: ./ + with: + test: ${{ matrix.lake-test }}