Stream: Coq devs & plugin devs

Topic: Getting the path of the current file


view this post on Zulip Arpan Agrawal (Feb 13 2023 at 19:13):

Hi,

I have an unusual problem, I want to get the path of the file where a certain custom tactic is being called. I tried doing

Names.ModPath.to_string (Lib.current_mp ())

but this results in "Plugin.Test" instead of the path, which is theories/Test.v

Can someone help me with this?
Thanks!

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:16):

Just bumping this. We are building a plugin to interface between Coq and a machine learning tool. We need the full path of the file so we can call the machine learning tool. Is there a way to get the full file path for the file within a plugin? I'd thought it'd be the dirpath or something, not sure if there's a place to access that within a plugin, and if it's what I think it is?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:18):

@Talia Ringer what Coq version are you?

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:18):

I think 8.15, is that right @Arpan Agrawal ?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:19):

But in general, to do this you need some hack, as of today Coq's standard document manager doesn't store that info, IIRC it is only parsed to the parser.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:19):

If you have access to the some data that has been parsed, then you can extract it from the location.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:19):

coq-lsp document manager indeed knows more about the workspace so you can query for this info

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:20):

[and actually abstracts away some other things that I just saw in your draft but will comment about that by mail]

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:20):

Ah I see, we had a hack but it's good to know the hack is justified. I think Arpan is getting it from the call to coqc right now, but the method fails when it's opened in an IDE which is important to us

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:20):

given an Ast, location is in the loc field

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:21):

@Talia Ringer is your plugin registering a command?

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:22):

yes (Arpan really wrote the plugin, just for credit's sake)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:22):

I agree it is actually silly Stm.doc doesn't store the file Uri, you can see a proposal for a more usable Coq document type here https://github.com/ejgallego/coq-lsp/blob/main/fleche/doc.mli

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:22):

then the command you have registered will allow you to access the file name

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:22):

ooooh how?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:22):

by means of loc in the mlg file

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:22):

omg

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:22):

haha i always wondered what that field was

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:23):

amazing, thanks

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:23):

Imagine you do this

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:23):

VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> { loc }

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:24):

:eyes:

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):

then loc is bound to the location of the command in the file

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):

HOWEVER

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):

here are the bad news

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):

IDEs may not set the filename

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:24):

does CoqIDE?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:25):

because the XML protocol doesn't include any notion of create document, so this is what CoqIDE does:

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:25):

I think if we are compatible with CoqIDE and maybe Proof General, that should be enough to start. Or we can just have an Option that we make people set with the path if they're using an annoying IDE

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:26):

  let loc = { (initial ToplevelInput) with bp=off; line_nb; bol_pos } in

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:26):

So you are out of luck I'm afraid :(

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:26):

haha ouchhh

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:26):

Yeah so you will have to keep your hack

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:27):

Sorry about that

view this post on Zulip Talia Ringer (Feb 20 2023 at 22:27):

OK, thanks for at least confirming that

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:28):

Newer doc managers will hopefully solve many of your issues, and they can be backported to 8.15 or even later on, and more stable than SerAPI was

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:28):

In fact they are ready to use, but only became so very recently

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2023 at 22:29):

They even abstract the notion of build etc for you

view this post on Zulip Gaëtan Gilbert (Feb 20 2023 at 22:32):

what's the hack btw?

view this post on Zulip Arpan Agrawal (Feb 20 2023 at 22:53):

The hack I was using was to use the last argument from Sys.agrv, which on running dune build happens to be the filepath I need. Not sure how well it generalizes when called from files outside the dune project directory

view this post on Zulip Arpan Agrawal (Feb 20 2023 at 22:56):

And we're using Coq 8.16, in case that helps


Last updated: Mar 29 2024 at 06:39 UTC