exact? crashes

Stream: mathlib4

[Kalle Kytölä]

I have not experienced this behavior before: exact? just crashes in the following (somewhat minimized but maybe not fully). I suspect I may have borked my Lean somehow. But to make sure, can someone reproduce this?

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.LibrarySearch

example (x : ℝ) : x = 1 * x := by
  exact?
  -- Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: incomplete case
  sorry

In a VS Code pop-up box I get the error:

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::exception: incomplete case

In the "Output" box there is a long list of errors of the form:

Lean (version 4.0.0-nightly-2023-08-15, commit b5a736708f40, Release)
libc++abi: terminating due to uncaught exception of type lean::exception: incomplete case
[Error - 11:22:27 PM] Request textDocument/codeAction failed.
Message: Server process for file:///.../Test.lean crashed, likely due to a stack overflow or a bug.
Code: -32902
[Error - 11:22:27 PM] Request textDocument/foldingRange failed.
Message: Server process for file:///.../Test.lean crashed, likely due to a stack overflow or a bug.
Code: -32902
[Error - 11:22:27 PM] Request textDocument/documentSymbol failed.
Message: Server process for file:///.../Test.lean crashed, likely due to a stack overflow or a bug.
Code: -32902

[Jireh Loreaux]

Have you tried restarting the Lean server?

[Kalle Kytölä]

Yes, there was a VS Code pop-up box also for that and I did it several times. I also closed VS Code and reopened. I even rebooted and reran lake exe cache get! to try to make sure it is not a borked cache.

The error persists on my machine.

[Jireh Loreaux]

IIRC Scott reversed the priority of matching lemmas, in that ones that are "more specific" appear first, and others are tried last. In this case, you have a very generic lemma (the head symbol is just HAdd.hadd), which means it could potentially match many things, and maybe that's causing the problem.

[Jireh Loreaux]

I'll try it in a minute.

[Jireh Loreaux]

Works for me instantly.

[Kalle Kytölä]

Ok, I suspect I have indeed borked something... Thank you!

I will see if I can reproduce in a fresh project.

[Jireh Loreaux]

Maybe there's a problem with the library search cache file. You could try lake exe cache get!

[Kalle Kytölä]

I did. It didn't help.

[Jireh Loreaux]

oops, sorry you said that.

[Kalle Kytölä]

Oh, it works for me, too, on a fresh project. So I must just have borked the config of the particular project that I was working in.

Thank you @Jireh Loreaux!

[Kalle Kytölä]

And sorry for the noise!

[Kalle Kytölä]

I'm resisting the temptation to "mark the topic as resolved". :grinning_face_with_smiling_eyes:

[Kalle Kytölä]

Ok, if anyone else ever manages to create a mess of the same kind as I did, then this fixes the project:

• delete lake-packages and build directories of the project
• (run lake update and copy the lake-packages/mathlib/lean-toolchain to project root directory --- these are perhaps unnecessary, but I did these out of habit)
• run lake exe cache get!

[Kalle Kytölä]

That fix seems embarrassingly predictable and routine. I think I was thrown off by (1) lake exe cache get! not fixing the problem without me deleting the directories and (2) that exact? was still closing some goals (which may have all been rfl, come think of it now).