Stream: Coq devs & plugin devs

Topic: Spring cleanup of the evar_map


view this post on Zulip Enrico Tassi (Dec 31 2021 at 09:48):

I was wondering if we could have 2 evar_info, one returned by find_undefined and another one by find_defined. In some sense move the evar_body option type outside and have the general api find return one or the other info.

We already have in the evar map distinct defined/undefined maps, I was thinking of making them carry different info. For example I expect we don't need to have the entire context/type once the evar is assigned.

Can anyone see a problem in doing that?

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 09:58):

I've been looking at that recently, actually

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 09:59):

I am 100% in favour of this change but there are parts of the code that are not ready yet IIRC

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 10:00):

(I mean, if you just go for an isomorphism it's fine, but if you want to remove data it's going to be hard)

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 10:02):

A good first step is to double check calls to Evd.find, most of those are actually statically known to be calls to Evd.find_undefined

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:06):

About dreams, I'd like, on the coq-elpi side, to build a weak map on the evar_info_unassigned. For this to work I need two things: one is to add a field which is the evar number (easy, to get a fast "hash") and another one would be to make it "immutable" (if the uvar body is hoisted, it is kind of like that). One thing that worries me is there are a few metadata which Coq may update (TC status for example). I don't know how far this can go..., if they can be hoisted as well...

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:10):

I can't build a weak map on Evar.t because it is not boxed, but boxing it just for coq-elpi would be too much...

Of course we could decide we box them and make the evar map a weak map!
I have no idea if this would scale, but if it does it would solve a major problem of the current evar map, which implements a heap without a garbage collector.
It would also simplify many things, eg no need to roll back the evar map. But one would need to bench it...

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:11):

I think it's very dangerous to implement the evarmap as a weak map. Clearly it's a heap and it's lacking a GC, but the lifetimes are not bound to the actual reachability of OCaml values. Rather, I'd prefer that we clearly expose a set of roots in the map and implement our own GC atop of that.

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:12):

Not even mentioning the fact we have to marshal that stuff.

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:14):

There is one moral root, the proof root. All other roots are the terms one builds before calling refine. I fail to see the danger.

Yes, marshaling sigma "as is" won't work.

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:14):

it's an interesting experiment though, if ever you try this out I would be very eager to see the results

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:15):

no, the one root theory is an illusion. We can (and we do) store data that can refer to evars outside of the proof term

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:15):

That would be a potential leak, but won't be worse than today.

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:16):

I prefer a leak to a Not_found

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:16):

fair enough

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:17):

but you'd still have to make imperative copies from time to time, so it's not clear to me that it's going to be efficient when compared to a high-level GC

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:18):

copies of what? I thought so, but actually no (as long as the evar counter is always increasing)

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:19):

since it is weak, you can pull out of backtracking completely

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:20):

how do you backtrack on assignment?

view this post on Zulip Pierre-Marie Pédrot (Dec 31 2021 at 11:20):

the whole API is designed around the immutability of the evarmap, you can't change that like that...

view this post on Zulip Enrico Tassi (Dec 31 2021 at 11:34):

Sure you have to undo assignments (but the weak hash table can just stay there, outside the monad). Nevermind this point.

view this post on Zulip Matthieu Sozeau (Jan 06 2022 at 13:16):

Each evar introduced by pretyping while type-checking a term is a root too, no?

view this post on Zulip Jason Gross (Jan 06 2022 at 20:14):

Derive, Program, and mutual (co)fixpoints in interactive mode all introduce multiple roots too, right?


Last updated: Feb 06 2023 at 20:02 UTC