Stream: Coq devs & plugin devs

Topic: arrays vs lists


view this post on Zulip Ali Caglayan (Apr 12 2022 at 19:29):

@Pierre-Marie Pédrot I see that mkApp uses an array meaning you have to convert your new lists back to arrays. What is the reason for the use of arrays in the first place?

view this post on Zulip Ali Caglayan (Apr 12 2022 at 19:30):

I would assume they are quite optimized for copying etc.

view this post on Zulip Ali Caglayan (Apr 12 2022 at 19:32):

for context I am talking about https://github.com/coq/coq/pull/15923 btw

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:37):

"historical reasons"

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:38):

even Xavier Leroy asked about that once

view this post on Zulip Ali Caglayan (Apr 12 2022 at 19:40):

Have there been attempts to move things in the kernel to using lists?

view this post on Zulip Ali Caglayan (Apr 12 2022 at 19:40):

Not that I think it is a good idea, but I am wondering why "historical reasons" have lasted so long.

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:43):

the one (1) advantage I know of arrays in applications is that it's more compact in vo files

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:44):

per n elements, lists are 3n words when arrays are n + 1

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:44):

Exactly, space consumption is surely relevant.

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:45):

we lose a lot of space in other areas so I'm not sure that this criterion is really relevant

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:45):

In an abandoned branch of mine, I did use the mutability of arrays is the lazy reduction machine, rather than an explicit mutable node, and there was a good speedup.

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:46):

did you remove the mutable node altogether?

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:47):

IIRC yes,the branch is this one: https://github.com/gares/coq/tree/speedup/tcomp

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:47):

but it does many more things, not sure it is usable

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:48):

then you might also have changed the lazy heuristics, which might be much more observable than just this

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:48):

(I have no shame saying that I don't understand what kind of sharing the kernel reduction is attempting)

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:50):

Hum, now that I look at the code, I think the speedup was also from other stuff:
https://github.com/gares/coq/blob/2b0c3d679d18e40b513c813e567249db605a52d1/kernel/closure.ml#L404-L405

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:50):

(and also, the kernel reduction seems to have been historically tailored for computation not conversion)

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:50):

IIRC I did rewrite the whole thing and avoid many unnecessary allocations, and that was still by-name, then when i added by-need, I did change nothing, since arrays were already mutable

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:51):

but there is no single "by-need" so you might be wildly different from master in that respect

view this post on Zulip Pierre-Marie Pédrot (Apr 12 2022 at 19:51):

more sharing can be contraproductive in conversion, for instance

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:53):

sure, my point was: arrays do give us space, but they could also be used to implement Zupdate (but they are not, IIRC).

view this post on Zulip Enrico Tassi (Apr 12 2022 at 19:58):

Anyway, if the bench is OK, I'm all for dropping arrays. But I would be surprised there is no memory penalty

view this post on Zulip Enrico Tassi (Apr 12 2022 at 20:00):

The more I look at my old code, and the more I doubt about my recollections

view this post on Zulip Enrico Tassi (Apr 12 2022 at 20:00):

maybe it's time to go to bed ;-)

view this post on Zulip Hugo Herbelin (Apr 27 2022 at 14:35):

"historical reasons"

App to array was introduced around Coq 5.10 (presumably by Chet Murthy). Chet had the habit to benchmark various implementation choices but I can't tell for sure the motivation here. Beforehand (at least up to version 5.6), this was a binary app node.

view this post on Zulip Enrico Tassi (Apr 27 2022 at 14:44):

Well, anything is better than binary applications ;-)


Last updated: Feb 06 2023 at 18:03 UTC