Arpan Agrawal (Feb 13 2023 at 19:13): 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!
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?
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:18):@Talia Ringer what Coq version are you?
Talia Ringer (Feb 20 2023 at 22:18):I think 8.15, is that right @Arpan Agrawal ?
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.
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.
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
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]
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:20):given an Ast, location is in the loc field
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:21):@Talia Ringer is your plugin registering a command?
Talia Ringer (Feb 20 2023 at 22:22):yes (Arpan really wrote the plugin, just for credit's sake)
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
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
Talia Ringer (Feb 20 2023 at 22:22):ooooh how?
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:22):by means of loc in the mlg file
Talia Ringer (Feb 20 2023 at 22:22):omg
Talia Ringer (Feb 20 2023 at 22:22):haha i always wondered what that field was
Talia Ringer (Feb 20 2023 at 22:23):amazing, thanks
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:23):Imagine you do this
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:23):VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> { loc }
:eyes:
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):then loc is bound to the location of the command in the file
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):HOWEVER
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):here are the bad news
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:24):IDEs may not set the filename
Talia Ringer (Feb 20 2023 at 22:24):does CoqIDE?
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:
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:26): let loc = { (initial ToplevelInput) with bp=off; line_nb; bol_pos } in
So you are out of luck I'm afraid :(
Talia Ringer (Feb 20 2023 at 22:26):haha ouchhh
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:26):Yeah so you will have to keep your hack
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:27):Sorry about that
Talia Ringer (Feb 20 2023 at 22:27):OK, thanks for at least confirming that
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
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:28):In fact they are ready to use, but only became so very recently
Emilio Jesús Gallego Arias (Feb 20 2023 at 22:29):They even abstract the notion of build etc for you
Gaëtan Gilbert (Feb 20 2023 at 22:32):what's the hack btw?
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
Arpan Agrawal (Feb 20 2023 at 22:56):And we're using Coq 8.16, in case that helps
Last updated: Dec 06 2023 at 14:01 UTC