coq-serapi icon indicating copy to clipboard operation
coq-serapi copied to clipboard

Published 20 hours ago • verified publisher icon ejgallego

Minor request: use -Q DIR LP instead of -Q DIR,LP?

Open cpitclaudel opened this issue 5 years ago • 1 comments
trafficstars

I'm not sure what the proper way is to do this without breaking existing code. It's just a bit unfortunate that SerAPIs options are not spelled the same as Coq's

cpitclaudel avatar Jun 28 '20 05:06 cpitclaudel

It is indeed a big pain, I tried to have cmdliner to parse that, but I didn't manage to hack a solution where cmdliner would take the arguments in this way, I'll try to re-hack to see what can be done [patches welcome of course]

A likely easier solution would be to have Coq itself take -R log=dir

ejgallego avatar Jun 28 '20 13:06 ejgallego

coq-lsp auto-configures itself if passed the correct root, so this is less of an issue.

ejgallego avatar Feb 15 '23 00:02 ejgallego