Skip to content

feat: modulize and revamp #import_diff - #193

Open
thorimur wants to merge 65 commits into
leanprover-community:mainfrom
thorimur:import-diff-module
Open

thorimur wants to merge 65 commits into
leanprover-community:mainfrom
thorimur:import-diff-module

Conversation

@thorimur

@thorimur thorimur commented Nov 9, 2026 •

Copy link
Copy Markdown
Collaborator

This PR makes #import_diff function in the module system, and changes the usage and output significantly.

It now provides tabular output with statistics about the differences between initial and final import states, such as

                 Δ    +    -    ∩
modules imported +194 +453 -259 302

public           +167 +167 -0   0
private          +431 +690 -259 64
public meta      -49  +3   -52  225
private meta     -45  +30  -75  246

previous modules +441 +574 -133 531
ir loaded        +108 +110 -2   397

                 Δ    new  old
build depth      +37  177  140

It also allows two different kinds of input syntax to specify the initial and final states:

Relative to the current imports, which constructs the final state by adding imports to or removing imports from the current imports:

#import_diff +import Foo; -import Bar

Absolute, which compares two import blocks without consulting the current imports at all:

#import_diff from import Foo; meta import Bar to public import Bar

(If from ... is omitted, the current imports are taken as the initial imports.)

The output also provides a collapsible legend for convenience, since this information is rather technical, and the ability to copy the reduced initial and final imports.

See docstrings for details.


Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant