7 Commits

Author SHA1 Message Date
Sebastian Ullrich
16873fb123 chore: modulize: work around unknown initial command (#12080) 2026-01-21 20:25:13 +00:00
Sebastian Ullrich
94e8fd4845 chore: update script/Modulize.lean (#12079) 2026-01-21 13:22:39 +00:00
Markus Himmel
b28daa6d60 chore: rename String.endPos -> String.rawEndPos (#10853)
This PR renames `String.endPos` to `String.rawEndPos`, as in a future
release the name `String.endPos` will be taken by the function that is
currently called `String.endValidPos`.
2025-10-21 11:25:30 +00:00
Sebastian Ullrich
715c53d92e chore: Modulize: put section below first module doc (#10693) 2025-10-07 09:10:42 +00:00
Sebastian Ullrich
1ecdf8ddfa chore: simplify and extend Modulize.lean (#10692)
Take explicit list of files instead of asking Lake, take `--meta` flag
instead of guessing based on module name.
2025-10-07 08:22:52 +00:00
Sebastian Ullrich
d17160518c chore: module system fixes and refinements from Mathlib porting (#10643) 2025-10-02 08:28:08 +00:00
Sebastian Ullrich
44a2b085c4 feat: scripts/Modulize.lean (#10460)
This PR introduces a simple script that adjusts module headers in a
package for use of the module system, without further minimizing import
or annotation use.

---------

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
2025-09-24 11:40:17 +00:00