CI errors that are not local errors

Stream: mathlib4

[Matthew Ballard]

Do we want this? I would like to be fairly confident that if it builds and lints on my machine then CI will happy.

The example I got bit by was says

[Kevin Buzzard]

By "lints on my machine" you presumably don't mean "I added some stuff to one file and #lint was happy"?

[Matthew Ballard]

if lake build and lake exe runLinter mathlib are happy on my machine I would very much hope they are on other machines

[Kevin Buzzard]

I was just observing that mathlib linting is much more then "put #lint at the bottom of the file" but it looks like you're running more than that (presumably you're running what CI runs)

[Mario Carneiro]

says is about whether the says.verify option is enabled, which is currently true for CI and false for local use, hence the issue

[Mario Carneiro]

this is mostly orthogonal to linting

[Mario Carneiro]

This was one of the reasons I was against using says in the library BTW

[Mario Carneiro]

it's all well and good to have the mechanism, but actually using it in mathlib means more text on screen and more runtime, both in CI and locally, unless you disable says.verify locally and then you miss errors that appear in CI as mentioned here. I see only downsides

[Matthew Ballard]

Hard error or not. I can be swayed. I think inconsistent behavior between CI and local has no benefits.

[Mario Carneiro]

I think to some extent we should expect differences; most people are not going to be running shake, runLinter and lean4checker locally

[Mario Carneiro]

of course it's possible for you to mimic a CI run locally, but I think it's okay if we optimize the in-editor experience for fast iteration over full checking

[Mario Carneiro]

in fact I'd love it if we got that quick-and-dirty option so that we can just skip proofs in the file we don't care about

[Matthew Ballard]

Sure. (I only care about lake build and lake exe runLinter Mathlib locally.) _If_ you choose to run something locally, you should expect non-divergent behavior in CI.

[Mario Carneiro]

are you willing to take lake build -KCI as an option?

[Matthew Ballard]

I did not know about that. What does it do beside turn this on?

[Eric Rodriguez]

I think says.verify is a bad option that shoudp almost never be on

[Mario Carneiro]

I agree, it kind of defeats the purpose

[Mario Carneiro]

but people were concerned about the hints going out of date

[Mario Carneiro]

or if it suggests more or less than it used to

[Mario Carneiro]

but in those cases I think it's fine to just let it go out of date

[Matthew Ballard]

Is says.verify the only difference with the -KCI flag?

[Mario Carneiro]

actually it appears says.verify does not use the -KCI flag; if you use the default settings then it checks the CI environment variable during elaboration. So you have to do CI=true lake build instead

[Yaël Dillies]

Here's one CI error which I'm not managing to reproduce locally: https://github.com/leanprover-community/mathlib4/actions/runs/7869281349/job/21468075433

[Yaël Dillies]

I would be interested to even know where it is coming from.

[Ruben Van de Velde]

PANIC at Lean.MapDeclarationExtension.insert Lean.Environment:607:2: assertion violation: env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`

[Mario Carneiro]

that means you are adding an attribute/extension entry for a declaration not in the current module

[Mario Carneiro]

most attributes catch this in order to present a better error message (that also makes people sad), this is what happens if you don't

[Mario Carneiro]

I am reproducing it locally

[Mario Carneiro]

remember that panics show a popup and appear in the Output > "Lean: Editor" panel, not as red squiggles

[Mario Carneiro]

the culprit is

add_decl_doc AddMonoidHom.map_zero

[Mario Carneiro]

which should be relocated to the same file as the declaration

[Mario Carneiro]

(you can also use the @[to_additive "declaration doc here"] form to add a doc on the additive version of a declaration)

[Yaël Dillies]

Yeah I know about this, but it was very very hard to edit this file because the LSP server becomes unusably slow when there's >= 30 errors in the file (is this a known issue? I've been encountering it a lot).

[Mario Carneiro]

lean4#3311