leanprover
refactor: lake: CLI API overhaul
This PR refactors Lake's CLI API and related code to make more use of the new String Slice API. It also generally expands the scope of the CLI API to cover argument parsing and some basic verification.
This is mostly a quality-of-life improvement for my use of the API in Lake and for adding additional CLI code in the future.
Benchmark results for 3a049c91e65686b1157b135fec0a71448dde67f2 against b0e6db322421ce368999f08870fd747e45242f86 are in! @tydeu
Minor changes (3)
- 🟥
build//instructions: +31.4G (+0.2%) - ✅
bv_decide_large_aig.lean//instructions: -308.9M (-0.7%) - 🟥
size/stdlib/.olean.server//bytes: +64kiB (+0.2%)
Benchmark results for 7ca252eefa336f078e191add233b05cc7b78ae1e against 5bd331e85d9d110a29fb3367dbb21854010ffcbd are in! @tydeu
Minor changes (2)
- 🟥
build//instructions: +31.4G (+0.2%) - 🟥
size/all/.olean.server//bytes: +64kiB (+0.2%)
Reference manual CI status:
- ✅ Reference manual branch lean-pr-testing-11435 has successfully built against this PR. (2025-12-07 20:16:40) View Log
- 🟡 Reference manual branch lean-pr-testing-11435 build against this PR didn't complete normally. (2025-12-07 20:17:50) View Log
- ✅ Reference manual branch lean-pr-testing-11435 has successfully built against this PR. (2025-12-08 04:04:17) View Log
- 🟡 Reference manual branch lean-pr-testing-11435 build against this PR didn't complete normally. (2025-12-08 04:05:08) View Log
Mathlib CI status (docs):
- ✅ Mathlib branch lean-pr-testing-11435 has successfully built against this PR. (2025-12-07 21:13:04) View Log
