Michael Soegtrop (Nov 28 2022 at 10:59): Michael Soegtrop (Nov 28 2022 at 10:59):@Pierre-Marie Pédrot @Jason Gross : I have an odd issue with Coq-rewriter and Coq 8.16.1: on an Intel Mac it builds fine with 32 MB stack (ulimit -s 32768). On an Apple silicon Mac it does not build with almost twice as much stack. Unfortunately macOS has a hard limit of 65520kB stack size (seriously?). I expect that I am using native ARM Ocaml (it is definitely much faster than the Intel Mac, so I don't think it messed it up in a way which makes me work with Rosetta). Any thoughts?
Btw.: I wanted to also supply an Apple Silicon Coq Platform installer - but I might have to drop rewrite and fiat-crypto for this reason.
Michael Soegtrop (Nov 28 2022 at 11:02):P.S.: I CCed Pierre-Marie above because I thought there is also a difference between 8.16.0 and 8.16.1 in that (I remember some discussions about this), but this does not seem to be the case.
Jason Gross (Nov 28 2022 at 12:27):Ew, really? I'm happy to add a SKIP_ENORMOUS_STACK variable to the Makefile that disables the build of the things that need that much stack. If I'm recalling correctly, it's only solinas_reduction that needs this much stack? Is that right, or are there other targets that fail?
Jason Gross (Nov 28 2022 at 12:32):I think we'd wrap https://github.com/mit-plv/fiat-crypto/blob/d72df784a772ea179243dde8a3ac04c59e3ce70d/Makefile.examples#L123 and the addition of solinas_reduction to https://github.com/mit-plv/fiat-crypto/blob/d72df784a772ea179243dde8a3ac04c59e3ce70d/Makefile.config#L53 in something like ifneq ($(SKIP_ENORMOUS_STACK),1) ... endif.
Jason Gross (Nov 28 2022 at 12:34):Another alternative is that we could possibly set up the ARM build to use Haskell rather than ocamlopt to build extracted code? Idk if that's any better?
Jason Gross (Nov 28 2022 at 12:35):And if you can let me know what's failing, it might be worth opening an issue on the OCaml bug tracker that compiling this file takes too much stack and ocamlopt should be more efficient, or at least have a mode for compiling with less stack?
Michael Soegtrop (Nov 28 2022 at 12:53):@Jason Gross It is this file which fails at 64M stack size:
File "./src/Rewriter/Demo.v", line 20, characters 0-21:
Error: Stack overflow.
but afair it was a different one with 32M - maybe also a randomness in parallel build - I am rerunning it at 32M.
Jason Gross (Nov 28 2022 at 12:56):Line 20 in Demo.v is Search, you should report an issue on the Coq bug tracker requesting that Search be more tail recursive if need be
https://github.com/mit-plv/rewriter/blob/d644f09c90513b0837c2f9f54fd0a19315ee31dd/src/Rewriter/Demo.v#L20
In the meantime you can just patch out that line?
Michael Soegtrop (Nov 28 2022 at 13:16):Hmm OK - a Search (?x + 0 = ?x). really looks rather innocent.
Should I bisect the stack size needed on Intel for this?
Enrico Tassi (Nov 28 2022 at 13:18):We have stack overflows problems on searches like that one using JScoq since many years.
The easy way out is to limit the search to a module, so that the number of results is smaller, eg Search ... inside module_name.
Enrico Tassi (Nov 28 2022 at 13:19):Fixing the issue in Coq would surely be better, just wanted to share a quick work around.
Michael Soegtrop (Nov 28 2022 at 13:20):@Enrico Tassi : can you imagine why ARM would take 2x the amount of stack than Intel?
Michael Soegtrop (Nov 28 2022 at 13:21):@Jason Gross : yes sure I can patch this out. Let's see how far I get with Fiat crypto then ...
Enrico Tassi (Nov 28 2022 at 13:27):Michael Soegtrop said:
Enrico Tassi : can you imagine why ARM would take 2x the amount of stack than Intel?
nope, CC @Gabriel Scherer which surely knows better than me if this is a known issue. Which OCaml version are we talking about BTW?
Michael Soegtrop (Nov 28 2022 at 13:29):COQ_PLATFORM_OCAML_VERSION='4.13.1'
Michael Soegtrop (Nov 28 2022 at 13:31):@Jason Gross : With the patch I get:
File "./src/Rewriter/Language/IdentifiersLibraryProofs.v", line 285, characters 12-29:
Error: Stack overflow.
That is https://github.com/mit-plv/rewriter/blob/d644f09c90513b0837c2f9f54fd0a19315ee31dd/src/Rewriter/Language/IdentifiersLibraryProofs.v#LL285C13-L285C29 which is
https://github.com/mit-plv/rewriter/blob/d644f09c90513b0837c2f9f54fd0a19315ee31dd/src/Rewriter/Language/IdentifiersLibraryProofs.v#L176-L182
None of the tactics here are even recursive (they're all defined right above that tactic), so I don't see what could be taking up stack space. Could you get a stack trace?
Jason Gross (Nov 28 2022 at 13:50):But it's starting to sound like OCaml / Coq on ARM aren't ready for serious development. These aren't even the parts of rewriter and Fiat Crypto that are known to stress various bits of the Coq toolchain
Michael Soegtrop (Nov 28 2022 at 14:01):@Jason Gross : I guess it makes more sense to not ship rewriter and fiat-crypto with the ARM DMG (which I would anyway call experimental). Of course I will include it in the Intel DMG. This looks like we can't solve this between 12 and lunch.
Michael Soegtrop (Nov 28 2022 at 14:02):Possibly I should try a newer OCaml ...
Michael Soegtrop (Nov 28 2022 at 14:05):@Jason Gross : actually good news: for testing I put the stack size back to 32M. When I use 64M, coq rewriter and coq fiat-crypto run through :-)
Michael Soegtrop (Nov 28 2022 at 14:05):So I will include them in the Apple silicon DMG
Gabriel Scherer (Nov 28 2022 at 15:12):nope, CC @Gabriel Scherer which surely knows better than me if this is a known issue.
Stack usage is a system-dependent property, for example some platform may expect call-frame alignment guarantees that artificially inflate stack usage on small non-tail recursive functions. Reporting 2x stack usage differences in corner cases is not terribly surprising.
Note that OCaml 5 does not use the system stack for OCaml calls anymore, so this category of issue will magically disappear.
(OCaml 5 is still somewhat experimental, of course.)
Gabriel Scherer (Nov 28 2022 at 15:12):(Minor note: having everything in a single Zulip thread made it a bit difficult for me to follow this sub-conversation, I would welcome a new topic if there is more about this specific issue.)
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.
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.
Michael Soegtrop (Nov 29 2022 at 10:42):@Paolo Giarrusso : are you aware of improvements between 4.13.1 and 4.14.x?
Paolo Giarrusso (Nov 29 2022 at 13:12):Tail-call with up to 64 arguments are now guaranteed to be optimized for all architectures.
Paolo Giarrusso (Nov 29 2022 at 13:12):(all I've seen was listed for https://ocaml.org/releases/4.14.0)
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
Michael Soegtrop (Nov 29 2022 at 13:42):Thanks! I consider switching to 4.14. Are there known issues around Coq?
Paolo Giarrusso (Nov 29 2022 at 16:40):Not AFAIK
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: Jun 03 2023 at 04:30 UTC