lean-regex/.github/workflows/ci.yml at 3e43b3312632dbc1ceee0dbe0a249fadcad264df · pandaman64/lean-regex · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
name: continuous integration

on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main

jobs:
    build:
      name: Build
      strategy:
        fail-fast: false
        matrix:
          os:
            # lean-action does not provide lake executable on Windows for some reason
            # - windows-latest
            - ubuntu-latest
            - macos-latest
      runs-on: ${{ matrix.os }}
      steps:
        - uses: actions/checkout@v4
        - name: Build Regex
          uses: leanprover/lean-action@v1
          with:
            build-args: '--wfail'
            lake-package-directory: regex
        - name: Run CorpusTest
          run: |
            cd regex
            time lake exe CorpusTest --verify
            time lake exe CorpusTest --verify --backtracker
            time lake exe CorpusTest --verify --backtracker
            time lake exe CorpusTest --verify
        - name: Build RegexCorrectness
          uses: leanprover/lean-action@v1
          with:
            build-args: '--wfail'
            lake-package-directory: correctness