Skip to content

Commit a3944af

Browse files
YaelDilliesYaelDillies
committed
Workflow changes from Toric
* PRs will now be tested on the blueprint build * Enforce the rule that `LeanCamCombi.Mathlib` only imports files from `LeanCamCombi.Mathlib` and `Mathlib` (and `Batteries`, and...) * Make sure that the style lint checks out the project. I guess we were not linting for style for the past three years. 🙈 * Rearrange build steps so that the master and PR workflows look more alike. * Upgrade default elan version and action versions.
1 parent 075f1c4 commit a3944af

File tree

3 files changed

+86
-75
lines changed

3 files changed

+86
-75
lines changed

‎.github/workflows/push_master.yml‎

Lines changed: 46 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -16,49 +16,41 @@ jobs:
1616
name: Lint style
1717
runs-on: ubuntu-latest
1818
steps:
19-
- name: Check for long lines
20-
if: always()
21-
run: |
22-
! (find LeanCamCombi -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
19+
- name: Checkout project
20+
uses: actions/checkout@v4
21+
with:
22+
fetch-depth: 0
2323

2424
- name: Don't 'import Mathlib', use precise imports
2525
if: always()
2626
run: |
2727
! (find LeanCamCombi -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
2828
29+
- name: Files in LeanCamCombi.Mathlib can't import LeanCamCombi files outside LeanCamCombi.Mathlib
30+
run: |
31+
! (find LeanCamCombi/Mathlib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import LeanCamCombi.(?!Mathlib)')
32+
2933
build_project:
3034
runs-on: ubuntu-latest
3135
name: Build project
3236
steps:
33-
- name: Checkout project
34-
uses: actions/checkout@v4
3537

36-
- name: Copy README.md to website/index.md
37-
run: cp README.md website/index.md
38+
# The following actions make sure the project builds properly.
3839

39-
- name: Check LeanCamCombi.Mathlib only imports from Mathlib or LeanCamCombi.Mathlib
40-
run: python3 scripts/check_mathlib_imports.py
41-
42-
- name: Upstreaming dashboard
43-
run: |
44-
mkdir -p website/_includes
45-
python3 scripts/upstreaming_dashboard.py
40+
- name: Checkout project
41+
uses: actions/checkout@v4
42+
with:
43+
fetch-depth: 0
4644

4745
- name: Install elan
48-
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.15.0
46+
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.18.0
4947

5048
- name: Get cache
5149
run: ~/.elan/bin/lake exe cache get || true
5250

5351
- name: Build project
5452
run: ~/.elan/bin/lake build LeanCamCombi
5553

56-
- name: File dependencies
57-
run: |
58-
sudo apt-get update
59-
sudo apt install graphviz -y
60-
~/.elan/bin/lake exe graph website/file_deps.pdf
61-
6254
- name: Cache documentation
6355
uses: actions/cache@v4
6456
with:
@@ -69,25 +61,47 @@ jobs:
6961
- name: Build documentation
7062
run: scripts/build_docs.sh
7163

72-
# - name: Build blueprint and copy to `website/blueprint`
64+
# - name: Build blueprint
7365
# uses: xu-cheng/texlive-action@v2
7466
# with:
75-
# scheme: full
67+
# docker_image: ghcr.io/xu-cheng/texlive-full:20231201
7668
# run: |
69+
# # Install necessary dependencies and build the blueprint
7770
# apk update
7871
# apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
7972
# git config --global --add safe.directory $GITHUB_WORKSPACE
8073
# git config --global --add safe.directory `pwd`
81-
# python3 -m pip install --upgrade pip requests wheel
82-
# python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
83-
# pip install -r blueprint/requirements.txt
84-
# python3 -m pip install invoke
85-
# inv all
74+
# python3 -m venv env
75+
# source env/bin/activate
76+
# pip install --upgrade pip requests wheel
77+
# pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
78+
# pip install leanblueprint
79+
# leanblueprint pdf
80+
# leanblueprint web
81+
82+
# The following actions create and deploy the website.
83+
84+
- name: Copy documentation to website/docs
85+
run: mv docs/build/* website/docs
8686

87-
- name: Copy documentation to `website/docs`
87+
# - name: Copy blueprint to website/blueprint
88+
# run: |
89+
# cp blueprint/print/print.pdf website/blueprint.pdf
90+
# cp -r blueprint/web website/blueprint
91+
92+
- name: Copy README.md to website/index.md
93+
run: cp README.md website/index.md
94+
95+
- name: Upstreaming dashboard
8896
run: |
89-
mkdir -p website/docs
90-
mv docs/build website/docs
97+
mkdir -p website/_includes
98+
python3 scripts/upstreaming_dashboard.py
99+
100+
- name: File dependencies
101+
run: |
102+
sudo apt-get update
103+
sudo apt install graphviz -y
104+
~/.elan/bin/lake exe graph website/file_deps.pdf
91105
92106
- name: Bundle dependencies
93107
uses: ruby/setup-ruby@v1
@@ -108,8 +122,3 @@ jobs:
108122
- name: Deploy to GitHub Pages
109123
id: deployment
110124
uses: actions/deploy-pages@v4
111-
112-
- name: Make sure the cache works
113-
run: |
114-
mkdir -p docbuild/.lake/build/doc
115-
mv website/docs docbuild/.lake/build/doc

‎.github/workflows/push_pr.yml‎

Lines changed: 40 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
on:
2-
pull_request:
32
push:
43
branches-ignore:
54
- master
@@ -9,15 +8,19 @@ jobs:
98
name: Lint style
109
runs-on: ubuntu-latest
1110
steps:
12-
- name: Check for long lines
13-
if: always()
14-
run: |
15-
! (find LeanCamCombi -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
11+
- name: Checkout project
12+
uses: actions/checkout@v4
13+
with:
14+
fetch-depth: 0
1615

1716
- name: Don't 'import Mathlib', use precise imports
1817
if: always()
1918
run: |
20-
! (find LeanCamCombi -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
19+
! (find Toric -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
20+
21+
- name: Files in Toric.Mathlib can't import Toric files outside Toric.Mathlib
22+
run: |
23+
! (find Toric/Mathlib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Toric.(?!Mathlib)')
2124
2225
build_project:
2326
runs-on: ubuntu-latest
@@ -27,15 +30,43 @@ jobs:
2730
cancel-in-progress: true
2831
steps:
2932
- name: Checkout project
30-
uses: actions/checkout@v2
33+
uses: actions/checkout@v4
3134
with:
3235
fetch-depth: 0
3336

3437
- name: Install elan
35-
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
38+
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.18.0
3639

3740
- name: Get cache
3841
run: ~/.elan/bin/lake exe cache get || true
3942

4043
- name: Build project
41-
run: ~/.elan/bin/lake build LeanCamCombi
44+
run: ~/.elan/bin/lake build Toric
45+
46+
# - name: Cache documentation
47+
# uses: actions/cache@v4
48+
# with:
49+
# path: website/docs
50+
# key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
51+
# restore-keys: MathlibDoc-
52+
53+
# - name: Build documentation
54+
# run: scripts/build_docs.sh
55+
56+
# - name: Build blueprint
57+
# uses: xu-cheng/texlive-action@v2
58+
# with:
59+
# docker_image: ghcr.io/xu-cheng/texlive-full:20231201
60+
# run: |
61+
# # Install necessary dependencies and build the blueprint
62+
# apk update
63+
# apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
64+
# git config --global --add safe.directory $GITHUB_WORKSPACE
65+
# git config --global --add safe.directory `pwd`
66+
# python3 -m venv env
67+
# source env/bin/activate
68+
# pip install --upgrade pip requests wheel
69+
# pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
70+
# pip install leanblueprint
71+
# leanblueprint pdf
72+
# leanblueprint web

‎scripts/check_mathlib_imports.py‎

Lines changed: 0 additions & 29 deletions
This file was deleted.

0 commit comments

Comments
 (0)