Emilio Jesús Gallego Arias (Feb 06 2023 at 16:37): Emilio Jesús Gallego Arias (Feb 06 2023 at 16:37):@Matthieu Sozeau I am looking into this, but I'm unsure there is a way to put this in _CoqProject right?
If not, where should this info be stored?
How do you set OCAMLPATH for the other IDEs?
Matthieu Sozeau (Feb 06 2023 at 16:38):I don't want to put it in the _CoqProject, I think it should just be for the lsp process
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:38):If you do a make launch-code which does export OCAMLPATH= ... code . do things work?
Matthieu Sozeau (Feb 06 2023 at 16:38):I guess, I didn't try
Matthieu Sozeau (Feb 06 2023 at 16:39):It might be coq-lsp's -I not working the same as vscoq's/coqtop. I think -I are added to the OCAMLPATH so findlib can find my plugins even if they're not installed yet
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:39):Actually if you are still in 0.1.2 that could be a bug we had
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:41):Actually it should work the same, let me try (actually you can see what settings are detected from the Output > Coq LSP Server Events buffer, but we need to replace that one because it is very verbose, there is a workspace panel coming up soon with that information
Emilio Jesús Gallego Arias (Feb 06 2023 at 16:43):Tho if you check that buffer it should say something such as "Configuration loaded from ..."
Emilio Jesús Gallego Arias (Feb 16 2023 at 21:12):@Matthieu Sozeau , I have finally got some testing and found the bug, indeed you were correct, I'm unsure why I was under the impression that I had fixed -I properly. With the fix applied coq-lsp 0.1.5 seems to works well with MetaCoq (what I could try)
I will release 0.1.5.1
Emilio Jesús Gallego Arias (Feb 16 2023 at 22:12):Ok, release pushed, I was able to work with all of metacoq now :)
Emilio Jesús Gallego Arias (Feb 16 2023 at 22:12):I found some other wishes, like ignoring .vo files, and caching document creating, but these will go on 0.1.6 (beyond a quickfix)
Emilio Jesús Gallego Arias (Feb 16 2023 at 22:13):Also the new obligation display could be useful for you folks, but that's master-only, for 8.16/8.17 would require we use Coq variants in opam
Emilio Jesús Gallego Arias (Feb 17 2023 at 13:08):I've also added for next release support for workspaces with multiple folders, so now you can indeed add all of metacoq folders and it works.
Emilio Jesús Gallego Arias (Feb 17 2023 at 13:09):I did some testing and indeed most files work fine, but in 8.16 there is some problem due to the way coq-lsp handles program and universes in some cases I think, this seems the same bug we detected in the simple compiler, and has to do with strange stuff, Stm workarounds that using a large hack.
I'll retest with Coq master as that is likely solved.
Last updated: Apr 19 2024 at 04:02 UTC