shake in non-mathlib projects

Stream: general

[Kevin Buzzard]

Can I run shake in CI in FLT somehow?

[Kevin Buzzard]

I think the reason I care is different to the reason that mathlib cares -- I just want to minimise the time it takes to build the docs in CI!

[Yaël Dillies]

Try lake exe shake FLT locally to see if it works. In my experience it worked until very recently (in Toric) and now fails with a confusing error message about ././././scripts/noshake.json.

[Riccardo Brasca]

Just put {} in that file and it works (at least it doesn't complain)

[Kevin Buzzard]

I can confirm that running lake exe shake FLT I got a confusing error message about scripts/noshake.json (it's confusing because it says Invalid config file '././././scripts/noshake.json' but what it means is that the file is completely missing) and when I create the file with contents {} then I get what looks like helpful shaky stuff

[Yaël Dillies]

What I'm confused about is that circa 2-3 weeks ago lake exe shake Toric without a scripts/noshake.json gave me helpful shakey stuff already

[Kevin Buzzard]

That's progress for you!

[Yaël Dillies]

But shake is supposedly extremely stable :sweat_smile:

[Kevin Buzzard]

First FLT error is a false positive -- I import Mathlib.Analysis.Quaternion because I want notation ℍ from that file, rather than any of the theorems :-) Is there some kind of shake wishlist or tracking issue? I can just announce that I don't want to shake this and then forget about it, but is this some kind of indication that mathlib should have a Mathlib.Analysis.Quaternion.Notation file or something? Is notation definitely out of scope for shake?

[Yaël Dillies]

shake doesn't detect uses of notation, and probably never will

[Yaël Dillies]

If anything, creating notation-only files makes the issue worse!

[Kevin Buzzard]

oh yeah :-)

[Kevin Buzzard]

Well at least it looks like I have something to put into scripts/noshake.json!

[Kevin Buzzard]

wait -- can I not put a comment in a json file saying why I'm not shaking this import??

[Yaël Dillies]

"Comments are not permitted in JSON." :rofl: Oh well

[Ruben Van de Velde]

Yeah, I'm afraid JSON is for interchange only, not reading or writing yourself :)

[Kevin Buzzard]

Is there a recommended way of keeping track of various reasons that shake was "wrong" about imports?

[Kevin Buzzard]

Or are these reasons all already known and wontfix and the idea is that having a noshake file which we can just forget about even if things change is the way we're supposed to be doing it?

[Yaël Dillies]

I doubt it needs much explanation? You can always try removing the import and see what breaks

[Kevin Buzzard]

I somehow have it in my head that these JSON files used to represent things that we were supposed to fix (modules without docstrings which the community hadn't yet written, linting errors which the community hadn't got around to dealing with etc etc) but here the file seems to indicate shortcomings in the system, which seems like a different thing

[Kevin Buzzard]

Right now I'm looking at a big JSON file called nolints.json and thinking "I can make this smaller by adding a bunch of docstrings and that will make my project better" but for the shake file the idea seems to be that I'm not striving to make it smaller?

[Yaël Dillies]

I agree with your analysis. noshake.json is not expected to get smaller with time. shake is already optimal for its level of complexity, and a new tool would need to be much more complicated to improve upon it.

[Kevin Buzzard]

OK, I'll get back to nolints :-)

[Kevin Buzzard]

My main motivation really is to stop people sneakily adding import Mathlib to the repo and thus doubling the amount of mathlib docs we have to build.

[Yaël Dillies]

I have a step linting for this in Toric. Do you want it?

[Yaël Dillies]

Here it is: https://github.com/YaelDillies/Toric/blob/master/.github/workflows/push_master.yml#L24-L27

[Kevin Buzzard]

Is there a way I can do "do all the things lake exe shake FLT suggests" other than doing them manually?

[Ruben Van de Velde]

lake exe shake --fix FLT?

[Kevin Buzzard]

Now my project mostly builds but I want to add a couple more things to noshake. Is there an automatic way of saying "I know shake is noisy right now but apply none of the suggestions you're making, instead add them all to noshake"?

[Yaël Dillies]

Yes, that's lake exe shake --update FLT

[Kevin Buzzard]

I'm now trying to understand the remaining errors. Is it a known thing that a simp call can break if you remove an import which shake tells you to remove? More details: if I change the simp to a simp only then it explicitly uses a lemma in the (FLT, not mathlib) file which shake is telling me to remove. Is this a bug?

[Kevin Buzzard]

Another question. Shake tells me to change the import here:

import Mathlib.Algebra.Module.Submodule.Basic

@[gcongr] protected alias ⟨_, GCongr.Submodule.toAddSubgroup_le⟩ := Submodule.toAddSubgroup_le

(that's the entire file) from ...Submodule.Basic to ...Submodule.Defs but Submodule.toAddSubgroup_le is defined in Mathlib.Algebra.Module.Submodule.Basic. So aliases are also problematic for shake?

Is there a list of known issues?

[Kevin Buzzard]

(I know that it has problems with tactic imports)

[Kevin Buzzard]

Some of these are subtle: I removed an import of a random maths file and a proof broke and the fix was to import Mathlib.Tactic.Have! Somehow some of have's syntax was missing. But I guess this is expected behaviour for me. The simp breakage was the only really surprising thing.

[Michael Rothgang]

Mathlib.Tactic.Have defines stream-of-conscioudness have, which mathlib deprecates

[Kevin Buzzard]

The only other thing which looked like a bug to me was that in the file FLT.Mathlib.GroupTheory.Index which starts import Mathlib.GroupTheory.Index and then only contains notation, shake tells me

././././FLT/Mathlib/GroupTheory/Index.lean:
  remove #[Init, Mathlib.GroupTheory.Index]
  add #[Init.Prelude]

and it was the occurrence of Init which surprised me.

[Kevin Buzzard]

Aah so in fact I shouldn't be importing Mathlib.Tactic.Have at all?

[Michael Rothgang]

Mathlib has a syntax linter against that, you can add that to the FLT lakefile

[Kevin Buzzard]

I'm in the middle of something else but I'll add it to the linter tracking issue :-)

[Damiano Testa]

Yaël Dillies said:

If anything, creating notation-only files makes the issue worse!

Maybe syntax-only files should be added to the list of noshake files that shake always ignores, instead of ignoring them every single time in every file that imports them.

[Yaël Dillies]

Sure, that's an option too

[Yaël Dillies]

Kevin Buzzard said:

My main motivation really is to stop people sneakily adding import Mathlib to the repo and thus doubling the amount of mathlib docs we have to build.

I agree with the feeling, but do be aware that:

• not importing all of mathlib means that the FLT docs will be incomplete. In practice, this seems to only be a problem when someone is working on something new importing things that haven't been imported in FLT previously.
• Since docs are cached with a key depending on lake-manifest.json only, the cost of building extra docs is only paid once every time you bump mathlib.

[Kevin Buzzard]

I don't really understand what you mean by the cost of extra docs. CI takes a long time precisely because it's building half of mathlib's docs every time, right?

[Yaël Dillies]

If it does, then something is wrong! Documentation for mathlib is cached, and the cache is cleared only when you bump mathlib.

[Yaël Dillies]

Something I have noticed is that it takes a long time to replay files that have already been built (ie whose docs have already been generated). It doesn't take as long as when building the files the first time, but still not as instantaneous as expected. This is something I've been wanting to investigate.

[Damiano Testa]

This discussion makes me wonder: why does shake not flag as unused the imports of deprecated modules?

[Damiano Testa]

Maybe it is because Shake skips import-only modules, and deprecated modules count as "import-only", since they only contain a deprecation, which does not add declarations to the environment!

[Mario Carneiro]

Yaël Dillies said:

But shake is supposedly extremely stable :sweat_smile:

Note, I haven't touched shake in ~6 months

[Mario Carneiro]

Kevin Buzzard said:

Is there a recommended way of keeping track of various reasons that shake was "wrong" about imports?

you can put a comment on the import line in the downstream file, if it's a one-off. If it's a file which is always a false positive (e.g. a notation-only file) I would put the comment in that file

[Kim Morrison]

Perhaps a reasonable feature for shake would be to warn you if it proposed removing an import which has a comment on the same line.