Stream: VsCoq devs & users

Topic: ✔ Return of CoqTop Problem


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

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

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

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

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

view this post on Zulip Brandon Sisler (Dec 12 2022 at 02:42):

You are absolutely right, I installed it to there, and voila, it works. Thanks again!

view this post on Zulip Notification Bot (Dec 12 2022 at 02:42):

Brandon Sisler has marked this topic as resolved.


Last updated: May 18 2024 at 08:40 UTC