@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?
I would assume they are quite optimized for copying etc.
for context I am talking about https://github.com/coq/coq/pull/15923 btw
even Xavier Leroy asked about that once
Have there been attempts to move things in the kernel to using lists?
Not that I think it is a good idea, but I am wondering why "historical reasons" have lasted so long.
the one (1) advantage I know of arrays in applications is that it's more compact in vo files
per n elements, lists are 3n words when arrays are n + 1
Exactly, space consumption is surely relevant.
we lose a lot of space in other areas so I'm not sure that this criterion is really relevant
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.
did you remove the mutable node altogether?
IIRC yes,the branch is this one: https://github.com/gares/coq/tree/speedup/tcomp
but it does many more things, not sure it is usable
then you might also have changed the lazy heuristics, which might be much more observable than just this
(I have no shame saying that I don't understand what kind of sharing the kernel reduction is attempting)
Hum, now that I look at the code, I think the speedup was also from other stuff:
(and also, the kernel reduction seems to have been historically tailored for computation not conversion)
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
but there is no single "by-need" so you might be wildly different from master in that respect
more sharing can be contraproductive in conversion, for instance
sure, my point was: arrays do give us space, but they could also be used to implement Zupdate (but they are not, IIRC).
Anyway, if the bench is OK, I'm all for dropping arrays. But I would be surprised there is no memory penalty
The more I look at my old code, and the more I doubt about my recollections
maybe it's time to go to bed ;-)
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.
Well, anything is better than binary applications ;-)
Last updated: Dec 05 2023 at 12:01 UTC