Emilio Jesús Gallego Arias

> Which one is wrong is hard to tell, but I guess CoqIDE patches are missing. Indeed, it seems like CoqIDE patches not being applied, however the local repos seems...

> This issue is that you have "coqide.8.19.0" but an opam package with the patch exists only for coqide.8.19.2. Thanks @MSoegtropIMC , where do you see "coqide.8.19.0", I see instead:...

Great, thanks!

Indeed Nix provides very good build times for Coq, it is used heavily in some Coq projects.

Thanks for the CEP @herbelin , I didn't check it deeply but it seems to me that things are going on the right direction. From my own use cases, the...

I can take care of the coq-lsp overlay folks, once you ping me this is stable.

Here it is: https://github.com/ejgallego/coq-lsp/pull/865 It was actually trivial, but I was wary about potential issues.

> @ejgallego Technically if you're willing to explicitly suppress a deprecation warning you can even make this overlay backward compatible. (That's the reason I wanted to have a deprecated alias.)...

@kayceesrk , interesting, I am having trouble reproducing the results on my intel laptop too. The way we worked was: - we started from the numbers from the Coq bench...

Thanks for the detailed analysis folks; indeed @gasche patch helped quite a bit in the Coq bench; I am still stuck as I cannot observe any slowdown on my i7-10875H...