VSCode "Go to definition" on M1 Mac

Stream: new members

[Martin C. Martin]

I have an M1 Macbook Air. I installed Lean using these instructions, that say to do everything under arch -x86_64 and use rosetta.

I have a recent VS Code, and the lean plugin for it. However, when trying to use "Go to definition" in VS Code, it sometimes says "No definition found", other times it takes me to the wrong place, like the definition of rw or exact. Sometimes it takes me to the right place.

From order/liminf_limsup.lean

How can I debug this?

[Ruben Van de Velde]

Mm, I've run into it taking me to the wrong place as well on linux, like ending up somewhere in lean core from a local hypothesis called pp, so it might not be specific to you. Not sure I even had "no definition found"

[Martin C. Martin]

Yeah, for example on line 97 of that same file, order/liminf_limsup.lean, if I double click eventually_map and hit F12, it takes me to the definition of rw in interactive.lean, as you say that's in the lean core.

[Yaël Dillies]

@Eric Wieser, isn't that due to the codepoint counting mismatch?

[Eric Rodriguez]

Martin has the new version, Yael

[Patrick Massot]

The "Go to definition" operation has never been 100% reliable.

[Martin C. Martin]

When it takes me to lean core, it's generally something higher up in the parse tree, or at least what I imagine the parse tree to be. For example, on line 464, if I try exists_lt_of_lt_cSup, it takes me to obtain, which is probably 40 tokens earlier on the line above. But exists_lt_of_lt_cSup is the start of the body of the obtain.

[Arthur Paulino]

I noticed that too, but for me, "Go to definition" is much better in Lean 4, so maybe it's one of those details that are hard to get precisely right in Lean 3 but is already solved in Lean 4 because of LSP

[Eric Rodriguez]

I'm not sure if anyone else gets this on M1 macs. I don't have an issue on mine, but I rebuild my Lean to be running on ARM-native so it's not directly comparable.

[Martin C. Martin]

Should I try recomputing the olean file for that source file? How do I do that?

[Martin C. Martin]

Is the olean format documented anywhere?