Stream: Coq devs & plugin devs

Topic: V82 compat layer

Maxime Dénès (Jun 10 2020 at 20:24):

Just out of curiosity, is there any major blocker to removing the last uses of the V82 compat layer, or is it just a matter of spending a bit of time?

Pierre-Marie Pédrot (Jun 10 2020 at 20:27):

funind is going to be a lot of efforts

Maxime Dénès (Jun 10 2020 at 20:28):

but just because there are lots of occurrences? or some missing functionality?

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:33):

With funind I got far enough as to have only one real blocker

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:34):

some very weird manipulation that I couldn't manage, but that should be doable

Maxime Dénès (Jun 10 2020 at 20:34):

so you have a branch that removes most uses of the V82 compat layer?

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:35):

I indeed still have some commits here and there

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:35):

but they are very routine

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:35):

I got blocked on that weird destruct stuff

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

also some evar_maps are passed by ref and they are quite hard to understand

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

recently I cleaned up a few

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

so indeed it would make sense to do a pass

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

but likely we want to leave funind for the last

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

what about ssreflect tho?

Emilio Jesús Gallego Arias (Jun 10 2020 at 20:37):

with funind my understanding is that easily we will be down to 2 / 3 problematic places

Maxime Dénès (Jun 10 2020 at 20:37):

yeah ssr is also why I was asking if there were "real" blockers

Maxime Dénès (Jun 10 2020 at 20:38):

I guess we are still going to hit the lack of evar garbage collection issue

Maxime Dénès (Jun 10 2020 at 20:39):

@Pierre-Marie Pédrot I have a related question: what does the comment at https://github.com/coq/coq/blob/c077db40a204132eda8a5d5979022f4961503cab/engine/proofview.ml#L754 mean?

Maxime Dénès (Jun 10 2020 at 20:40):

i.e. why can future goals come only from the compat layer at that code point?

Last updated: Jun 05 2023 at 10:01 UTC