Skip to content

feat: mention #min_imports in imports style documentation - #896

Open
JadAbouHawili wants to merge 3 commits into
leanprover-community:lean4from
JadAbouHawili:min-imports
Open

feat: mention #min_imports in imports style documentation#896
JadAbouHawili wants to merge 3 commits into
leanprover-community:lean4from
JadAbouHawili:min-imports

Conversation

@JadAbouHawili

Copy link
Copy Markdown

No description provided.

@grunweg grunweg left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for trying to keep the docs updated. I applaud the idea, but I'm not sure this particular change is useful. I have explained this in more detail below.

then group all `import`s together,
Try to keep the imports alphabetical within each block of imports.
Try to keep the imports alphabetical within each block of imports
and avoid specifying imports which are already transitively imported by another import.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would be a new policy, so deserves a careful look. In this case, there is no general agreement about this being a good change - so please revert this sentence. (What is true is that one shouldn't randomly add transitively implied imports - but that might be understood in general, hence shouldn't be said here.)

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(What is true is that one shouldn't randomly add transitively implied imports )

I agree , which is why you should "try" "to avoid specifying imports which are already transitively imported by another import" , which is the current wording.

A policy would be something like:
"Put the module keyword on its own line right after the header, skip a line, ..."
"The file header should contain copyright information, ..."

@JadAbouHawili JadAbouHawili Aug 20, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can instead say "and try to avoid specifying imports ... " to make the point clear

Comment thread templates/contribute/style.md Outdated
Try to keep the imports alphabetical within each block of imports.
Try to keep the imports alphabetical within each block of imports
and avoid specifying imports which are already transitively imported by another import.
We recommend using `#min_imports` at the end of the file which would output

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wouldn't say "recommend" (that's too strong) --- more that it's a possibility.

That said, I'm not sure if this document is the best place for such general advice. This style guide is describing rules to follow, not giving advice to users. (I don't see an obvious other place to put it either, unfortunately.)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that currently #min_imports is not mentioned anywhere on the site, which seems wrong.

@JadAbouHawili JadAbouHawili Aug 20, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

changed the wording to not say "recommend" , just to say that using #min_imports would output something that satisfies these conditions.

I think that mentioning #min_imports here (or some other docs) is an improvement

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.

3 participants