Darij Grinberg (Jul 07 2021 at 22:59): Darij Grinberg (Jul 07 2021 at 22:59):Hi! Can anyone help me with this? bug1.png
Darij Grinberg (Jul 07 2021 at 23:00):Remote - WSL is installed
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
Darij Grinberg (Jul 07 2021 at 23:04):vscode is 1.57.1; vscoq is 1.3.5; WSL is Debian
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?
Darij Grinberg (Jul 07 2021 at 23:06):correct
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)
Paolo Giarrusso (Jul 07 2021 at 23:11):Google leads to https://github.com/leongrdic/wsl-alias
Paolo Giarrusso (Jul 07 2021 at 23:11):https://github.com/coq/coq/pull/8729#issuecomment-486382167
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.
Darij Grinberg (Jul 07 2021 at 23:14):!!
Darij Grinberg (Jul 07 2021 at 23:14):i wasn't aware of that readme
Darij Grinberg (Jul 07 2021 at 23:14):thank you!
Darij Grinberg (Jul 07 2021 at 23:14):i was missing the code . step
Darij Grinberg (Jul 07 2021 at 23:15):hmm ok
Darij Grinberg (Jul 07 2021 at 23:16):so now vscode has been started from WSL, but it still fails to find coqtop
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
Darij Grinberg (Jul 08 2021 at 09:40):I thought that'd be even harder to integrate with VSCode
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...)
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).
Darij Grinberg (Jul 08 2021 at 10:03):problem is, it doesn't recognize it
Darij Grinberg (Jul 08 2021 at 10:04):i gave it the path
Darij Grinberg (Jul 08 2021 at 10:05):bug1b.png that's the folder I've entered as the path
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
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)
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.
Enrico Tassi (Jul 08 2021 at 10:33):In that case coq is a native windows application, not an elf binary
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
Darij Grinberg (Jul 08 2021 at 10:54):so that'd be a probable dead end
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
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
Enrico Tassi (Jul 08 2021 at 11:53):if you use the platform scripts, you can also install additional software
Enrico Tassi (Jul 08 2021 at 11:53):coq packages I mean
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: Jun 04 2023 at 23:30 UTC