Ali Caglayan (Apr 12 2022 at 19:29): 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?
Ali Caglayan (Apr 12 2022 at 19:30):I would assume they are quite optimized for copying etc.
Ali Caglayan (Apr 12 2022 at 19:32):for context I am talking about https://github.com/coq/coq/pull/15923 btw
Pierre-Marie Pédrot (Apr 12 2022 at 19:37):"historical reasons"
Pierre-Marie Pédrot (Apr 12 2022 at 19:38):even Xavier Leroy asked about that once
Ali Caglayan (Apr 12 2022 at 19:40):Have there been attempts to move things in the kernel to using lists?
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.
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
Pierre-Marie Pédrot (Apr 12 2022 at 19:44):per n elements, lists are 3n words when arrays are n + 1
Enrico Tassi (Apr 12 2022 at 19:44):Exactly, space consumption is surely relevant.
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
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.
Pierre-Marie Pédrot (Apr 12 2022 at 19:46):did you remove the mutable node altogether?
Enrico Tassi (Apr 12 2022 at 19:47):IIRC yes,the branch is this one: https://github.com/gares/coq/tree/speedup/tcomp
Enrico Tassi (Apr 12 2022 at 19:47):but it does many more things, not sure it is usable
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
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)
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
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)
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
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
Pierre-Marie Pédrot (Apr 12 2022 at 19:51):more sharing can be contraproductive in conversion, for instance
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).
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
Enrico Tassi (Apr 12 2022 at 20:00):The more I look at my old code, and the more I doubt about my recollections
Enrico Tassi (Apr 12 2022 at 20:00):maybe it's time to go to bed ;-)
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.
Enrico Tassi (Apr 27 2022 at 14:44):Well, anything is better than binary applications ;-)
Last updated: Jun 04 2023 at 19:30 UTC