Maxime Dénès (Feb 17 2023 at 08:48): Maxime Dénès (Feb 17 2023 at 08:48):@Hjalte Sorgenfrei Mac Dalland I'll do a quick pass now on your autocompletion PR, should be good to merge after that. It would be nice to then open another one with your declaration provider (maybe as a draft). A few things will need to be tweaked as to how we load .vo files, but it is still nice to have.
Hjalte Sorgenfrei Mac Dalland (Feb 17 2023 at 09:30):Alright thanks.
I will open a new PR with declaration provider.
Regarding the .vofiles, are they not just compiled binaries and therefore not useful when navigating to source?
Where should the code search for the .vfiles when looking for non-stdlib theories, where we don't really know the path?
Maxime Dénès (Feb 17 2023 at 09:31):Ideally Coq should emit some information about that, but it is not the case today.
Maxime Dénès (Feb 17 2023 at 09:32):So in fact your heuristic was not so bad. We discussed with @Enrico Tassi and tought we only need to tweak it for the sources of the current project. If it is built with Dune, with your heuristic it will jump to a copied read-only version of the sources, which is confusing. But for external dependencies it should work fine.
Hjalte Sorgenfrei Mac Dalland (Feb 17 2023 at 10:24):I have made a draft PR now
Enrico Tassi (Feb 17 2023 at 10:30):Maxime Dénès said:
Ideally Coq should emit some information about that, but it is not the case today.
Since I'm working on location in Coq for another PR, I might give it a try
Last updated: Jun 04 2023 at 22:30 UTC