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