Zulip Chat Archive

Stream: general

Topic: debug symbols


view this post on Zulip Björn Fischer (Jul 29 2019 at 16:23):

Given some name, can I (if applicable) find its definition location (lean file and line(s)) using a tactic or by some other means?

view this post on Zulip Jeremy Avigad (Jul 29 2019 at 16:28):

In VSCode, I usually type e.g. #check nat.add, then right-click on nat.add and choose "Go to Definition". Similar things work for notation.

view this post on Zulip Johan Commelin (Jul 29 2019 at 16:38):

Also in VScode: Ctrl-click on a symbol. and #print some_name will print the full term definition (can be ugly). Finally Ctrl-T will allow you to search (with completion) for names in the library.

view this post on Zulip Björn Fischer (Jul 29 2019 at 16:38):

Thanks @Jeremy Avigad I need this for automation, though. I want to import definitions (by their name) into Latex listings without having to copy/paste.

FYI: In VSCode you can also lookup definitions by typing Ctrl+P and then #nat.add.

view this post on Zulip Rob Lewis (Jul 29 2019 at 17:12):

There's environment.decl_olean and environment.decl_pos.

view this post on Zulip Björn Fischer (Jul 30 2019 at 11:20):

@Rob Lewis Thanks! Exactly what I'm looking for.

Follow up question: I've noticed that Lean (surprisingly) prints warnings to stdout. Can this be disabled or changed to stderr? I've tried --quiet.

view this post on Zulip Floris van Doorn (Jul 30 2019 at 13:58):

FYI: In VSCode you can also lookup definitions by typing Ctrl+P and then #nat.add.

Nice! I didn't know this. That sounds incredibly useful if you're in a file which you don't want to modify.


Last updated: May 08 2021 at 10:12 UTC