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!
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?
@Talia Ringer what Coq version are you?
I think 8.15, is that right @Arpan Agrawal ?
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.
If you have access to the some data that has been parsed, then you can extract it from the location.
coq-lsp
document manager indeed knows more about the workspace so you can query for this info
[and actually abstracts away some other things that I just saw in your draft but will comment about that by mail]
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
given an Ast, location is in the loc
field
@Talia Ringer is your plugin registering a command?
yes (Arpan really wrote the plugin, just for credit's sake)
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
then the command you have registered will allow you to access the file name
ooooh how?
by means of loc
in the mlg file
omg
haha i always wondered what that field was
amazing, thanks
Imagine you do this
VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> { loc }
:eyes:
then loc is bound to the location of the command in the file
HOWEVER
here are the bad news
IDEs may not set the filename
does CoqIDE?
because the XML protocol doesn't include any notion of create document, so this is what CoqIDE does:
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
let loc = { (initial ToplevelInput) with bp=off; line_nb; bol_pos } in
So you are out of luck I'm afraid :(
haha ouchhh
Yeah so you will have to keep your hack
Sorry about that
OK, thanks for at least confirming that
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
In fact they are ready to use, but only became so very recently
They even abstract the notion of build etc for you
what's the hack btw?
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
And we're using Coq 8.16, in case that helps
Last updated: May 28 2023 at 16:30 UTC