Zulip Chat Archive

Stream: general

Topic: filename tactic

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.

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?

Scott Morrison (Apr 19 2020 at 02:40):

Have a look at env.decl_olean decl_name.

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.

Scott Morrison (Apr 19 2020 at 02:41):

Actually, read the linters, they must do this.

Reid Barton (Apr 19 2020 at 02:41):

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

Scott Morrison (Apr 19 2020 at 02:41):

Seems so, it only uses env.decl_olean.

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:

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.

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)

Scott Morrison (Apr 19 2020 at 02:45):

Ah!

Reid Barton (Apr 19 2020 at 02:45):

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

Reid Barton (Apr 19 2020 at 02:45):

decl_pos also returns nothing

Jason Rute (Apr 19 2020 at 02:46):

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

Reid Barton (Apr 19 2020 at 02:46):

Yes, where you could put a top-level command

Reid Barton (Apr 19 2020 at 02:48):

For example, #eval false

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

Reid Barton (Apr 19 2020 at 02:54):

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

Reid Barton (Apr 19 2020 at 02:54):

then use a tactic which invokes trace

Reid Barton (Apr 19 2020 at 02:54):

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

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.

Reid Barton (Apr 19 2020 at 02:57):

Are you using lean --make?

Reid Barton (Apr 19 2020 at 02:57):

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

Jason Rute (Apr 19 2020 at 03:01):

Probably lean filename or lean --make filename.

Jason Rute (Apr 19 2020 at 03:01):

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

Reid Barton (Apr 19 2020 at 03:04):

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

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: Dec 20 2023 at 11:08 UTC