I should expect Coq's logic monad to be properly tail-recursive, right? If that fails on ARM64 and I get a stack overflow, but not on x86, is this an OCaml bug? We're wondering with @Janno, but here's an highlight:
$ fgrep 'camlProofview__anon_fn$5blogic_monad$2eml$3a191$2c15$2d$2d96$5' bt-all.txt|wc -l 231582 $ fgrep -v 'camlProofview__anon_fn$5blogic_monad$2eml$3a191$2c15$2d$2d96$5' bt-all.txt|wc -l 202
We're somewhat confident this is arch-specific, since on x86_64 requires take more stack space...
To be a bit more specific about the stack space: I can compile the file on my x64 system with 260KB of stack space and it requires somewhere between 8 and 16MB on Paolo's machine.
Here's also the filtered stack trace: https://gist.github.com/Blaisorblade/688e0bce54a7431843e30db64abae664...
Of course, there's plenty of other fun stuff going on in the offending code, but TCO failing on a continuation monad could be a bigger compiler bug (even if it's not yet blocking).
BTW, I got essentially the same symptoms on OCaml 4.13.1 and 4.10.2 (all with flambda), and probably with some intermediate versions as well. The only difference is a known issue (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/PSA.3A.20ARM.20OCaml.20.3C4.2E13.20reports.20stack.20overflows.20as.20SIGSEGV).
what's the .v source?
we don't have (yet) a minimization we can share :-(, apologies
Ltac bad := bad. Lemma foo : False. bad.
stack overflows in a couple seconds with my dev coq, but my opam coq doesn't seem to stack overflow
possibly a difference between ocamlopt -opaque vs cross module optimized
Hm, now wondering whether
@tailcall be appropriate, and where exactly...
the backtrace looks like
Error: Stack overflow. Raised by primitive operation at file "clib/int.ml", line 22, characters 16-23 Called from file "map.ml", line 123, characters 18-33 Called from file "map.ml", line 127, characters 21-33 Called from file "map.ml", line 130, characters 21-33 Called from file "plugins/ltac/tacinterp.ml", line 1283, characters 18-50 Called from file "engine/logic_monad.ml", line 192, characters 38-43 Called from file "engine/logic_monad.ml", line 260, characters 6-27 Called from file "engine/logic_monad.ml", line 67, characters 36-42 Called from file "engine/logic_monad.ml", line 67, characters 36-42 ....
Hmm... our stacktrace seems almost entirely made of the bind operation (line
191) — we never got an OCaml stacktrace.
I've seen another such issue, fixed by OCaml 4.14.0: https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Coq.20Platform.20and.20stack.20overflows.
But let's continue the discussion there.
Last updated: May 28 2023 at 13:30 UTC