Emilio Jesús Gallego Arias

> @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...

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...

> 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...

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,...

`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...

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...

> @ejgallego : anything I can help with? Everything good, thanks! I started with the 8.19 pick, but indeed had to remove a few broken contribs. The installer seems to...

This particular artifact hasn't been tested yet, however the artifacts for 8.17 / 8.18 have been used by quite a few people with pretty good results I understand, including lectures.

Artifact tested, working pretty well on the cases we have. [Note that the current installer still requires to config VSCode as outline in the README on coq-lsp for Windows]

@MSoegtropIMC , actually there is something strange going on here (and in the sister PRs for 8.18 and 8.17) , for some reason, CoqIDE is not building correctly, I am...