Skip to content

Commit 05890b5

Browse files
samuelburnhamsamuelburnham
authored
feat: Add ix compile CLI and CI benchmarks (#304)
* feat: Add `ix compile` CLI and CI benchmarks * Fixup * Fix env * Switch to compiler binary * Pretty print * Build Benchmarks/Compile to get mathlib cache * Cache each matrix job separately * Deduplicate vars * Cache ix binary * Pre-build when compiling, move ix_test to Benchmarks * Fix CLI test * Auto-detect mathlib cache * Add CompileFC benchmark * Revert to shared cache * Don't cache individual targets * Cache FLT only * Restore CompileFC bench * Fix FLT/FC caching * Cache ix binary and remove broken CompileFC for now * Fixup * Cleanup
1 parent d8d7af5 commit 05890b5

36 files changed

+1236
-76
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ jobs:
7777
- uses: ./.github/actions/ci-env
7878
- uses: actions/checkout@v5
7979
- uses: dtolnay/rust-toolchain@stable
80+
- uses: Swatinem/rust-cache@v2
8081
- name: Check Rustfmt code style
8182
run: cargo fmt --all --check
8283
- name: Check *everything* compiles

‎.github/workflows/compile.yml‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
name: Benchmark Ix compiler
2+
3+
on:
4+
push:
5+
branches: main
6+
workflow_dispatch:
7+
8+
permissions:
9+
contents: read
10+
11+
concurrency:
12+
group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
13+
cancel-in-progress: true
14+
15+
env:
16+
COMPILE_DIR: Benchmarks/Compile
17+
18+
jobs:
19+
# First build and cache the `ix` binary for use in each matrix job
20+
build:
21+
runs-on: ubuntu-latest
22+
steps:
23+
- uses: actions/checkout@v6
24+
- uses: Swatinem/rust-cache@v2
25+
- uses: leanprover/lean-action@v1
26+
with:
27+
build-args: "ix --wfail -v"
28+
test: false
29+
- run: |
30+
mkdir -p ~/.local/bin
31+
echo | lake run install
32+
- uses: actions/cache/save@v4
33+
with:
34+
path: ~/.local/bin/ix
35+
key: ix-${{ github.sha }}
36+
37+
# Run the Ix compiler over each library env in Benchmarks/Compile
38+
run-compiler:
39+
needs: build
40+
strategy:
41+
matrix:
42+
bench: [InitStd, Lean, Mathlib, FLT] # Add FC once updated to Lean v4.26.0
43+
include:
44+
- bench: FLT
45+
cache_pkg: flt
46+
# - bench: FC
47+
# cache_pkg: formal_conjectures
48+
runs-on: warp-ubuntu-latest-x64-32x
49+
steps:
50+
- uses: actions/checkout@v6
51+
# Restore cached `ix` binary
52+
- uses: actions/cache/restore@v4
53+
with:
54+
path: ~/.local/bin/ix
55+
key: ix-${{ github.sha }}
56+
- run: echo "$HOME/.local/bin" >> $GITHUB_PATH
57+
- if: matrix.bench == 'FC'
58+
run: echo "COMPILE_DIR=${{env.COMPILE_DIR}}FC" | tee -a $GITHUB_ENV
59+
# Download elan and fetch mathlib cache
60+
- uses: leanprover/lean-action@v1
61+
with:
62+
lake-package-directory: ${{ env.COMPILE_DIR }}
63+
build: false
64+
use-github-cache: false
65+
# FLT and FC take a few minutes to rebuild, so we cache the build artifacts
66+
- if: matrix.cache_pkg
67+
uses: actions/cache@v4
68+
with:
69+
path: ${{ env.COMPILE_DIR }}/.lake/packages/${{ matrix.cache_pkg }}/.lake/build
70+
key: ${{ matrix.cache_pkg }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', env.COMPILE_DIR)) }}-${{ hashFiles(format('{0}/lake-manifest.json', env.COMPILE_DIR)) }}
71+
# Build the input library
72+
# Allow warnings due to copyright notice in formal-conjectures
73+
- run: lake build Compile${{ matrix.bench }}
74+
working-directory: ${{ env.COMPILE_DIR }}
75+
# Run the `ix` compiler over the input library env
76+
- run: ix compile --path ${{ env.COMPILE_DIR }}/Compile${{ matrix.bench }}.lean
77+

‎.github/workflows/nix.yml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,9 @@ jobs:
3333
- run: nix build .#bench-shardmap --print-build-logs --accept-flake-config
3434
# Ix tests
3535
- run: nix run .#test --accept-flake-config
36-
- run: nix run .#test-aiur --accept-flake-config
37-
- run: nix run .#test-ixvm --accept-flake-config
36+
# Expensive tests are only built in Nix to save time
37+
- run: nix build .#test-aiur --accept-flake-config
38+
- run: nix build .#test-ixvm --accept-flake-config
3839

3940
# Tests Nix devShell support on Ubuntu
4041
nix-devshell:

‎.gitignore‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
# Lean
2-
/.lake
2+
**/.lake
33

44
# Rust
55
/target

‎Benchmarks/Compile/CompileFLT.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
import FLT
2+

ix_test/IxTest.lean renamed to Benchmarks/Compile/CompileInitStd.lean

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,7 @@
1-
-- This module serves as the root of the `IxTest` library.
2-
-- Import modules here that should be built as part of the library.
3-
import IxTest.Basic
41
import Init
52
import Std
63

74
def id' (A: Type) (x: A) := x
8-
def ref (A: Type) (_x : A) := hello
95

106
def idX {A: Type} : A -> A := fun x => x
117
def idY {A: Type} : A -> A := fun y => y

‎Benchmarks/Compile/CompileLean.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import Lean

‎Benchmarks/Compile/CompileMathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import Mathlib

‎Benchmarks/Compile/README.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# Compile
2+
3+
Test libraries for the Ix compiler
4+
5+
- [Init, Std, and Lean libraries](https://github.com/leanprover/lean4)
6+
- [Mathlib](https://github.com/leanprover-community/mathlib4)
7+
- [FLT project](https://github.com/ImperialCollegeLondon/FLT)
8+
9+
## Usage
10+
11+
`ix compile --path /path/to/Compile<Lib>.lean` # replace `<Lib>` with `InitStd`, `Lean`, `Mathlib`, or `FLT`
12+
13+
> [!NOTE]
14+
> Compiling Mathlib and FLT currently requires a multi-core CPU and >64 GB RAM.

‎Benchmarks/Compile/lake-manifest.json‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/ImperialCollegeLondon/FLT",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "",
8+
"rev": "5d2db3af80b5260ae7d64ba4daf2b7768a9a95b7",
9+
"name": "flt",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.26.0",
12+
"inherited": false,
13+
"configFile": "lakefile.toml"},
14+
{"url": "https://github.com/leanprover-community/mathlib4",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
19+
"name": "mathlib",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "v4.26.0",
22+
"inherited": false,
23+
"configFile": "lakefile.lean"},
24+
{"url": "https://github.com/PatrickMassot/checkdecls.git",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "",
28+
"rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
29+
"name": "checkdecls",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": null,
32+
"inherited": true,
33+
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/leanprover-community/plausible",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
39+
"name": "plausible",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
49+
"name": "LeanSearchClient",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "main",
52+
"inherited": true,
53+
"configFile": "lakefile.toml"},
54+
{"url": "https://github.com/leanprover-community/import-graph",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
59+
"name": "importGraph",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "main",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
69+
"name": "proofwidgets",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "v0.0.83",
72+
"inherited": true,
73+
"configFile": "lakefile.lean"},
74+
{"url": "https://github.com/leanprover-community/aesop",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
79+
"name": "aesop",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "master",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover-community/quote4",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "9312503909aa8e8bb392530145cc1677a6298574",
89+
"name": "Qq",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "master",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"},
94+
{"url": "https://github.com/leanprover-community/batteries",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "leanprover-community",
98+
"rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
99+
"name": "batteries",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"},
104+
{"url": "https://github.com/leanprover/lean4-cli",
105+
"type": "git",
106+
"subDir": null,
107+
"scope": "leanprover",
108+
"rev": "933fce7e893f65969714c60cdb4bd8376786044e",
109+
"name": "Cli",
110+
"manifestFile": "lake-manifest.json",
111+
"inputRev": "v4.26.0",
112+
"inherited": true,
113+
"configFile": "lakefile.toml"}],
114+
"name": "Compile",
115+
"lakeDir": ".lake"}

0 commit comments

Comments
 (0)