Hi! Can anyone help me with this? bug1.png
Remote - WSL is installed
the path does exist and has a coqtop, a coqtop.byte and a coqtop.opt in it
vscode is 1.57.1; vscoq is 1.3.5; WSL is Debian
Just to be sure, that's a Vscode in windows trying to start Coq from inside WSL?
(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)
Google leads to https://github.com/leongrdic/wsl-alias
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.
i wasn't aware of that readme
i was missing the
code . step
so now vscode has been started from WSL, but it still fails to find coqtop
Why wsl? I know it is cool, but we have well tested scripts for cygwin in the coq platform https://github.com/coq/platform
I thought that'd be even harder to integrate with VSCode
anyway: I finally got coqide running, so I don't need vscode that much any more (though I'd still prefer it to work...)
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).
problem is, it doesn't recognize it
i gave it the path
bug1b.png that's the folder I've entered as the path
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
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)
I was suggesting to do so if you use the platform (scripts or prebuilt installer). With wsl I've no idea, I never tried.
In that case coq is a native windows application, not an elf binary
the native Windows coq will surely work, but I don't know how to install packages onto it
so that'd be a probable dead end
unless the packages are completely independent of coq and i can use WSL to install them while still using the native coq compiler
please have a look at https://github.com/coq/platform/blob/2021.02/README_Windows.md#compiling-from-sources-with-cygwin-as-build-host
if you use the platform scripts, you can also install additional software
coq packages I mean
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