lean4checker failure

Stream: lean4

[Ruben Van de Velde]

lean4checker found a problem in Mathlib.Geometry.Manifold.BumpFunction

[Kim Morrison]

% lake env lean4checker/.lake/build/bin/lean4checker Mathlib.Geometry.Manifold.BumpFunction
lean4checker found a problem in Mathlib.Geometry.Manifold.BumpFunction
uncaught exception: parser 'subscript' was not found

[Kim Morrison]

I'm guessing that is referring to the parser from Mathlib.Util.Superscript

[Kim Morrison]

It's nothing about the contents of Mathlib.Geometry.Manifold.BumpFunction that causes the problem: an otherwise empty file containing import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension fails lean4checker.

[Kim Morrison]

Walking down the graph a bit, import Mathlib.Analysis.InnerProductSpace.PiL2 is sufficient to fail lean4checker.

[Kim Morrison]

Note that that file then contains import Mathlib.Util.Superscript.

[Kim Morrison]

Indeed, stripping down to A.lean containing:

import Mathlib.Util.Superscript

syntax (name := PiLp.vecNotation) "!" noWs subscript(term) noWs "[" term,* "]" : term
macro_rules | `(!$p:subscript[$e:term,*]) => do
  let n := e.getElems.size
  `((WithLp.equiv $p <| ∀ _ : Fin $(Lean.Quote.quote n), _).symm ![$e,*])

and B.lean containing import Mathlib.A results in

% lake build Mathlib.B && lake env lean4checker/.lake/build/bin/lean4checker Mathlib.B
Build completed successfully.
lean4checker found a problem in Mathlib.B
uncaught exception: parser 'subscript' was not found

[Kim Morrison]

However, it's not immediately occurring to me what change in v4.15.0-rc1 has caused this. Ideas very welcome!

[Kim Morrison]

(Lesson: we need to be running lean4checker against nightly-testing, too!)

[Yaël Dillies]

Ah shoot, I am giving a talk on thursday about how to run a Lean project, and I am planning on showing https://yaeldillies.github.io/LeanCamCombi/upstreaming, but the page is currently not building because of the above doc-gen error

[Yaël Dillies]

I guess I'll strip doc-gen from LeanCamCombi for now

[Johan Commelin]

@Mario Carneiro @Kyle Miller @Eric Wieser Do you see anything suspicious about the MWE that Kim produced for the leanchecker failure?
See https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/lean4checker.20failure/near/485829507 above.

[Mario Carneiro]

I think this is not the first time this issue has been reported

[Mario Carneiro]

I forget what the resolution was though. I think it has something to do with not running enableInitializersExecution?

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Non-builtin.20parser.20aliases/near/483369623

[Kim Morrison]

I can sprinkle enableInitializersExecution in lean4checker, but ... I'm not too happy about doing so without understanding what changed in v4.15.0-rc1. It seems likely that it is Sebastian's changes in preparation for async elaboration.

[Eric Wieser]

Did the PiL2 change land before or after v4.14.0?

[Eric Wieser]

I just checked: it landed after

[Eric Wieser]

So what changed here is "mathlib started calling (an unfolded version of, #19009) register_parser_alias"

[Kim Morrison]

@Eric Wieser, sorry, does this mean you know what we should do? :-)

[Eric Wieser]

I think the resolution is do the sprinkling you describe

[Eric Wieser]

I don't think there is a Lean regression here to worry about, just a latent sharp edge that mathlib now builds upon

[Eric Wieser]

Maybe longer term a different initialization mechanism is needed to handle parser aliases, or parser aliases need to switch to a different registration mechanism

[Mario Carneiro]

I'm kind of against running initializers in lean4checker and lean4lean. I don't want arbitrary code running in my kernel rechecker

[Mario Carneiro]

lean4lean shows the same behavior, and it seems the culprit is src#Lean.finalizeImport calling finalizePersistentExtensions with no option to skip it

[Mario Carneiro]

by the way the macro rules is not necessary, this suffices in A.lean:

import Mathlib.Util.Superscript

syntax "foo" subscript(term) : term

[Mario Carneiro]

I think I have narrowed down the error to this line, which is doing something questionable: it is in the ImportM monad which has an environment in it, but rather than using that environment to look up the parser alias it is consulting parserAliasesRef which is an IO.Ref not a priori related to the environment. In the setting of lean4checker this IO.Ref will be an empty map because initializes have not been run. This only happens for parser aliases, not regular parser references, because these are looked up properly in the environment.

[Mario Carneiro]

the consequence of this is that effectively, all parser aliases must be built in. The error is the combination of:

• declaring a parser alias
• outside of lean core
• and trying to import the resulting file outside of a lean elaborator process

[Mario Carneiro]

Shall I move all the discussion above to #lean4 so I can ping @Sebastian Ullrich ?

[Notification Bot]

31 messages were moved here from #mathlib reviewers > lean4checker failure by Kim Morrison.

[Kim Morrison]

@Sebastian Ullrich

[Kim Morrison]

#19735 "chore: run lean4checker on most recent nightly-testing-YYYY-MM-DD tag", is perhaps "after the horse has bolted", but may help next time!

[Eric Wieser]

I think the actual problem here was that the offending PR landed on the same day as the Lean bump, and the nightly leanchecker run didn't distinguish the two?

[Eric Wieser]

While maybe the extra run is a good idea anyway, I don't think it would have had any effect here.

[Kim Morrison]

Eric Wieser said:

I think the actual problem here was that the offending PR landed on the same day as the Lean bump, and the nightly leanchecker run didn't distinguish the two?

Ah, thanks, I was still under the misapprehension that the Mathlib change had come earlier.

[Kevin Buzzard]

And there could of course be more horses waiting to bolt!

[Yaël Dillies]

I'm reading this thread again and I can't understand whether the issue was fixed or not? Was it fixed?

[Yaël Dillies]

Context is that it prevents me from building the docs for LeanCamCombi, which incidentally is now quoted here on the website of an additive combinatorics course in ETH

[Kim Morrison]

My understanding is that it hasn't been fixed.

[Eric Wieser]

Why does this prevent a doc build?

[Eric Wieser]

Mario has a reasonable objections to enableInitializersExecution in leanchecker, but presumably doc-gen can/already does call it?

[Eric Wieser]

Looks like the mathlib docs are also no longer building, so I guess it doesn't call it.

[Eric Wieser]

Mario suggested a workaround to me privately, which is to add def subscriptTerm := subscriptParser termParser or similar, and avoid the subscript(term) parser alias

[Yaël Dillies]

Eric, here is the incriminating CI error

[Eric Wieser]

Yes, this error appears in every program that tries to be a Lean interpreter, of which both leanchecker and doc-gen are examples. I claim here the bug is in doc-gen.

[Eric Wieser]

https://github.com/leanprover/doc-gen4/pull/243 should hopefully fix doc-gen

[Henrik Böving]

https://github.com/leanprover-community/mathlib4_docs/actions/runs/12231240463/job/34113912187 doesn't seem to get picked up by a runner anymore

[Moritz Firsching]

I think I'm seeing an instance of this failure here:
https://github.com/mo271/FormalBook/actions/runs/12239032320/job/34138491509?pr=84
doc-gen4 was failing to build before I pulled in the latest changes fixing it there, and now the problem happens when the ci runs

lake exe checkdecls blueprint/lean_decls

[Bryan Gin-ge Chen]

Henrik Böving said:

https://github.com/leanprover-community/mathlib4_docs/actions/runs/12231240463/job/34113912187 doesn't seem to get picked up by a runner anymore

It looks like the reason is that the hoskinson9 runner went offline at some point. cc: @Wojciech Nawrocki

For now I've applied the doc-gen tag to the hoskinson5 runner, so hopefully it should work now.

[Bryan Gin-ge Chen]

The run seems to have failed: https://github.com/leanprover-community/doc-gen/actions/runs/12221600715/job/34090851796

Maybe there's something missing on the runner?

[Henrik Böving]

Why are we still running doc-gen3 jobs?

[Henrik Böving]

Also the mathlib4 runners are still not picking up, I can try to schedule another run

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Bryan Gin-ge Chen said:

Henrik Böving said:

https://github.com/leanprover-community/mathlib4_docs/actions/runs/12231240463/job/34113912187 doesn't seem to get picked up by a runner anymore

It looks like the reason is that the hoskinson9 runner went offline at some point. cc: Wojciech Nawrocki

For now I've applied the doc-gen tag to the hoskinson5 runner, so hopefully it should work now.

Just restarted hoskinson9

[Henrik Böving]

9 picked up the doc-gen job

[Bryan Gin-ge Chen]

Whoops I didn't even notice it was a doc-gen3 job. I've turned those off for now.

[Pietro Monticone]

This might be related lean4checker found a problem in equational_theories

https://github.com/teorth/equational_theories/actions/runs/12469938951/job/34804098470?pr=970#step:8:28