Stream: Coq devs & plugin devs

Topic: CoqIDE in 8.17 / master


view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2023 at 16:17):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2023 at 16:17):

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

view this post on Zulip Michael Soegtrop (Mar 09 2023 at 16:46):

Were this the changes done to bring speed of CoqIDE back to normal? If so, I can check if speed is still OK.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 09 2023 at 16:56):

Thanks @Michael Soegtrop , it'd be appreciated

view this post on Zulip Théo Zimmermann (Mar 09 2023 at 20:36):

I don't think this was related to performance, but it never hurts to check.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 10 2023 at 13:42):

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 master ?

view this post on Zulip Théo Zimmermann (Mar 10 2023 at 17:21):

I think the performance issue was already fixed before.

view this post on Zulip Michael Soegtrop (Mar 10 2023 at 18:32):

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.

view this post on Zulip Michael Soegtrop (Mar 10 2023 at 18:34):

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: Oct 13 2024 at 01:02 UTC