check for unused imports doesn't stop

Stream: mathlib4

[Ralf Stephan]

What to do if that check doesn't stop? See #14389. Five hours now.

[Ruben Van de Velde]

I've hit the "cancel" button

[Ruben Van de Velde]

I guess github would have timed it out eventually

[Ralf Stephan]

Does it stay cancelled? How to restart? Do I need to make a commit?

[Damiano Testa]

I just restarted it: I went to the Required Build and told it to re-run all failed jobs.

[Ralf Stephan]

Thanks!

[Damiano Testa]

Although it seems to be stuck again: normally, Shake takes under a minute to run and it has been going for over half an hour now.

[Ralf Stephan]

Are there options that I can give the shaker locally to see what's wrong?

[Damiano Testa]

Does it also run forever locally?

[Damiano Testa]

(In any case, I do not know of such options, so this is mere curiosity.)

[Ralf Stephan]

Cannot say, lake build already runs forever at the moment. Need to wait an hour probably to be able to test it.

[Ralf Stephan]

Anyway, next I'll make a null commit, maybe it's not in the code.

[Damiano Testa]

I downloaded the cache and lake exe shake does seem to run forever

[Damiano Testa]

(or rather, for at least 20 seconds!)

[Damiano Testa]

I noticed something weird that it downloaded something from aesop with the cache. Maybe merge master into the pr and push.

[Damiano Testa]

This is what it said, in case it is helpful:

mathlib4 (rwst/primesplit3)$ lake exe cache get
info: aesop: URL has changed; deleting '././.lake/packages/aesop' and cloning again
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
Attempting to download 4073 file(s)
Downloaded: 4073 file(s) [attempted 4073/4073 = 100%] (100% success)
Decompressing 4767 file(s)
lake exe shakeUnpacked in 17102 ms
Completed successfully!

[Mario Carneiro]

I would suspect an import cycle

[Ralf Stephan]

Mario Carneiro said:

I would suspect an import cycle

...that passes the build step?

[Ralf Stephan]

No difference after merged master.

[Mario Carneiro]

There is something really weird going on here, I think it is related to the latest lean bump. It appears that constants can now reference constants declared in later modules(?) and this is messing up shake's analysis which assumes some acyclicity

[Mario Carneiro]

Here's a MWE:

import Mathlib.Algebra.Group.Commute.Defs
import Mathlib.Data.Nat.Cast.Defs

open Lean
run_meta
  let env ← getEnv
  let some ci := env.find? `pow_bit1 | throwError "pow_bit1 not found"
  let i : Nat := env.const2ModIdx.find! ci.name
  println! env.header.moduleNames[i]!

  let some ci := env.find? `bit1.eq_1 | throwError "bit1.eq_1 not found"
  let i : Nat := env.const2ModIdx.find! ci.name
  println! env.header.moduleNames[i]!

This code says that pow_bit1 is in Mathlib.Algebra.Group.Commute.Defs, and bit1.eq_1 is in Mathlib.Data.Nat.Cast.Defs, and pow_bit1 depends on bit1.eq_1 even though Mathlib.Data.Nat.Cast.Defs comes after Mathlib.Algebra.Group.Commute.Defs in the import order (these two files do not import each other so it's just the order they are listed in the test file). It shouldn't be possible for pow_bit1 to depend on a file not in its dependency closure?

If I remove the import of Mathlib.Data.Nat.Cast.Defs, then the module of bit1.eq_1 changes to Mathlib.Algebra.Group.Commute.Defs. Are these definitions just defined in multiple places?

[Mario Carneiro]

the shake bug is fixed in #14417 and the lean bug is lean4#4652

[Ralf Stephan]

This passes locally after a dozen seconds:

lake exe shake --no-downstream
././././Mathlib/Dynamics/PeriodicPts.lean:
  remove #[Mathlib.Data.Nat.Prime.Int]
  add #[Mathlib.Dynamics.Newton]
././././Mathlib/Data/Int/NatPrime.lean:
  remove #[Mathlib.Data.Nat.Prime.Int]
  add #[Mathlib.Algebra.Group.Int]

In contrast this does not stop:

lake exe shake --gh-style
././././Mathlib/Dynamics/PeriodicPts.lean:10:1: warning: unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
././././Mathlib/Dynamics/PeriodicPts.lean:13:1: warning: import #[Mathlib.Dynamics.Newton] instead
././././Mathlib/Dynamics/PeriodicPts.lean:
  remove #[Mathlib.Data.Nat.Prime.Int]
  add #[Mathlib.Dynamics.Newton]

I committed the suggested fixes. Let's see.

[Ralf Stephan]

The fixes make it no longer compile, so are the fixes buggy because shake is confused?

[Ralf Stephan]

Anyway shake --gh-style or even shake in general seems no longer reliable. And I'm back tomorrow morning (although I don't think I can be much help from now on).

[Mario Carneiro]

what do you mean by no longer compile?

[Mario Carneiro]

shake has been confused since this issue was introduced in march

[Mario Carneiro]

so it's possible there are some missed diagnostics

[Mario Carneiro]

on the other hand it's also possible that the fix is not enough and the whole algorithm needs a rethink because definitions existing multiple times in the tree was never a part of the design

[Ralf Stephan]

Mario Carneiro said:

what do you mean by no longer compile?

"build mathlib" passed before the last commit.