lake exe shake --fix is broken

Stream: general

[Yaël Dillies]

It doesn't really work still. lake exe shake --fix in Toric returns a list of suggestions, but doesn't apply the import deletions. Funnily enough, it does apply the import additions!

[Kevin Buzzard]

I can confirm -- I just ran into this in FLT and whilst additions worked fine, I had to remove imports from 12 files manually after the fallout of some mathlib file splitting. Which repo should I open an issue against?

[Yaël Dillies]

shake is currently in mathlib

[Kevin Buzzard]

#24743

[Yury G. Kudryashov]

I have an impression that lake exe shake --fix doesn't remove any imports. It adds imports it shows in the log but doesn't remove them.

[Yaël Dillies]

See #general > Running lake exe shake in projects depending on mathlib

[Yury G. Kudryashov]

I see the same in Mathlib.

[Yury G. Kudryashov]

Marking this one as resolved so that we discuss this in 1 thread.

[Notification Bot]

Yury G. Kudryashov has marked this topic as resolved.

[Notification Bot]

Yaël Dillies has marked this topic as unresolved.

[Yury G. Kudryashov]

To other readers: the few messages above mean that I resolved this thread, then Yael unresolved it and moved relevant messages from the other thread here.

[Kevin Buzzard]

I opened #24743

[Kim Morrison]

@Mario Carneiro, unfortunately after your fix shake is now too aggressive, and removes more imports than desired.

[Mario Carneiro]

I didn't change the behavior of shake, it is as aggressive as it has always been

[Mario Carneiro]

Do you mean that it is not correctly identifying imports that it claims to want to remove?

[Mario Carneiro]

The issue was that the syntax of import changed due to Sebastian's work on the module system, and I think it has changed twice in quick succession (import private became private import), so you may have run into some intermediate state

[Mac Malone]

Mario Carneiro said:

import private became private import

import private became import all; private import is a separate feature.

[Mario Carneiro]

well either way the grammar changed twice

[Kim Morrison]

It looked to me that when it found an import to delete, it was deleting more than just that import. (Perhaps all following imports? I didn't look closely.)

[Ruben Van de Velde]

Do you remember where this happened?

[Kim Morrison]

It was on nightly-testing, see 3f35133e04a0206d158ecb9642003b6b94b23720

[Ruben Van de Velde]

$ lake exe shake --fix

The following changes will be made automatically:
Mathlib/Data/Part.lean:
  remove #[Mathlib.Algebra.Notation.Defs]
Successfully applied 1 suggestions.

$ git diff

diff --git Mathlib/Data/Part.lean Mathlib/Data/Part.lean
index 3d156636ef5..5273adad838 100644
--- Mathlib/Data/Part.lean
+++ Mathlib/Data/Part.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
 -/
 import Mathlib.Algebra.Notation.Defs
-import Mathlib.Data.Set.Subsingleton
-import Mathlib.Logic.Equiv.Defs

 /-!
 # Partial values of a type

[Ruben Van de Velde]

That certainly doesn't look right

[Kevin Buzzard]

Yes, "1 suggestions" should clearly be "1 suggestion" ;-)

[Kevin Buzzard]

Just to be clear, my clever-clever comment above isn't supposed to detract from the fact that lake exe shake --fix is now the most broken it has ever been, it now deletes random imports instead of the right ones

[Yaël Dillies]

May I bump this issue on top of @Mario Carneiro's radar? lake exe shake --fix currently misapplies the suggestions: When trying to delete import B in the following, it instead deletes imports C and D

import A
import B
import C
import D

[Yaël Dillies]

This makes it basically unusable :sad:

[Mario Carneiro]

Mario Carneiro said:

well either way the grammar changed twice

As I suspected, the issue is that the syntax changed yet again (3rd time's the charm?). To emphasize, this is not the same bug as #24743, it was fixed and then it was broken again in that time window

[Mario Carneiro]

#25054

[Eric Wieser]

What are the new syntax features for import?

[Mario Carneiro]

it now has both private and all

[Mario Carneiro]

private import all Foo is syntactically correct

[Mario Carneiro]

don't ask me what it does

[Mario Carneiro]

I added a self-test so the next time sebastian has a bright idea I won't get a call at 3am

[Mario Carneiro]

...figuratively speaking :grinning_face_with_smiling_eyes:

[Eric Wieser]

I would guess private means "downstream files don't see this" and all overrides that in imported files

[Mario Carneiro]

no, private import is more like open private from batteries, it means you get to see internal details from a module

[Mario Carneiro]

IIRC

[Mario Carneiro]

This just went from bors r+ to merged in 7 minutes. This is surprisingly fast?

[Bryan Gin-ge Chen]

CI is fast on changes that don't require recompiling mathlib :wink:

[Mario Carneiro]

I thought linting put a lower bound on simple changes

[Mario Carneiro]

has it really become so fast that it can be done in 2.5 minutes or are the expensive things like simp confluence not running anymore?

[Aaron Liu]

well you didn't mark anything @[simp]

[Ruben Van de Velde]

We don't cache lint checks

[Mario Carneiro]

Eric Wieser said:

I would guess private means "downstream files don't see this" and all overrides that in imported files

You are right. From the source (isExported = !private):

structure Import where
  module        : Name
  /-- `import all`; whether to import and expose all data saved by the module. -/
  importAll : Bool := false
  /-- Whether to activate this import when the current module itself is imported. -/
  isExported    : Bool := true
  deriving Repr, Inhabited, ToJson, FromJson

[Edward van de Meent]

maybe the idea for this is "you only need the tactics when compiling the file, not after"?

[Mario Carneiro]

I think it is also meant to include actual definitions and theorems used in setting up an API that isn't meant to be unfolded

[Mario Carneiro]

the key goal is to claw back the idea that lean imports are transitive

[Mario Carneiro]

hopefully eventually this may mean that you will not need to even load most of the thousands of files in the dependency tree because most of them are only used as dependencies of dependencies and nothing about them is visible to you

[Yury G. Kudryashov]

We should discuss whether we want to use this feature in mathlib, but not in this thread.

[Mario Carneiro]

well, much like grind, it's waiting for the FRO to actually officially announce it and open up at least a call for testing

[Mario Carneiro]

Mario Carneiro said:

Mario Carneiro said:

well either way the grammar changed twice

As I suspected, the issue is that the syntax changed yet again (3rd time's the charm?). To emphasize, this is not the same bug as #24743, it was fixed and then it was broken again in that time window

Third time was apparently not the charm: lean4#8598 will break shake again once it percolates through the system. At least this time shake will break at compile time so @Kim Morrison will have to ping me about it

[Eric Wieser]

If it's any consolation, lean --deps-json also can't quite parse its imports correctly: lean4#9111