Stream: VsCoq devs & users

Topic: Autocompletion


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Hjalte Sorgenfrei Mac Dalland (Feb 17 2023 at 10:24):

I have made a draft PR now

view this post on Zulip 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: Mar 29 2024 at 10:01 UTC