Stream: Coq Platform devs & users

Topic: Coq-rewriter stack space


view this post on Zulip Notification Bot (Nov 28 2022 at 18:17):

24 messages were moved here from #Coq Platform devs & users > 2022.09+beta1 release by Karl Palmskog.

view this post on Zulip Paolo Giarrusso (Nov 28 2022 at 19:19):

FWIW, a :+1: from me on "ARM Macs need more stack", even if it's usually fine; there were some documented improvements between 4.10.2 and 4.14, and it was worse early on.

view this post on Zulip Michael Soegtrop (Nov 29 2022 at 10:42):

@Paolo Giarrusso : are you aware of improvements between 4.13.1 and 4.14.x?

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 13:12):

Tail-call with up to 64 arguments are now guaranteed to be optimized for all architectures.

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 13:12):

(all I've seen was listed for https://ocaml.org/releases/4.14.0)

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 13:15):

they also list https://github.com/ocaml/ocaml/pull/10549 but that one was also cherry-picked back to 4.13

view this post on Zulip Michael Soegtrop (Nov 29 2022 at 13:42):

Thanks! I consider switching to 4.14. Are there known issues around Coq?

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 16:40):

Not AFAIK

view this post on Zulip Michael Soegtrop (Dec 01 2022 at 14:37):

@Paolo Giarrusso : since fiat-crypto compiles fine with 64 MB on arm, I refrained from making such a rather large change that late. But I will do it first thing after the release.


Last updated: Jan 30 2023 at 11:03 UTC