Repository navigation
Conversation
_locked_mathlib had two try blocks with identical handlers around the layout check and the package decoding. The legacy-layout branch between them builds its diagnostic from constant strings and cannot raise, so it moves inside one try.
_trim_elan_whitespace looped over a frozenset of elan's whitespace. str.strip with the same characters as a string trims the same set.
- _MANIFEST_VERSION was _LAKE_VERSION with capture groups. The other use of _LAKE_VERSION only tests for a full match, so one pattern with the groups serves both. - _json_optional was _json_default with a None default. - _canonical_manifest_name and _canonical_toml_name both normalized the numeric parts _split_lean_name returned. _split_lean_name now does it.
Its only caller passed a fresh list and never read it again.
meta-cla
Bot
added
the
CLA Signed
Review at fc97d1cVerdict: merge-ready. The no-behaviour-change claim holds, but #204 breaks the CLI if both land unchanged. #204 is an open draft that imports two of the helpers this PR deletes. How the claim was checked:
Landing
|
#204 adds autoform_cli/library/locate.py, which imports _json_optional from _lake_metadata and _trim_elan_whitespace from inspect, and __main__ imports that module at startup. With both deleted, main plus this branch plus #204 merges cleanly, yet every autoform command then fails with ImportError. Restore main's two definitions unchanged, each with a comment naming the importer. This module's own callers stay on _json_default and str.strip. _ELAN_WHITESPACE is now a string rather than main's frozenset, but the loop only tests single characters, for which the two agree, so the restored trim returns what main's does for every string.
Franky100-pig
left a comment
Franky100-pig
left a comment
There was a problem hiding this comment.
Thanks for the unusually clear PR description — it made verification straightforward. I read the diff against each claimed change and grepped the tree for dangling references to the removed/renamed symbols.
Verified (behaviour-preserving):
_MANIFEST_VERSIONand_json_optionalare gone; grep finds no remaining references. The still-present names (_LAKE_VERSION,_json_default,_canonical_manifest_name,_canonical_toml_name) are all still defined and called._LAKE_VERSIONnow carries the capture groups and serves both call sites:_manifest_layoutusesmatch.groups(), and the otherfullmatchcall is unaffected. Same matches._json_optional(..., str)→_json_default(..., None, str)is equivalent for the three call sites (absent / explicit-null / wrong-type all behave identically)._split_lean_namenow normalizes numeric parts and returns a tuple; the two_canonical_*wrappers delegate correctly, so their outputs are unchanged._locked_mathlib: the legacy-layout branch now sits inside the singletry, and_validate_manifest_rootis still inside it, so itsValueErroris still caught by the oneexcept (AttributeError, RecursionError, ValueError).
One thing worth a second look (turns out fine):
_ELAN_WHITESPACEchanged fromfrozenset(...)to(...). At a glance that looks like it became a tuple, which would makestr.strip(_ELAN_WHITESPACE)raiseTypeError. But the three string literals are adjacent with no commas, so they concatenate into a singlestr—.strip()is valid and trims the same set (I confirmed locally:typeisstr, len 25, and" \u3000hi\u00a0 ".strip(...)→"hi"). A plain= "..."without the wrapping parentheses would remove the tuple-footgun for the next reader; non-blocking.
Minor / non-blocking:
- With
_json_optionalremoved, theNonedefault is now hard-coded at each call site. Fine here, just slightly less self-documenting than the old name implied.
The "no behaviour change" claim holds up. Nice cleanup. (I reviewed by reading + grepping; I didn't run uv/the suite locally, so I'm trusting your validation note on test_project_inspect.py / test_servers.py.)
|
Kept the two helpers #204 imports, in |
2 participants
Cleanup of the project inspection code from #14 and #79. No behaviour change: 2 files, +26/-44, one commit per item.
_locked_mathlib(inspect.py). Twotryblocks had identical handlers reportinginvalid-lake-manifest. The legacy-layout branch between them builds its warning from constant strings and cannot raise, so it moves inside onetry.inspect.py)._inspect_toolchaintrimmed the first line with_trim_elan_whitespace, a loop over a frozenset of elan's whitespace characters.str.stripwith the same characters as a string trims the same set, so it now calls that. The comment on_ELAN_WHITESPACEstill says why the set differs from Python's._lake_metadata.py)._MANIFEST_VERSIONwas_LAKE_VERSIONwith capture groups. The other use of_LAKE_VERSIONonly tests for a full match, so one pattern with the groups serves both._json_optionalis_json_defaultwith aNonedefault, so the module's three calls now use_json_default._canonical_manifest_nameand_canonical_toml_nameboth normalized the numeric parts_split_lean_namereturned._split_lean_namenow does it, and returns a tuple._inspect_snapshotowns its diagnostics list. Its only caller passed in a fresh list and never read it again.autoform search, and generate its index (#203, reader and generator) #204. Search a locked Lean library fromautoform search, and generate its index (#203, reader and generator) #204's library locator imports_json_optionaland_trim_elan_whitespace, andautoform_cli/__main__.pyimports the locator at startup. Deleting the two helpers let main, this PR and Search a locked Lean library fromautoform search, and generate its index (#203, reader and generator) #204 merge without a conflict, after which everyautoformcommand failed withImportError. Both keep main's definitions unchanged, each under a comment naming Search a locked Lean library fromautoform search, and generate its index (#203, reader and generator) #204 as the importer, so either PR can land first without a change to the other.No other open PR edits these two files, and none uses
_MANIFEST_VERSION,_LAKE_VERSION,_ELAN_WHITESPACE,_split_lean_nameor_inspect_snapshot, the names this PR removes or whose type or signature it changes.Validation at exact head
fc97d1cf:ruff check autoform_cli servers testsis clean.tests/test_project_inspect.py(272) andtests/test_servers.py(19) pass. Intests/test_plugin_runtime.py, 3 pass; the fourth,test_wheel_contains_only_the_minimal_runtime, fails the same way on main in this checkout, becauseuv buildreads a parent directory'spyproject.toml. CI runs it.At
b00a60c9, which only restores the two helpers: both parse to the same AST as on main._trim_elan_whitespacenow tests membership in_ELAN_WHITESPACEas a string rather than main's frozenset, and it returns the same as main's on 3,490,329 strings, including every code point alone and inside whitespace.ruff check autoform_cli servers testsis clean, andtests/test_project_inspect.pypasses (272) with the checkout importable by child processes.With #204 at
270ed1f7: merging this head and #204 onto main8575a15cgives no conflict and the same tree in either order. Therepython -m autoform_cli --helpexits 0; withfc97d1cfin place of this head it failed withImportError: cannot import name '_json_optional'. In that tree, #204's fivetests/test_library_*.pyfiles pass (118) andtests/test_project_inspect.pypasses (272).