Would it be reasonable for VsCoq to automatically detect the path to a standard installation of Coq with the Coq Platform Windows installer? I have a student using VsCoq on Windows and everything worked perfectly as soon as we provided the path in the extension settings. If not possible, VsCoq could maybe suggest in its error message that what is needed is to provide the path and even link directly to the appropriate extension setting?
(And actually, maybe both suggestions could be implemented as they are kind of orthogonal.)
Sounds very reasonable to me! Any PR in that direction would be very welcome :)
I won't have time to do this in the short-term but I would appreciate if someone would make an issue for this suggestion so that it is tracked.
It would be a hack, but the safest way to detect the installation directory of the most recently installed Coq would be to look into the uninstall information written here (https://github.com/coq/platform/blob/56a960c7e5c522cf25711fb056a740322ff01deb/windows/Coq.nsi#L91).
I was not suggesting using a hack, but rather using only standard locations (and the most recent version if several versions are detected in standard places).
One could align with what the smoke test does. See the code here:
The issue is that it might be hard to foresee what the "PRODUCTNAME" is. The smoke test kit just knows this, because it has been created for the same "PRODUCTNAME". For an outside software, this is in general not that trivial.
Using the uninstall registry key should be fairly bullet proof and this did not change since Coq 8.7 or so. But I think one only gets the most recent install this way.
We probably should define well defined registry keys for detecting installed Coq Platform versions.
Just filed https://github.com/coq-community/vscoq/issues/337, and I now see you have slightly different ideas.
but at least https://www.npmjs.com/package/vscode-windows-registry exists so looking at the Windows registry is possible.
Last updated: Jun 04 2023 at 23:30 UTC