LetRec Error

Stream: lean4

[Farzad Jafarrahmani]

I’m encountering an error in a file that I’ve never modified. The file in question is LetRec.lean, located at

.elan\toolchains\leanprover--lean4---v4.16.0-rc2\src\lean\Lean\Elab\LetRec.lean  

The error occurs in the definition of elabLetRecDeclValueson line 95:

(mkInfoOnError := (pure <| mkBodyInfo view.valStx none))

Here is the error message:

invalid argument name 'mkInfoOnError' for function 'Lean.Elab.Term.withInfoContext'

Do you have any idea where this issue comes from and how I can resolve it?

Additionally, when I checked the definition of "elabLetRecDeclValues" on Lean’s GitHub repository (here), I found a different definition, and surprisingly this file was updated two years ago. Unless I’m missing something, shouldn't this issue be related to an outdated Lean version?

[Sebastian Ullrich]

Why are you rebuilding a Lean core file? I think you've already taken a wrong turn two steps before and need to tell us how you got there

[Farzad Jafarrahmani]

I was doing some metaprogramming exercises that I encountered an error in one my definition using let rec. Upon opening the LetRec file, I found that there was already an error present there. I then thought that perhaps my error is related to this pre-existing issue in the LetRec file.

[Sebastian Ullrich]

I can assure you that all files in a Lean release were built without errors. Probably your editor is using the wrong version of Lean to visit the file. Could you please post the output of the "Lean 4: Troubleshooting: Show Setup Information" VS Code command in that file?

[Robin Arnez]

This also happens on my machine regularly, it just seems like when you enter a toolchain file, then it has some wrong lean path with outdated olean files.

[Robin Arnez]

Maybe this has something to do with symlink differences between windows and linux? When I open VS code directly in my lean fork, I get

unknown module prefix 'Init'

No directory 'Init' or file 'Init.olean' in the search path entries:
c:\Users\robin\.elan\toolchains\lean4-stage0\..\stage1\lib\lean

because the .. on windows means c:\Users\robin\.elan\toolchains\stage1\lib\lean in contrast to linux where (I'm pretty sure) it resolves the symlink first and then takes the parent directory.

[Farzad Jafarrahmani]

Sebastian Ullrich said:

I can assure you that all files in a Lean release were built without errors. Probably your editor is using the wrong version of Lean to visit the file. Could you please post the output of the "Lean 4: Troubleshooting: Show Setup Information" VS Code command in that file?

Is the following what you mean?

Operating system: Windows_NT (release: 10.0.19045)
CPU architecture: x64
CPU model: 8 x 11th Gen Intel(R) Core(TM) i7-1185G7 @ 3.00GHz
Available RAM: 16.84 GB

VS Code version: Reasonably up-to-date (version: 1.97.2)
Lean 4 extension version: 0.0.195
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.14.0)
Project: Valid Lean project (path: c:\Users\f00879599\.elan\toolchains\leanprover--lean4---v4.16.0-rc2\src\lean)

---

Elan toolchains:

installed toolchains
--------------------

stable (default)
leanprover/lean4:v4.11.0-rc2
leanprover/lean4:v4.16.0-rc2


active toolchain
----------------

stable (default)

Lean (version 4.14.0, x86_64-w64-windows-gnu, commit 410fab728470, Release)

[Sebastian Ullrich]

It's strange that your project path starts with c: instead of C:, that is likely triggering a bug in elan. https://github.com/leanprover/elan/issues/161