Théo Zimmermann (Feb 03 2023 at 11:03): Théo Zimmermann (Feb 03 2023 at 11:03):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?
Théo Zimmermann (Feb 03 2023 at 11:04):(And actually, maybe both suggestions could be implemented as they are kind of orthogonal.)
Maxime Dénès (Feb 03 2023 at 12:26):Sounds very reasonable to me! Any PR in that direction would be very welcome :)
Théo Zimmermann (Feb 03 2023 at 13:41):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.
Michael Soegtrop (Feb 03 2023 at 15:59):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).
Théo Zimmermann (Feb 03 2023 at 16:19):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).
Michael Soegtrop (Feb 03 2023 at 18:29):One could align with what the smoke test does. See the code here:
https://github.com/coq/platform/blob/56a960c7e5c522cf25711fb056a740322ff01deb/shell_scripts/create_smoke_test_kit.sh#L248
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.
Paolo Giarrusso (Feb 03 2023 at 18:32):Just filed https://github.com/coq-community/vscoq/issues/337, and I now see you have slightly different ideas.
Paolo Giarrusso (Feb 03 2023 at 18:33):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