Hi folks, in particular CoqIDE users (cc @Pierre-Marie Pédrot , @Hugo Herbelin )
We did prepare a revert to the CoqIDE changes in https://github.com/coq/coq/pull/17348 , that should put master / 8.17 in the same state than 8.16, but we'd like to get a confirmation that the PR gets CoqIDE to some kind of working state
If the state of that PR is "good", then we will backport and @Théo Zimmermann can proceed to release 8.17
I am having trouble determining the status myself as there were some broken things in 8.16, for example tooltips didn't already work, etc...
Were this the changes done to bring speed of CoqIDE back to normal? If so, I can check if speed is still OK.
Thanks @Michael Soegtrop , it'd be appreciated
I don't think this was related to performance, but it never hurts to check.
There was a performance problem but that was solved, I'm unsure what the problems were, do we have bugs openened against the version in
I think the performance issue was already fixed before.
Yes, but afair the performance issue had something to do with handling some sort of code location references (I don't understand the details), and the PR @Emilio Jesús Gallego Arias mentioned above vaguely seems to have something to do with it.
There is an easy test. Load this file: https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/Pff/Pff.v in CoqIDE (afair it only depends on standard library stuff). The file has 30k lines. It should go through in a minute or so. In the broken versions of CoqIDE it took much longer.
If you have the respective build ready, it might be easiest if you just check it. But I will also do a test build over the weekend and see.
Last updated: Dec 07 2023 at 09:01 UTC