Brandon Sisler (Dec 09 2022 at 21:30): Brandon Sisler (Dec 09 2022 at 21:30):Hey all, A while back I was having trouble getting VSCode to find coqtop, which was resolved when I found out that you needed to give the path to the file which contains coqtop, rather than to coqtop itself.
Unfortunately, after having updated Coq, I have reencountered the error and can not remedy it the same way that I did before.
For context I know that coqtop in located in the path
C:\Users\brand\OneDrive\Desktop\my_coq_projects\Coq-Platform~8.16~2022.09~beta1\bin
but VSCoq is really not happy with this, what am I missing?
Paolo Giarrusso (Dec 09 2022 at 22:15):(1) Does that contain coqidetop.opt.exe ? (2) what was the old PATH? (3) what does "not happy" mean?
Brandon Sisler (Dec 09 2022 at 22:22):(1) Yes
(2) To my memory it was in an identical place.
(3) I receive the error coqtop not found here
Paolo Giarrusso (Dec 10 2022 at 03:22):VsCoq lets one also customize the name of the binaries it calls. I wonder if you modified those settings... I should check the setting names on my laptop...
Michael Soegtrop (Dec 10 2022 at 13:46):I don't think it is a terribly good idea to install Coq Platform on a OneDrive drive - you should rather install it under C:\bin (but not under C:\Program Files - the path must not conatain spaces).
Brandon Sisler (Dec 12 2022 at 02:42):You are absolutely right, I installed it to there, and voila, it works. Thanks again!
Notification Bot (Dec 12 2022 at 02:42):Brandon Sisler has marked this topic as resolved.
Last updated: Jun 04 2023 at 23:30 UTC