Skip to content

Commit

Permalink
replace CI to not use docker, to try and fix memory issues
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Oct 23, 2023
1 parent a387be5 commit 96ad956
Showing 1 changed file with 40 additions and 3 deletions.
43 changes: 40 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
on:
push:
pull_request:

jobs:
update_lean_xyz_branch_and_build:
runs-on: ubuntu-latest
name: Update lean-x.y.z branch and build project
name: Build project
steps:

- name: checkout project
Expand All @@ -16,5 +17,41 @@ jobs:
if: github.ref == 'refs/heads/master'
uses: leanprover-contrib/update-versions-action@master

- name: build project
uses: leanprover-contrib/lean-build-action@master
- name: Install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: install Python
uses: actions/setup-python@v1
with:
python-version: 3.8

- name: Install leanproject
run: |
python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools
- name: Set up olean cache
uses: actions/cache@v3
with:
path: _cache
key: oleans

- name: Configure
run: |
leanpkg configure
leanproject get-mathlib-cache
leanproject get-cache --fallback=download-first || true
- name: Build
run: |
lean --json --make src | python3 _target/deps/mathlib/scripts/detect_errors.py
- name: Save olean cache
run: |
leanproject mk-cache

0 comments on commit 96ad956

Please sign in to comment.