[2023.08] [coq-lsp 0.2.0] [v8.17] Draft Windows build

[ejgallego]

Changes:

• Simplify some paths and logic
• Don't exclude sexplib0
• Pin to latest Coq's v8.17+lsp branch
• Pin to latest coq-lsp's branch for 8.17
• Slightly reduced package set

[MSoegtropIMC]

@ejgallego : I saw that you created a different cygwin root. Is this cause of path length issues?

[ejgallego]

@ejgallego : I saw that you created a different cygwin root. Is this cause of path length issues?

Both to prevent path length issues and to be able to distribute this installer without conflicting with the official release.

Things build OK, coq-lsp runs pretty well, except for that unfortunately it seems there are some problems with plugin loading / findlib which I'm currently debugging.

coq-lsp supports several project roots in the same process, such as MetaCoq, but that requires custom init to findlib for each document process.

[ejgallego]

Update: built from source on Windows, works very smoothly, other than the missing libgmp.

coq-lsp needs its own plugin loader as it needs to instrument plugins ASTs to make it work effectively, I bet coq-lsp plugin loader is finding some error with findlib and not handling it properly so I can see the real cause.

But other than that, which I shall solve soon, the coq-lsp platform installer should be ready soon.

The missing libgmp is only a problem for builds from source, once the installer puts that lib in C:\Coq\bin things are fine.

There are some problems with URIs and Windows paths too, these should be easy to solve, tho I am a bit confused on whether /c:/foo/bar is a valid windows path (URIs that vscode send are of the form file:///c:/foo/bar which get parsed by the OCaml URI library as /c:/foo/bar

That could possibly be very wrong?

[MSoegtropIMC]

Both to prevent path length issues and to be able to distribute this installer without conflicting with the official release.

The cygwin build path has noting to do with the install path - it exists only during build time. The installer is relocatable (which is the reason I am using a patched ocamlfind).

You say you are having issues with libgmp: this is quite strange since it is used in many places and this usually works. Did you add opam packages which need libgmp but don't declare this?

/c:/foo/bar is not a valid windows path, but c:/foo/bar is. Code which makes relative paths absolute needs to handle drive letters correctly. The forward slash is no issue even at WIndows API level, but CMD doesn't accept it without quoting.

[MSoegtropIMC]

Should I dig out a description of the findlib changes I did, or are you aware how this works?

[MSoegtropIMC]

One more note: it is a recommended use case to reuse coq platform cygwin installations. If you build on the same machine a standard and modified coq platform, or say several Coq versions, you can reuse the cygwin installed once and use it as any other opam environment. You can run the coq platform script from inside the cygwin shell and it will create a new opam switch.

[ejgallego]

You say you are having issues with libgmp: this is quite strange since it is used in many places and this usually works. Did you add opam packages which need libgmp but don't declare this?

The issue only happens in a build from source: binaries generated that way cannot be called from the explorer unless libgmp is placed somewhere windows can find it. IMHO not a big deal (tho for VSCode testing it gets in the way)

/c:/foo/bar is not a valid windows path, but c:/foo/bar is. Code which makes relative paths absolute needs to handle drive letters correctly.

In this particular case the problem is that VSCode sends the file:///c:/foo/bar URI, which is parsed by URI libraries as /c:/foo/bar. I didn't find any more information on this.

Should I dig out a description of the findlib changes I did, or are you aware how this works?

I think I'm good for now @MSoegtropIMC , thanks!

I am totally lost on what the problem is, so let me try to make some more progress first. coq-lsp works very well when built from source, but once it is put in the installer, something very weird is happening with library loading, which I couldn't track down yet, even using procmon.

It seems like Coq things a plugin was loaded, but actually it was not; then Coq crashes as the Dyn entries registered by the plugin are not in scope :(

[ejgallego]

Hi @MSoegtropIMC , I finally found the problem, it was indeed tricky, but somehow using an unpatched findlib + procmon I got to understand it.

The problem is as follows, the lib/sexplib0 directory is not copied from the .opam/$switch/lib folder to the installer.

Is that due to this line?

OPAM_PACKAGE_EXCLUSION_LIST="${OPAM_PACKAGE_EXCLUSION_LIST}"$'\n'"sexplib0"$'\n'"csexp"$'\n'"ocamlbuild"$'\n'"cppo"

The missing C:\CP\lib\sexplib0 directory makes the plugin loader in a silent way, I'm reviewing that code.

[MSoegtropIMC]

@ejgallego : yes, the OPAM_PACKAGE_EXCLUSION_LIST contains packages which are deemed to be required only at build time or for ocaml (which is not included in the installer). As far as I can tell this list was accurate in the past, but apparently no longer is. I would remove the package from this list.

I hope my ocamlfind changes are not a problem.

[ejgallego]

sexplib0 has been a runtime dep of coq-serapi since quite a bit of time, so I wonder what happened, originally this exclusion was only for the OSX installer, but now the windows one does it too after the refactoring

The first commit where this appears is this one 74ffe47 , doesn't seem to explain a lot, maybe it rings a bell to you?

I hope my ocamlfind changes are not a problem.

I think the ocamlfind changes are not a problem, but given that plugin loading was failing I went to debug them.

Indeed I think we could drop the ocamlfind patch in favor of making Coq relocatable. In a sense I already do that for the JS version of Coq, all that we would need is to consolidate the code in Coq's boot component a bit more. Dune also provides support for making binaries relocatable, but not sure would work well for us.

Happy to help with that if you folks are interested.

[ejgallego]

Indeed after removing sexplib0 from the list of excluded packages everything works normally. Damn I lost 2 days on this XD

I still have no idea why findlib didn't raise an exception or the exception handling code didn't print the warning, but that's a separate issue.

I'm gonna consolidate upstream some changes needed for windows that I saw on my testing, and build a complete installer soon.