Zulip Chat Archive

Stream: general

Topic: filename tactic


view this post on Zulip Jason Rute (Apr 19 2020 at 01:48):

Is there a tactic (or way to write a tactic) which returns the filename (and line/col number would be better) of the file it is being run in? I want the file to be the entry point file with the begin ... end block or by block. This might be too much to ask for, but it doesn't hurt to ask.

view this post on Zulip Jason Rute (Apr 19 2020 at 01:55):

If that is not possible or even if it is: Is there a way to label traces with the filename (when being run from the command line). The error messages are labeled with the file name, e.g.:

/tmp/tmp_lean_project/src/test.lean:3:0: error: tactic failed, there are unsolved goals
state:
⊢ true

Can one do the same for traces?

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:40):

Have a look at env.decl_olean decl_name.

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:40):

That requires that you know a declaration made in the current file. Hopefully there is something better.

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:41):

Actually, read the linters, they must do this.

view this post on Zulip Reid Barton (Apr 19 2020 at 02:41):

But it doesn't return anything for declarations in the current file.

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:41):

Seems so, it only uses env.decl_olean.

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:43):

I mean, as a terrible hack you can synthesize a new declaration, then use decl_olean to find the file it was defined in... :nauseated:

view this post on Zulip Reid Barton (Apr 19 2020 at 02:44):

I thought about trying to generate a warning, since those are also labelled with the position, but I couldn't figure out a way to make it happen. If you were at top level, it would be doable.

view this post on Zulip Reid Barton (Apr 19 2020 at 02:45):

Scott Morrison said:

I mean, as a terrible hack you can synthesize a new declaration, then use decl_olean to find the file it was defined in... :nauseated:

I tried this and it doesn't work because there is no location information for declarations in the current file (the name decl_olean is a hint)

view this post on Zulip Scott Morrison (Apr 19 2020 at 02:45):

Ah!

view this post on Zulip Reid Barton (Apr 19 2020 at 02:45):

though I don't see why Lean couldn't provide it in principle

view this post on Zulip Reid Barton (Apr 19 2020 at 02:45):

decl_pos also returns nothing

view this post on Zulip Jason Rute (Apr 19 2020 at 02:46):

What does "top level" mean here? Outside of any definition, theorem, etc?

view this post on Zulip Reid Barton (Apr 19 2020 at 02:46):

Yes, where you could put a top-level command

view this post on Zulip Reid Barton (Apr 19 2020 at 02:48):

For example, #eval false

view this post on Zulip Reid Barton (Apr 19 2020 at 02:53):

Hmm, thinking outside the box, if you're willing to interact with Lean through the server interface, you could obtain location information that way

view this post on Zulip Reid Barton (Apr 19 2020 at 02:54):

It can be as simple as feeding Lean the whole file as a batch

view this post on Zulip Reid Barton (Apr 19 2020 at 02:54):

then use a tactic which invokes trace

view this post on Zulip Reid Barton (Apr 19 2020 at 02:54):

Our editors know where to put the trace, so it must be in the server output

view this post on Zulip Jason Rute (Apr 19 2020 at 02:55):

Yeah, what I'm working on now isn't using the server. Worse case, I can run each file individually.

view this post on Zulip Reid Barton (Apr 19 2020 at 02:57):

Are you using lean --make?

view this post on Zulip Reid Barton (Apr 19 2020 at 02:57):

I don't know whether it is compatible with --server

view this post on Zulip Jason Rute (Apr 19 2020 at 03:01):

Probably lean filename or lean --make filename.

view this post on Zulip Jason Rute (Apr 19 2020 at 03:01):

Curious, how do you add warnings at the top level?

view this post on Zulip Reid Barton (Apr 19 2020 at 03:04):

#eval false was an example. I'm not sure if you can avoid the extraneous output.

view this post on Zulip Mario Carneiro (Apr 19 2020 at 03:06):

you can use lean --run to read a lean file and put #eval main at the bottom


Last updated: May 15 2021 at 22:14 UTC