GAUTAM

Stream: new members

[GAUTAM]

I am new to Lean. When I try to run a simple code on VScode, it says that I don't have the extension for debugging plain text. What should I do?

[Shreyas Srinivas]

GAUTAM said:

I am new to Lean. When I try to run a simple code on VScode, it says that I don't have the extension for debugging plain text. What should I do?

This is not the right stream for this question. Please open a thread on the #new members stream.

[Notification Bot]

2 messages were moved here from #lean4 > apply instance check fails at reducible transparency by Eric Wieser.

[Julian Berman]

@GAUTAM what instructions did you follow to set up lean, and what OS are you on?

[GAUTAM]

I use Mac OS Monterey 12.7.1.
I am not able to find the extension for debugging lean4 on VScode

[Julian Berman]

Then you should follow https://leanprover-community.github.io/install/macos.html which should walk you through installing everything you need essentially

[Mauricio Collares]

@GAUTAM You're not doing anything wrong, there is no extension for debugging Lean code (in the DAP sense, as in https://code.visualstudio.com/api/extension-guides/debugger-extension) at the moment. This also implies you cannot run Lean programs by pressing F5 or Ctrl-F5 in VSCode, if I understand correctly. You can run them by manually invoking lake inside VSCode's terminal.

[Mauricio Collares]

That being said, writing Lean code is a highly interactive process with the standard VSCode Lean4 extension, and with it you can #eval stuff to run snippets of code.

[GAUTAM]

Thank you very much.