-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
test: add workflow to run basic functional tests (#35)
Add functional tests: - basic `lake init` - basic `lake init` with basic `lake test` - `lake init` with `math` template - `lake init` with `math` template and basic `lake test`
- Loading branch information
1 parent
94e4fdb
commit 36ca152
Showing
1 changed file
with
56 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 }} |