Skip to content

Test end-to-end

Test end-to-end #135

Workflow file for this run

name: Test
run-name: Test end-to-end
on:
workflow_dispatch:
push:
branches:
- "main"
pull_request:
branches:
- "main"
concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
jobs:
test:
strategy:
fail-fast: false
matrix:
os:
- ubuntu-latest
- macos-latest
- windows-latest
browser:
- chrome
- firefox
include:
- os: ubuntu-latest
name: Linux
- os: macos-latest
name: macOS
- os: windows-latest
name: Windows
name: ${{ matrix.name }} - ${{ matrix.browser }}
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v4
with:
submodules: true
- uses: leanprover/lean-action@v1
if: matrix.os != 'windows-latest'
with:
lake-package-directory: "demo/server/LeanProject"
use-mathlib-cache: false
auto-config: false
build: false
test: false
lint: false
- name: Install elan (Windows)
if: matrix.os == 'windows-latest'
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
bash elan-init.sh -y
echo "$(realpath ~/.elan/bin)" >> $GITHUB_PATH
shell: bash
- uses: actions/setup-node@v4
- run: npm install
- run: npm run setup_demo
if: matrix.os != 'windows-latest'
# BUG: Somehow `lake` is not found when called through `npm` but it works on its own
- name: Run npm run setup_demo (Windows)
if: matrix.os == 'windows-latest'
run: |
concurrently \"(cd demo && npm install)\" \"npm run build\" -n install,build -c \"bgCyan.bold,bgBlue.bold\"
- name: Run lake build (Windows)
if: matrix.os == 'windows-latest'
run: |
cd demo/server/LeanProject
lake build
shell: bash
- name: Run tests
uses: cypress-io/github-action@v6
with:
start: npm start
wait-on: 'http://localhost:5173'
browser: ${{ matrix.browser }}
# - run: npm audit
# if: matrix.os == 'ubuntu-latest'
# continue-on-error: true