Skip to content

Conversation

@nomeata
Copy link
Collaborator

@nomeata nomeata commented Dec 10, 2025

This PR splits file and process related things out of Init.System.IO, to improve build parallelism in core.

@nomeata nomeata added the changelog-language Language features and metaprograms label Dec 10, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Dec 10, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 10, 2025

Benchmark results for 7087c07 against 30ea417 are in! @nomeata

Runs (2)
  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

@nomeata
Copy link
Collaborator Author

nomeata commented Dec 10, 2025

In particular some of these dependencies on Lean.Expr (or at least on Lean.ImportingFlag) could hopefully be avoided:

       2.3  1.4%     44.9   26.8%  Init.Data.String.Decode
       2.9  1.7%     47.8   28.5%  Init.Data.String.Basic
       0.3  0.2%     48.0   28.7%  Init.Data.String.Lemmas.Basic
       0.4  0.2%     48.4   28.9%  Init.Data.String.Lemmas.Splits
       0.5  0.3%     49.0   29.2%  Init.Data.String.Termination
       2.3  1.4%     51.3   30.6%  Init.Data.String.Pattern.String
       0.3  0.2%     51.6   30.8%  Init.Data.String.Pattern
       2.7  1.6%     54.3   32.4%  Init.Data.String.Slice
       0.7  0.4%     55.0   32.8%  Init.Data.String.Search
       0.4  0.2%     55.3   33.0%  Init.System.FilePath
       1.3  0.8%     56.6   33.8%  Init.System.IO
       0.4  0.2%     57.0   34.1%  Lean.ImportingFlag
       0.7  0.4%     57.8   34.5%  Lean.Data.Options
       0.5  0.3%     58.2   34.8%  Lean.Data.Format
       0.3  0.2%     58.5   35.0%  Lean.Hygiene
       1.6  1.0%     60.1   35.9%  Lean.Level
       1.9  1.1%     62.0   37.1%  Lean.Expr

@nomeata
Copy link
Collaborator Author

nomeata commented Dec 10, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Dec 10, 2025

Benchmark results for 045b8b5 against 30ea417 are in! @nomeata

Minor changes (2)
  • build/stat/imported consts//amount: -504.6k (-0.6%)
  • 🟥 size/init/.olean//bytes: +186kiB (+0.2%)

@nomeata
Copy link
Collaborator Author

nomeata commented Dec 10, 2025

Only a mild effect on the build graph

build/lakeprof/longest build path	//	wall-clock	2m 44s	-3s	-2.0%	s

https://radar.lean-lang.org/repos/lean4/commits/045b8b5d50191e8facf93cd7221f02736bf5d2b6?s=longest&reference=30ea4170a726da78860f78f9586658a9f223289a

Probably not worth the disruption at this point.

@nomeata nomeata closed this Dec 10, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants