LeanInk regression on v4.3.0-rc1

Stream: lean4

[Utensil Song]

LeanInk terminates on v4.3.0-rc1 for

import Mathlib.Tactic

#help tactic

with

% lake env leanInk analyze examples/Help.lean
Starting Analysis for: "examples/Help.lean"
libc++abi: terminating due to uncaught exception of type lean::exception: incomplete case

It was OK on v4.2.0-rc3.

Any idea how to debug this?

[Utensil Song]

I also want to test it with v4.2.0-rc4 but I don't know how to align all deps of Mathlib back to when it was using v4.2.0-rc4 except manually copy the manifest from the commit when Mathlib was using them.

UPDATE: It's also OK on v4.2.0-rc4.

[Utensil Song]

By manually bisecting the imports, the new #mwe is only

import Mathlib.Init.Logic

then

lake env leanInk analyze examples/Help.lean

crashes silently (return code 139) while the imports of Mathlib.Init.Logic don't cause the crash.

[Scott Morrison]

I'm a bit confused by what you are doing. Are you certain that you're using LeanInk and Mathlib at the same toolchain?

[Utensil Song]

Further minimized to:

import Mathlib.Tactic.Relation.Symm

attribute [symm] Eq.symm

now it reports

% lake env lean --version
Lean (version 4.3.0-rc1, commit baa4b68a7192, Release)
% lake env leanInk analyze examples/Help.lean
Starting Analysis for: "examples/Help.lean"
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: loose bvar in expression

caused by only the last line (not the import).

[Utensil Song]

Scott Morrison said:

I'm a bit confused by what you are doing. Are you certain that you're using LeanInk and Mathlib at the same toolchain?

Does lake env leanInk guarantee this? Besides local test, I'm also running this on CI which has only one toolchain.

[Utensil Song]

The (personal) consequence is that most of my non-trivial Lean files (the ones commented out below) can't be analyzed by LeanInk on v4.3.0-rc1.

image.png

[Mario Carneiro]

Utensil Song said:

Scott Morrison said:

I'm a bit confused by what you are doing. Are you certain that you're using LeanInk and Mathlib at the same toolchain?

Does lake env leanInk guarantee this? Besides local test, I'm also running this on CI which has only one toolchain.

No, if you compiled leanInk previously on an old toolchain then you can get ABI mismatches

[Utensil Song]

On CI, I can see the only toolchain is compiling LeanInk, and the analysis panics and gives the trace: https://github.com/utensil/lean-playground/actions/runs/6728771542/job/18288590308#step:5:219

PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:317:22: loose bvar in expression
Starting Analysis for: "examples/Help.lean"
backtrace:
leanInk(lean_panic_fn+0x9e)[0x5612d567da8e]
leanInk(l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3+0x103a)[0x5612d376d5ea]
leanInk(l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_reduceUntilBadKey_step+0xc4)[0x5612d36c6754]
leanInk(l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_reduceUntilBadKey+0xbd)[0x5612d36c74cd]
leanInk(l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_pushArgs+0x1d9)[0x5612d36c8d09]
leanInk(l_Lean_Meta_DiscrTree_mkPathAux+0x201)[0x5612d36cafc1]
leanInk(l_Lean_Meta_DiscrTree_mkPath+0x2d5)[0x5612d36cb705]
leanInk(+0x352d84f)[0x5612d568784f]
leanInk(+0xb40724)[0x5612d2c9a724]
leanInk(+0xb3e9a0)[0x5612d2c989a0]
leanInk(+0xb40a62)[0x5612d2c9aa62]
leanInk(+0xb3e9a0)[0x5612d2c989a0]
leanInk(+0xb42573)[0x5612d2c9c573]
leanInk(+0xb3b3b1)[0x5612d2c953b1]
leanInk(+0xb421f7)[0x5612d2c9c1f7]
leanInk(+0xb41ecd)[0x5612d2c9becd]
leanInk(lean_apply_6+0x6be)[0x5612d568c4fe]

...more...

[Mario Carneiro]

If the leanInk repo contains an old lean-toolchain, it would use that toolchain even in CI, assuming your CI script downloads the git repo and calls lake build

[Mario Carneiro]

https://github.com/leanprover/LeanInk/blob/main/lean-toolchain

[Utensil Song]

Yes, the toolchain in LeanInk is pretty old, but this is not the issue, because it works fine on v4.2.0-rc4.

[Mario Carneiro]

I'm not sure how that follows

[Mario Carneiro]

any lean version can introduce ABI breaks, and the effects of this on compiled programs is unpredictable

[Utensil Song]

Assuming the issue is caused by that the LeanInk is compiled by leanprover/lean4:nightly-2023-08-19 and Mathlib is compiled by v4.3.0-rc1, because when it works fine when Mathlib is compiled by v4.2.0-rc4, then the conclusion is either:

1. v4.3.0-rc1 introduces some ABI change, now LeanInk with lean4:nightly-2023-08-19 starts crashing
2. v4.3.0-rc1 itself has some issues to cause crash, only happen to be triggered by LeanInk, no matter which version it was compiled

If it's case 1, then LeanInk would have to update its toolchain, and maybe it's all OK again.

I'm more concerned if it's case 2.

[Mario Carneiro]

you would have to fix 1 before you can determine whether 2 is the case

[Utensil Song]

Indeed, I bumped LeanInk to v4.3.0-rc1, and now it works. Case 1 it is. Thanks!

[Utensil Song]

@Henrik Böving The same ABI break might bite doc-gen4 too when it's bumped to v4.3.0-rc1 if LeanInk repo is still leanprover/lean4:nightly-2023-08-19. The bump is better to happen along with doc-gen4 bump?

[Mario Carneiro]

I think doc-gen links with LeanInk, so it has to recompile it anyway (with the current toolchain, not leanInk's)

[Henrik Böving]

Correct, shouldn't affect me.