symbol lookup error, likely due to a stack overflow or a bug.

[tribbloid]

Here is the error information when running code inspection in VSCode (with everything else installed automatically by elan):

/home/peng/git-release/__MATH/SciLean> lean --version
Lean (version 4.11.0-rc1, x86_64-unknown-linux-gnu, commit daa22187642d, Release)
/home/peng/git-release/__MATH/SciLean> lake --version
Lake version 5.0.0-daa2218 (Lean version 4.11.0-rc1)
/home/peng/.elan/toolchains/leanprover--lean4---v4.11.0-rc1/bin/lean: symbol lookup error: ././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.so: undefined symbol: l_Lean_Server_RequestM_readDoc___at_Lean_Server_RequestM_withWaitFindSnapAtPos___spec__1
[Error - 20:53:35] Request textDocument/documentSymbol failed.
  Message: Server process for file:///home/peng/git-release/__MATH/SciLean/examples/HarmonicOscillator.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902 
[Error - 20:53:35] Request textDocument/codeAction failed.
  Message: Server process for file:///home/peng/git-release/__MATH/SciLean/examples/HarmonicOscillator.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902 
[Error - 20:53:35] Request textDocument/documentSymbol failed.
  Message: Server process for file:///home/peng/git-release/__MATH/SciLean/examples/HarmonicOscillator.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902 

Should we upgrade the recommended lean toolchain version to avoid it?

[lecopivo]

Sorry I was doing some major changes to the library and lots of things are broken right now. I will fix it tomorrow and make sure that the example works.

[lecopivo]

I have never seen the above error and have no idea how to fix it.

[lecopivo]

For now you can use this commit which had successful CI run

af67d94