search

cpehle / lean4-plugin-example

1 stars 0 forks source link

VS Code executable setting does not work on Windows #1

Open tydeu opened 3 years ago

tydeu commented 3 years ago

Setting the Lean executable to leanWithPlugin.sh does not work on Windows due to path conversion problems between VS Code, the Lean server, MSYS2, and leanmake. Opening test\run\ex\ex0.lean in VS Code results in the following error:

`leanpkg print-paths` failed:

stderr:
make: *** No rule to make target 'buildExample.olean'.  Stop.
configuring example 0.1
> sh -c "<home>\.elan\toolchains\leanprover--lean4---nightly-2021-09-05\bin/leanmake" PKG=Example LEAN_OPTS="" LEAN_PATH=".\.\build" build\Example.olean MORE_DEPS+="leanpkg.toml" >&2    # in directory .
external command exited with status 2

I am fairly confident that we will have to wait for the next release of vscode-lean4 to land (which includes a setting for providing additional options to the Lean 4 server) before it is possible to make server plugins cross platform.

cpehle commented 3 years ago

Thanks for bringing this to my attention. It might be still possible to address this by using a script adapted to Windows.