Coq bin detection #439
Coq bin detection #439
Conversation
|
@maximedenes @gares is this working as intended, as I recall we were waiting for maxime to rebase the submodule but it should be all right now ? if so let's merge ! |
client/src/utilities/toolchain.ts
Outdated
| exec(cmd, {cwd: vscoqtopPath}, (error, stdout, stderr) => { | ||
| if(error) { | ||
| VsCoqToolchainManager._channel.appendLine(error); | ||
| window.showErrorMessage(stderr); |
There was a problem hiding this comment.
I think you should wrap the error saying something like:
$PATH_TO_VSCOQTOP cannot run properly since the installation of the standard library seems broken: $ERR. If this is not the Coq installation you want to use, set the right path in the settings panel.
There was a problem hiding this comment.
Done. I was wondering, if for whatever reason the user passes -coqlib and the dir does not work, the server will crash without real warning (-where does not detect that, it ignores the -coqlib arg). Is there a way to check that and notify the user that the path he gave is incorrect ?
There was a problem hiding this comment.
Starting from 8.18 coq* -where will honor -coqlib
| return ""; | ||
| } | ||
|
|
||
| private checkIfCoqFound(vscoqtopPath: string) { |
There was a problem hiding this comment.
About the comment request by @maximedenes:
Check if vscoqtop can load the prelude at its expected installation site, or wherever the user specified by passing -coqlib. (since 8.18 -where does not only print where the prelude is expected to be, but also checks it exists).
rtetley
force-pushed
the
coq-bin-detection
branch
from
b60fa34
to
0c95cdc
Compare
No description provided.