File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -35,14 +35,15 @@ jobs:
3535 use-github-cache : false
3636 use-mathlib-cache : true
3737
38- - name : lake build
39- run : |
40- lake build Mathlib Archive Counterexamples
38+ # - name: lake build
39+ # run: |
40+ # lake build Archive Counterexamples
4141
4242 - name : lake shake
4343 id : shake
4444 run : |
45- lake shake --add-public --keep-implied --keep-prefix --fix --explain Mathlib Archive Counterexamples > explain.txt 2>&1
45+ # Add back Archive and Counterexamples when they've been modulized
46+ lake shake --add-public --keep-implied --keep-prefix --fix --explain Mathlib > explain.txt 2>&1
4647 if git diff --quiet; then
4748 echo "changed=false" >> "$GITHUB_OUTPUT"
4849 else
@@ -143,7 +144,7 @@ jobs:
143144 api-key : ${{ secrets.ZULIP_API_KEY }}
144145 email : ' github-mathlib4-bot@leanprover.zulipchat.com'
145146 organization-url : ' https://leanprover.zulipchat.com'
146- to : ' nightly-testing'
147+ to : ' nightly-testing-mathlib '
147148 type : ' stream'
148149 topic : ' Mathlib `shake --fix`'
149150 content : |
You can’t perform that action at this time.
0 commit comments