Support -rifrom in coq-lsp arguments

[LasseBlaauwbroek]

I'm looking at adding support for coq-lsp in Tactician. For that, the binary needs to support a flag like -rifrom so that I can implicitly require a library. It would be great if that could be added.

[ejgallego]

@LasseBlaauwbroek would this solution to work for you:

• support the -rifrom in _CoqProject
• support that option with --rifrom=mod in the command line

?

[our cmdline parsing lib doesn't like options like -rifrom, an unexpected PITA]

[Alizter]

It is possible to do a first pass on -rifrom options in the args before passing it to cmdliner. I had a patch porting Coq to cmdliner that did this a while back. Since you match explicitly on short -rifrom you want to turn into long --rifrom you can do this wihtout messing up the posix/gnu short form convention.

[LasseBlaauwbroek]

I'd be happy for any kind variant for -rifrom on the command line. It can be --rifrom. I have to put a special case in for coq-lsp anyway. The precise command line invocation does not matter to me.

[LasseBlaauwbroek]

(But if I can have -rifrom and generally if coq-lsp can mirror the command line interface of coqc, that certainly makes my life easier.)

[LasseBlaauwbroek]

I also use cmdliner in Tactician by the way. This is such a good library that I'm still of the opinion that Coq should transition to it.

[ejgallego]

Thanks for the comments guys; for now I'll do the easy fix, but indeed it'd be nice if we could somehow solve this difference.

Something I didn't realize at first is that coq-lsp has to parse Coq arguments anyways in order to process correctly _CoqProject and dune files.

The general idea we've been promoting with coq-lsp is to actually not have command line args at all, but promote users adding their dune-project or _CoqProject files to projects, which coq-lsp then reads and applies to the project settings.

IMHO this is what every other major system is doing these days.

[LasseBlaauwbroek]

Yeah, Tactician is somewhat of a special case, in that it tries to hijack Coq a little bit by forcibly injecting extra command line arguments into coqc, coqide, coqtop and other binaries. Doing that through _CoqProject would be inconvenient and almost impossible.

A couple of years ago, this was a very convenient solution, because there were a small fixed set of binaries around Coq. Now, with language servers, this set is now a moving target, which is inconvenient. (That being said, all these language servers are pretty cool.)

[ejgallego]

Doing that through _CoqProject would be inconvenient and almost impossible.

Interesting, I was not aware of this, what is the problem in your case?

Note that coq-lsp took into account all your feedback some time ago, so indeed I hope it will provide a clearer model for your tool to hook in, I'd be very happy to chat about a deeper integration if you think that's interesting.

[LasseBlaauwbroek]

Interesting, I was not aware of this, what is the problem in your case?

Well, the point of Tactician is that you should be able to have a Coq project that does not depend on Tactician at all. Manually adding things to _CoqProject goes against that. Instead, you can do things like tactician exec coqide or tactician exec make or tactician exec dune build or tactician exec emacs to patch in Tactician when you need it. This command dynamically and temporarily injects Tactician into the Coq binaries through -rifrom commands.

See also this discussion a year ago we had: ocaml/dune#6163 (comment)

[LasseBlaauwbroek]

Note that coq-lsp took into account all your feedback some time ago, so indeed I hope it will provide a clearer model for your tool to hook in, I'd be very happy to chat about a deeper integration if you think that's interesting.

I'm not exactly sure what you are talking about here? I also saw you mention this in Zulip. Currently Tactician doesn't use SerAPI or coq-lsp at all. (Although I did use some of SerAPI a long time ago in Tactician.)

I do remember having a discussion with you about how to best access, and map/fold over Coq's internal datastructures. Especially in the presence of plugins. Are you talking about that? If so, in what way have you addressed this issue?

[ejgallego]

Well, the point of Tactician is that you should be able to have a Coq project that does not depend on Tactician at all. Manually adding things to _CoqProject goes against that. Instead, you can do things like tactician exec coqide or tactician exec make or tactician exec dune build or tactician exec emacs to patch in Tactician when you need it. This command dynamically and temporarily injects Tactician into the Coq binaries through -rifrom commands.

I see, thanks! Indeed in a setup like coq-lsp, where coq-lsp owns the workspace, it could also make sense that a coq-lsp tactician plugin would instrument things like that. But indeed, that depends on have a build system plugin.

I'm not exactly sure what you are talking about here? I also saw you mention this in Zulip. Currently Tactician doesn't use SerAPI or coq-lsp at all. (Although I did use some of SerAPI a long time ago in Tactician.)

I'm talking about having a better API for a plugin to store per-sentence state, to query document state, and or course to suggest completions to users. There was a bit of summary here https://github.com/coq/coq/wiki/BreakOut-2020-11-30-Lasse

You can hook as we discussed in the tactic engine, but now you can hook on document actions here.

[LasseBlaauwbroek]

I see. But doing this would be Flèche-dependent right? Ideally, I'd like Tactician to be independent of any LSP, STM, or document manager or whatever. I'm now also having problems with VsCoq2 because it doesn't load the STM.

I expect that the number of Coq frontends will only increase over time (think of Waterproof for example), and I'd very much like Tactician to be as oblivious as possible to this.

[ejgallego]

I see. But doing this would be Flèche-dependent right? Ideally, I'd like Tactician to be independent of any LSP, STM, or document manager or whatever. I'm now also having problems with VsCoq2 because it doesn't load the STM.

Indeed, on the other hand that's a lot more work for you, as in the end you'll have to implement your own document manager for Coq I think.

Note that Coq WaterProof uses coq-lsp, so it gets most improvements for free. Also any coq-lsp plugin will work out of the box in jsCoq 2.0.

I think you can keep tactician as is, but provide a very small extra plugin for coq-lsp that would provide functionality that is now hard to do otherwise.

[ejgallego]

So AFAICT, a tactician plugin would just be a few lines telling coq-lsp:

• to inject the corresponding instrumentation at document creation time
• to listen for some events when the document change, possibly doing some actions like storing metadata in the docs
• to listen to completion requests and propose solution
• maybe to instrument the goal with specific information about tactician state

[ejgallego]

I would expect you already have code for all this.

[LasseBlaauwbroek]

as in the end you'll have to implement your own document manager for Coq I think.

I'm not sure I'd have to do that. The state I rely on is on a lower level, either in a Summary.ref, the state of the tactic monad or in a Libobject.obj. Unless there are plans for any of that to go away, I think I'll mostly be fine.
Currently, the big hack in this area is the possibility to transfer data from the tactic monad to a Summary.ref once a proof gets closed. But is seems that coq-lsp allows me to do that without the hack, and magically without having to change anything. Perhaps that is more luck than wisdom, but I'm happy.

So AFAICT, a tactician plugin would just be a few lines telling coq-lsp:
to inject the corresponding instrumentation at document creation time

I guess in the very long term that might be convenient. But in the short term, the current PR will be enough for that.

to listen for some events when the document change, possibly doing some actions like storing metadata in the docs

I don't think I'll need that, as long as I can keep my Summary.ref data.

to listen to completion requests and propose solution

Having more rich interaction with the user than through my simple Suggest command would certainly be nice. But I'd imagine that this could indeed be achieved through a pretty thin plugin on top of Tactician.

maybe to instrument the goal with specific information about tactician state

Not sure what this is about.

[ejgallego]

I see, thanks for the info.

I don't think I'll need that, as long as I can keep my Summary.ref data.

That will actually go away at some point, but likely not soon.

Not sure what this is about.

The idea is that you can add your own data to the goals display.

[LasseBlaauwbroek]

The idea is that you can add your own data to the goals display.

That could indeed be cool. Although I have no immediate use for it. (I guess that anything printed through Feedback is already printed pretty close to the goal display. Do you have something extra-special in mind that cannot be done through Feedback?)

[ejgallego]

I think the main advantage is that you get to send indeed Feedback or custom data when the user requests a goal, so this is a hook that you don't have easily now in Coq.

Having custom data can be very useful in some contexts.