Skip to content

Commit

Permalink
hack(ci): run lean make twice (#7192)
Browse files Browse the repository at this point in the history
At the moment running `lean --make src` after `leanproject up` will recompile some files.  Merging this PR should have the effect of uploading these newly compiled olean files.

This also makes github actions call `lean --make src` twice to prevent this problem from happening in the first place.
  • Loading branch information
gebner committed Apr 14, 2021
1 parent 6380155 commit b3eabc1
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 1 deletion.
1 change: 1 addition & 0 deletions .github/workflows/build.yml
Expand Up @@ -83,6 +83,7 @@ jobs:
leanpkg configure
echo "::set-output name=started::true"
lean --json -T100000 --make src | python scripts/detect_errors.py
lean --json -T100000 --make src | python scripts/detect_errors.py
- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
Expand Down
3 changes: 2 additions & 1 deletion README.md
Expand Up @@ -6,7 +6,8 @@
[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)

[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter.
It contains both programming infrastructure and mathematics,
as well as tactics that use the former and allow to develop the latter.

## Installation

Expand Down

0 comments on commit b3eabc1

Please sign in to comment.