Skip to content

[Merged by Bors] - chore: no newline between public imports - #42064

Closed
felixpernegger wants to merge 3 commits into
leanprover-community:masterfrom
felixpernegger:spacepublicimports
Closed

[Merged by Bors] - chore: no newline between public imports#42064
felixpernegger wants to merge 3 commits into
leanprover-community:masterfrom
felixpernegger:spacepublicimports

Conversation

@felixpernegger

@felixpernegger felixpernegger commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Similar (motivation) to #42063. This PR removes all newlines between public imports. This is not important as standalone PR, but makes diffs of later PRs nicer and thus help reviewing.

This includes space between ordinary public and public meta imports (and imports from Lean core). Maybe there should be a convention on there to be a newline for those cases, but this is not currently done in the vast majority of cases and not the scope of this PR.

Also some import orders of affected files are not ordered alphabetically still, which I did not fix as this is again not the goal of this PR.

Open in Gitpod

@github-actions

github-actions Bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 815258f10e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 815258f).

  • +0 new declarations
  • −0 removed declarations

No declaration differences.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 815258f10e
Reference commit 7779d601f7

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@felixpernegger

felixpernegger commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

easy

@github-actions github-actions Bot added the easy < 20s of review time. See the lifecycle page for guidelines. label Jul 24, 2026
themathqueen
themathqueen reviewed Jul 24, 2026
View reviewed changes
Comment thread Mathlib/Tactic/NormNum/Result.lean
public import Mathlib.Algebra.Ring.Nat
public import Mathlib.Data.Int.Cast.Basic
public import Qq.MetaM

@themathqueen themathqueen Jul 24, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

I'd keep this since the import below is a meta import

themathqueen
themathqueen reviewed Jul 24, 2026
View reviewed changes
Comment thread Mathlib/Topology/Defs/Basic.lean
public import Mathlib.Tactic.FunProp
public import Mathlib.Tactic.MkIffOfInductiveProp
public import Mathlib.Data.Nat.Notation

@themathqueen themathqueen Jul 24, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

same here

j-loreaux
j-loreaux reviewed Jul 24, 2026
View reviewed changes

@j-loreaux j-loreaux 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.

bors d+

@felixpernegger

felixpernegger commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

bors merge

@mathlib-bors

mathlib-bors Bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

🔒 Permission denied

An existing reviewer can click here to make felixpernegger a reviewer.

@felixpernegger

felixpernegger commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

bors r+

@mathlib-bors

mathlib-bors Bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

🔒 Permission denied

An existing reviewer can click here to make felixpernegger a reviewer.

@felixpernegger

felixpernegger commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

@j-loreaux seems like bors bugged

@j-loreaux

j-loreaux commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

bors merge

@mathlib-bors mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jul 24, 2026
mathlib-bors Bot pushed a commit that referenced this pull request Jul 24, 2026
@felixpernegger
chore: no newline between public imports (#42064)
f61feab 
Similar (motivation) to #42063. This PR removes all newlines between public imports. This is not important as standalone PR, but makes diffs of later PRs nicer and thus help reviewing.

This includes space between ordinary public and `public meta` imports (and imports from Lean core). Maybe there should be a convention on there to be a newline for those cases, but this is not currently done in the vast majority of cases and not the scope of this PR.

Also some import orders of affected files are not ordered alphabetically still, which I did not fix as this is again not the goal of this PR.

Co-authored-by: Batixx <s59fpern@uni-bonn.de>
@mathlib-bors mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jul 24, 2026
@mathlib-bors

mathlib-bors Bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: no newline between public imports [Merged by Bors] - chore: no newline between public imports Jul 24, 2026
@mathlib-bors mathlib-bors Bot closed this Jul 24, 2026
mpacholski pushed a commit to mpacholski/mathlib4 that referenced this pull request Jul 30, 2026
@felixpernegger @mpacholski
chore: no newline between public imports (leanprover-community#42064)
8dc4b4b 
Similar (motivation) to leanprover-community#42063. This PR removes all newlines between public imports. This is not important as standalone PR, but makes diffs of later PRs nicer and thus help reviewing.

This includes space between ordinary public and `public meta` imports (and imports from Lean core). Maybe there should be a convention on there to be a newline for those cases, but this is not currently done in the vast majority of cases and not the scope of this PR.

Also some import orders of affected files are not ordered alphabetically still, which I did not fix as this is again not the goal of this PR.

Co-authored-by: Batixx <s59fpern@uni-bonn.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments
@themathqueen themathqueen themathqueen left review comments

Assignees

No one assigned

Labels

bors-staging This PR is currently being built by bors on the staging branch. easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@felixpernegger @j-loreaux @themathqueen