Stream: VsCoq devs & users

Topic: can't find coqtop


view this post on Zulip Darij Grinberg (Jul 07 2021 at 22:59):

Hi! Can anyone help me with this? bug1.png

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:00):

Remote - WSL is installed

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:00):

the path does exist and has a coqtop, a coqtop.byte and a coqtop.opt in it

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:04):

vscode is 1.57.1; vscoq is 1.3.5; WSL is Debian

view this post on Zulip Paolo Giarrusso (Jul 07 2021 at 23:06):

Just to be sure, that's a Vscode in windows trying to start Coq from inside WSL?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:06):

correct

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:09):

(i'd ditch the WSL hack if i knew i could get the packages to install natively on windows... doesn't look like that though)

view this post on Zulip Paolo Giarrusso (Jul 07 2021 at 23:11):

Google leads to https://github.com/leongrdic/wsl-alias

view this post on Zulip Paolo Giarrusso (Jul 07 2021 at 23:11):

https://github.com/coq/coq/pull/8729#issuecomment-486382167

view this post on Zulip Paolo Giarrusso (Jul 07 2021 at 23:13):

Hmmm nevermind you're following another route https://github.com/coq/coq/wiki/Installation-of-Coq-on-Windows#front-end-setup-in-wsl, hopefully some Windows user has better answers.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:14):

!!

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:14):

i wasn't aware of that readme

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:14):

thank you!

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:14):

i was missing the code . step

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:15):

hmm ok

view this post on Zulip Darij Grinberg (Jul 07 2021 at 23:16):

so now vscode has been started from WSL, but it still fails to find coqtop

view this post on Zulip Enrico Tassi (Jul 08 2021 at 07:17):

Why wsl? I know it is cool, but we have well tested scripts for cygwin in the coq platform https://github.com/coq/platform

view this post on Zulip Darij Grinberg (Jul 08 2021 at 09:40):

I thought that'd be even harder to integrate with VSCode

view this post on Zulip Darij Grinberg (Jul 08 2021 at 09:40):

anyway: I finally got coqide running, so I don't need vscode that much any more (though I'd still prefer it to work...)

view this post on Zulip Enrico Tassi (Jul 08 2021 at 09:59):

You can tell vscoq the path of coqidetop in the config window, that is all you need. Note that even if we use cygwin to build coq and all its packages, you don't really need cygwin to run coq (you need to open a cygwin shell if you want to opam install more stuff, but that is it).

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:03):

problem is, it doesn't recognize it

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:04):

i gave it the path

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:05):

bug1b.png that's the folder I've entered as the path

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:06):

I suspect it either cannot access the folder because of Windows folder black magic, or it cannot run the compiler because it's a linux elf

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:07):

it'd be great to know which of the two it is, but vscode doesn't give informative error messages (it took me two days to figure out an extension wouldn't install because vscode was out of date)

view this post on Zulip Enrico Tassi (Jul 08 2021 at 10:33):

I was suggesting to do so if you use the platform (scripts or prebuilt installer). With wsl I've no idea, I never tried.

view this post on Zulip Enrico Tassi (Jul 08 2021 at 10:33):

In that case coq is a native windows application, not an elf binary

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:54):

the native Windows coq will surely work, but I don't know how to install packages onto it

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:54):

so that'd be a probable dead end

view this post on Zulip Darij Grinberg (Jul 08 2021 at 10:55):

unless the packages are completely independent of coq and i can use WSL to install them while still using the native coq compiler

view this post on Zulip Enrico Tassi (Jul 08 2021 at 11:52):

please have a look at https://github.com/coq/platform/blob/2021.02/README_Windows.md#compiling-from-sources-with-cygwin-as-build-host

view this post on Zulip Enrico Tassi (Jul 08 2021 at 11:53):

if you use the platform scripts, you can also install additional software

view this post on Zulip Enrico Tassi (Jul 08 2021 at 11:53):

coq packages I mean

view this post on Zulip Paolo Giarrusso (Jul 10 2021 at 17:15):

aah, the key point is > The resulting Coq installation is opam based and best used from the Cygwin prompt (started via C:\<your_coq_platform_Cygwin_path>\Cygwin.bat)


Last updated: Jan 30 2023 at 17:03 UTC