pp.beta, linter, "cannot evaluate ... in the same module"

Stream: mathlib4

[Kyle Miller]

After #7205 was merged, which added a pp.beta pretty printer option, people started reporting linter errors (for example here and here). In particular, this one:

info: [53/53] Linking runMathlibLinter
libc++abi: terminating due to uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'Lean.pp.beta' in the same module

[Kyle Miller]

The PR was reverted in #7774 and now I'm trying to reintroduce the option in #7910. This error is puzzling to me because the code in #7205 seemed fine: there was one module that added the pp.beta option along with a function to read its value, and then in another the option was actually used. For #7910, I moved this function into the second module to prevent the linter from failing (but I haven't looked into what the linter is doing).

[Kyle Miller]

Two and a half questions:

1. If #7910 is passing CI, is it fine to merge? Are there other linting environments out there where this will fail? I want to prevent the need to revert again.
2. Is this indicative of a bug in the linter?
3. (How did pp.beta manage to get merged by bors and then later cause linting issues?)

[Notification Bot]

Yaël Dillies has marked this topic as resolved.

[Kyle Miller]

(@Yaël Dillies Mis-click, or are you saying we need not worry about these questions? :wink:)

[Notification Bot]

Patrick Massot has marked this topic as unresolved.

[Sebastian Ullrich]

The exception suggests the linter binary is trying to execute imported code without having run enableInitializersExecution before importing

[Yaël Dillies]

Phone in wet pocket :sweat_smile:

[Oliver Nash]

I believe that the CI failures after #7205 were sporadic (I should be able to confirm this by digging through some old branches if that would help). Given this, I would hazard answers as follows:

1. Probably not
2. Unclear
3. We were (un)lucky on the CI runs for #7205