Skip to content

Commit 211b161

Browse files
RexWzhRexWzh
authored
Merge branch 'leanprover-community:main' into main
2 parents a82e49f + f2f3530 commit 211b161

File tree

28 files changed

+4781
-3008
lines changed

28 files changed

+4781
-3008
lines changed

‎.github/workflows/build.yml‎

Lines changed: 88 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,99 @@
1-
name: Build
2-
run-name: Build the project
1+
name: Build and Test
2+
run-name: Build and Test
33
on:
4+
workflow_dispatch:
45
push:
5-
branches: ["main"]
6+
branches:
7+
- "main"
8+
- "dev"
69
pull_request:
7-
branches: ["main"]
10+
branches:
11+
- "main"
12+
- "dev"
13+
paths:
14+
- ".github/workflows/build.yml"
15+
16+
concurrency:
17+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
18+
cancel-in-progress: true
19+
20+
defaults:
21+
run:
22+
shell: bash
23+
824
jobs:
9-
build:
25+
test:
26+
runs-on: ${{ matrix.os }}
1027
strategy:
1128
fail-fast: false
1229
matrix:
13-
include:
14-
- name: Linux
15-
os: ubuntu-latest
16-
# - name: macOS
17-
# os: macos-latest
18-
# - name: Windows
19-
# os: windows-latest
20-
name: ${{ matrix.name }}
21-
runs-on: ${{ matrix.os }}
30+
os: [ubuntu-latest, macos-latest]
31+
browser: [electron, chrome]
2232
steps:
23-
- uses: actions/checkout@v4
24-
- uses: actions/setup-node@v4
25-
- uses: leanprover/lean-action@v1
33+
- name: Checkout repository
34+
uses: actions/checkout@v4
35+
36+
- name: Setup Node.js
37+
uses: actions/setup-node@v4
38+
with:
39+
node-version: "22"
40+
41+
- name: Install elan
42+
uses: leanprover/lean-action@v1
2643
with:
27-
lake-package-directory: "Projects/mathlib-demo"
28-
build: true
44+
lake-package-directory: Projects/mathlib-demo
45+
use-mathlib-cache: false
46+
use-github-cache: false
47+
auto-config: false
48+
build: false
2949
test: false
3050
lint: false
31-
- run: npm install
32-
# - run: npm audit
33-
# continue-on-error: true
34-
- run: npm run build_client
35-
- run: npm run build_server
51+
52+
- name: Build sample projects
53+
run: npm run build:server
54+
55+
- name: Ensure sample project 'mathlib-demo' is built
56+
run: |
57+
cd Projects/mathlib-demo
58+
lake build --no-build
59+
60+
- name: Ensure sample project 'stable' is built
61+
run: |
62+
cd Projects/stable
63+
lake build --no-build
64+
65+
- name: Install dependencies
66+
run: npm ci
67+
68+
- name: Build client for production
69+
run: npm run build:client
70+
71+
- name: Run Cypress tests (No Video)
72+
id: cypress_no_video
73+
run: npm test
74+
env:
75+
CYPRESS_DEFAULT_BROWSER: ${{ matrix.browser }}
76+
CYPRESS_VIDEO: false
77+
78+
- name: Upload screenshots on failure
79+
if: failure() && steps.cypress_no_video.conclusion == 'failure'
80+
uses: actions/upload-artifact@v4
81+
with:
82+
name: cypress-screenshots-${{ matrix.os }}-${{ matrix.browser }}
83+
path: cypress/screenshots
84+
85+
- name: Run Cypress tests (With Video)
86+
id: cypress_with_video
87+
if: failure() && steps.cypress_no_video.conclusion == 'failure'
88+
run: npm test
89+
env:
90+
CYPRESS_DEFAULT_BROWSER: ${{ matrix.browser }}
91+
CYPRESS_VIDEO: true
92+
CYPRESS_VIDEO_COMPRESSION: true
93+
94+
- name: Upload videos
95+
if: failure() && steps.cypress_no_video.conclusion == 'failure'
96+
uses: actions/upload-artifact@v4
97+
with:
98+
name: cypress-videos-${{ matrix.os }}-${{ matrix.browser }}
99+
path: cypress/videos

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,9 @@ dist
1212
dist-ssr
1313
*.local
1414

15+
cypress/screenshots
16+
cypress/videos
17+
1518
**/.lake
1619

1720
# Editor directories and files

‎.npmrc‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
engine-strict=true

‎Projects/mathlib-demo/MathlibLatest/Rational.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ variable (x y z : ℚ)
99
example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by
1010
linarith -- the `linarith` tactic can do this automatically
1111

12-
-- let's prove that (x+y)^2=x^2+2*x*y+y^2
12+
-- let's prove that (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2
1313

14-
example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
14+
example : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
1515
ring -- the `ring` tactic can do this automatically

‎Projects/mathlib-demo/lake-manifest.json‎

Lines changed: 50 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,75 +1,95 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover-community/batteries",
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "",
8+
"rev": "0ae30b68e680199367b2d4de739cbfdd6032b480",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "master",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
515
"type": "git",
616
"subDir": null,
717
"scope": "leanprover-community",
8-
"rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
9-
"name": "batteries",
18+
"rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
19+
"name": "plausible",
1020
"manifestFile": "lake-manifest.json",
1121
"inputRev": "main",
1222
"inherited": true,
13-
"configFile": "lakefile.lean"},
14-
{"url": "https://github.com/leanprover-community/quote4",
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
1525
"type": "git",
1626
"subDir": null,
1727
"scope": "leanprover-community",
18-
"rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
19-
"name": "Qq",
28+
"rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
29+
"name": "LeanSearchClient",
2030
"manifestFile": "lake-manifest.json",
21-
"inputRev": "master",
31+
"inputRev": "main",
2232
"inherited": true,
23-
"configFile": "lakefile.lean"},
24-
{"url": "https://github.com/leanprover-community/aesop",
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
2535
"type": "git",
2636
"subDir": null,
2737
"scope": "leanprover-community",
28-
"rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
29-
"name": "aesop",
38+
"rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
39+
"name": "importGraph",
3040
"manifestFile": "lake-manifest.json",
31-
"inputRev": "master",
41+
"inputRev": "main",
3242
"inherited": true,
3343
"configFile": "lakefile.toml"},
3444
{"url": "https://github.com/leanprover-community/ProofWidgets4",
3545
"type": "git",
3646
"subDir": null,
3747
"scope": "leanprover-community",
38-
"rev": "a96aee5245720f588876021b6a0aa73efee49c76",
48+
"rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
3949
"name": "proofwidgets",
4050
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v0.0.41",
51+
"inputRev": "v0.0.53",
4252
"inherited": true,
4353
"configFile": "lakefile.lean"},
44-
{"url": "https://github.com/leanprover/lean4-cli",
54+
{"url": "https://github.com/leanprover-community/aesop",
4555
"type": "git",
4656
"subDir": null,
47-
"scope": "",
48-
"rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
49-
"name": "Cli",
57+
"scope": "leanprover-community",
58+
"rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
59+
"name": "aesop",
5060
"manifestFile": "lake-manifest.json",
51-
"inputRev": "main",
61+
"inputRev": "master",
5262
"inherited": true,
5363
"configFile": "lakefile.toml"},
54-
{"url": "https://github.com/leanprover-community/import-graph",
64+
{"url": "https://github.com/leanprover-community/quote4",
5565
"type": "git",
5666
"subDir": null,
5767
"scope": "leanprover-community",
58-
"rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
59-
"name": "importGraph",
68+
"rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "b8e143008dc1e5f28f48a8aa8de63deaf4fe8068",
79+
"name": "batteries",
6080
"manifestFile": "lake-manifest.json",
6181
"inputRev": "main",
6282
"inherited": true,
6383
"configFile": "lakefile.toml"},
64-
{"url": "https://github.com/leanprover-community/mathlib4",
84+
{"url": "https://github.com/leanprover/lean4-cli",
6585
"type": "git",
6686
"subDir": null,
67-
"scope": "",
68-
"rev": "00df099f8ed42c12b35cdedcfbf1fde6c7413662",
69-
"name": "mathlib",
87+
"scope": "leanprover",
88+
"rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
89+
"name": "Cli",
7090
"manifestFile": "lake-manifest.json",
71-
"inputRev": "master",
72-
"inherited": false,
73-
"configFile": "lakefile.lean"}],
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
7494
"name": "mathlibLatest",
7595
"lakeDir": ".lake"}

‎Projects/mathlib-demo/lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.11.0
1+
leanprover/lean4:v4.18.0-rc1

0 commit comments

Comments
 (0)