lean.py/.github/workflows/ci.yml at main · BasisResearch/lean.py · 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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
name: CI
on: [push, pull_request]

jobs:
  # Run the full test suite on Linux + macOS.
  test:
    strategy:
      fail-fast: false
      matrix:
        os: [ubuntu-latest, macos-latest]
    runs-on: ${{ matrix.os }}
    steps:
      - uses: actions/checkout@v4

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
            -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Install Lean toolchain
        run: |
          elan toolchain install $(cat lean-toolchain)
          elan default $(cat lean-toolchain)

      - name: Install uv
        uses: astral-sh/setup-uv@v5

      - name: Set up Python
        run: uv python install 3.12

      - name: Install Python dependencies
        run: uv sync --dev

      - name: Install demo dependencies (sympy, numpy)
        run: uv pip install sympy numpy

      - name: Build root Lake project
        run: lake build

      - name: Build TestLib (test fixture)
        run: lake build TestLib:shared
        working-directory: tests/lean

      - name: Inspect tests/lean build output (diagnostic)
        if: always()
        run: |
          echo "--- tests/lean/.lake/build ---"
          find tests/lean/.lake/build -maxdepth 5 -type f 2>/dev/null | sort | head -50
          echo "------------------------------"

      - name: Set library path (for downstream commands)
        shell: bash
        run: |
          LEAN_SYSROOT=$(lean --print-prefix)
          if [ "$RUNNER_OS" == "Linux" ]; then
            echo "LD_LIBRARY_PATH=$LEAN_SYSROOT/lib/lean" >> $GITHUB_ENV
          else
            echo "DYLD_LIBRARY_PATH=$LEAN_SYSROOT/lib/lean" >> $GITHUB_ENV
          fi

      - name: Run tests
        run: uv run pytest tests -v

  # macOS-only: run the test suite under `leaks` to check for missing
  # ref-count drops. This is slower so kept on a separate job.
  memory-macos:
    runs-on: macos-latest
    needs: test
    continue-on-error: true   # leaks(1) reports of system frameworks are noisy
    steps:
      - uses: actions/checkout@v4
      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
            -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
      - name: Install Lean toolchain
        run: |
          elan toolchain install $(cat lean-toolchain)
          elan default $(cat lean-toolchain)
      - name: Install uv + deps
        uses: astral-sh/setup-uv@v5
      - run: uv python install 3.12
      - run: uv sync --dev
      - run: uv pip install sympy numpy
      - name: Build
        run: |
          lake build
          (cd tests/lean && lake build)
      - name: leaks(1) check
        run: tests/leaks_check.sh

  # Linux-only: run the test suite with ASAN via LD_PRELOAD.
  # This catches memory errors in our C bridge and ctypes FFI layer
  # without needing to rebuild Lean from source.
  asan-linux:
    runs-on: ubuntu-latest
    needs: test
    continue-on-error: true
    steps:
      - uses: actions/checkout@v4
      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
            -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
      - name: Install Lean toolchain
        run: |
          elan toolchain install $(cat lean-toolchain)
          elan default $(cat lean-toolchain)
      - name: Install uv + deps
        uses: astral-sh/setup-uv@v5
      - run: uv python install 3.12
      - run: uv sync --dev
      - run: uv pip install sympy numpy
      - name: Build
        run: |
          lake build
          (cd tests/lean && lake build)
      - name: Run tests under ASAN (LD_PRELOAD)
        run: |
          LIBASAN=$(gcc -print-file-name=libasan.so)
          echo "Using libasan: $LIBASAN"
          LEAN_SYSROOT=$(lean --print-prefix)
          LD_LIBRARY_PATH="$LEAN_SYSROOT/lib/lean" \
          LD_PRELOAD="$LIBASAN" \
          ASAN_OPTIONS=detect_leaks=0:halt_on_error=1 \
          uv run pytest tests -v --tb=short 2>&1 | tee asan.log
          if grep -q "ERROR: AddressSanitizer" asan.log; then
            echo "::error::ASAN detected memory errors"
            exit 1
          fi

  # Linux-only: run the test suite under valgrind for stronger coverage
  # of definite leaks.
  memory-linux:
    runs-on: ubuntu-latest
    needs: test
    continue-on-error: true   # valgrind under Python interpreter is noisy
    steps:
      - uses: actions/checkout@v4
      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
            -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
      - name: Install Lean toolchain
        run: |
          elan toolchain install $(cat lean-toolchain)
          elan default $(cat lean-toolchain)
      - name: Install valgrind
        run: |
          sudo apt-get update
          sudo apt-get install -y valgrind
      - name: Install uv + deps
        uses: astral-sh/setup-uv@v5
      - run: uv python install 3.12
      - run: uv sync --dev
      - run: uv pip install sympy numpy
      - name: Build
        run: |
          lake build
          (cd tests/lean && lake build)
      - name: valgrind check
        run: tests/leaks_check.sh
        env:
          PYTHONMALLOC: malloc