Stream: Coq devs & plugin devs

Topic: V82 compat layer


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jun 10 2020 at 20:27):

funind is going to be a lot of efforts

view this post on Zulip Maxime Dénès (Jun 10 2020 at 20:28):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:33):

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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jun 10 2020 at 20:34):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:35):

I indeed still have some commits here and there

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:35):

but they are very routine

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:35):

I got blocked on that weird destruct stuff

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

recently I cleaned up a few

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

so indeed it would make sense to do a pass

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

but likely we want to leave funind for the last

view this post on Zulip Emilio Jesús Gallego Arias (Jun 10 2020 at 20:36):

what about ssreflect tho?

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jun 10 2020 at 20:37):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC