Compiling lens.v fails with stack overflow on ppc64el #678
Comments
|
Note: this issue is new with OCaml 5.2.0. coq-elpi did build successfully with OCaml 4.14.1: |
|
Stéphane's report is about coq-elpi 2.1.0 ; I also tried with coq-elpi 2.2.3, and the log looks actually worse: |
|
To give a bit more information, failures are with OCaml 5.2.0, elpi 1.18.2 and both coq-elpi 2.1.0 and 2.2.3. I'll try to see what happens with a more recent elpi. |
|
If you |
|
Here is a better backtrace: |
|
That seems short for a stack overflow, but IDK how to get something more complete. |
|
(typical stack overflow looks like Set Debug "backtrace".
Compute 50000.
(* Error:
Stack overflow.
Raised by primitive operation at Vnorm.app_type in file "pretyping/vnorm.ml", line 61, characters 10-31
Called from Vnorm.construct_of_constr in file "pretyping/vnorm.ml", line 85, characters 19-61
Called from Vnorm.construct_of_constr_block in file "pretyping/vnorm.ml" (inlined), line 101, characters 32-57
Called from Vnorm.nf_whd in file "pretyping/vnorm.ml", line 182, characters 22-65
Called from Vnorm.nf_val in file "pretyping/vnorm.ml" (inlined), line 147, characters 31-70
then repeat the following many times
Called from Vnorm.nf_telescope.init in file "pretyping/vnorm.ml", line 357, characters 16-40
Called from Stdlib__Array.init in file "array.ml", line 54, characters 22-27
Called from Vnorm.nf_telescope in file "pretyping/vnorm.ml", line 362, characters 13-32
Called from Vnorm.nf_bargs in file "pretyping/vnorm.ml", line 374, characters 9-43
Called from Vnorm.nf_whd in file "pretyping/vnorm.ml", line 183, characters 17-46
Called from Vnorm.nf_val in file "pretyping/vnorm.ml" (inlined), line 147, characters 31-70
*)) |
|
Could it be that the overflow happens outside of Coq's reach with elpi? |
|
What is weird is that I see no elpi stack frame |
|
Maybe there is a silly catch all in coq-elpi that erases the stack and the rethrows the exception.. but I don't even see that entry in the trace |
|
Am I right that ppc native backend was added in 5.2? Are there known limitations, like stack size consumption? |
|
I don't think ppc64el was added with OCaml 5.2.0 since we already had the packages before... but indeed OCaml 5.2.0 might have changed something somewhere... |
What about ocaml 5.1? Or is 5.2 the first post-5 version tested? |
|
It is the first OCaml 5 ; Debian is only transitioning out of OCaml 4 now. |
|
So it could be that the 5.2 ppc backend uses more stack than the 4.14 one. |
|
cc @xavierleroy |
|
It is true that the PPC back-end produces larger stack frames than the other back-ends, but stack limits in OCaml 5 are much much higher than those in OCaml 4, so I doubt this explains the observed failure. There may be something wrong in the OCaml 5 PPC code generator and runtime support, as it is new code since OCaml 5.2, but it's impossible to tell from the backtrace (which may very well be incorrect itself). Is it possible to run the invocation of coqc under gdb, with a breakpoint on |
|
@glondu @SnarkBoojum I have no more access to the Debian cluster, so you will have to do it yourself. |
|
I found the time to experiment more ; with coq-elpi 2.2.3 there are even more stack overflows: apps/derive/theories/derive/param1_functor.v, apps/tc/theories/add_commands.v, apps/eltac/theories/injection.v... Coming back to coq-elpi 2.1.0, I tried to run the compilation in gdb, but didn't manage. I moved to coq-elpi-2.1.0/apps/derive/, then ran "gdb coqc", then: then 'run'... and I got the same error, but no backtrace. What did I do wrong? |
|
I have access to a POWER9 machine and may be able to investigate this. Could you please give me precise instructions on what packages to install, what sources to download, and what commands to issue to reproduce the problem? |
|
On a Debian box, "apt-get build-dep coq-elpi" as administrator will give all build-time dependencies, then as user "apt-get source coq-elpi" will download and unpack the source directory; then after "cd coq-elpi-*", running "dpkg-buildpackage" should compile until the error. Is the box you have access to a ppc64el? It is possible to grant a temporary access to the Debian box I use if you need... see how here |
|
My box runs Ubuntu 24.04 and I don't want to install .deb packages from Debian unstable. Any instructions using only OPAM packages and source tarballs (or git clone) ? |
|
You can setup an unstable schroot - so those packages won't pollute your main system, but you'll still be able to reproduce. That's what I do on the porterbox anyway. There are helper scripts which have the necessary admin access I lack to setup said schroot so I don't know how to do that part unfortunately... Probably this can help |
I can reproduce similar failures (i.e. stack overflows when compiling .v files) with the following commands (in a clean sid chroot + opam git libgmp-dev pkg-config, it should work on Ubuntu 24.04 as well): |
|
Thanks for the instructions, short and sweet. Analysis and fix at ocaml/ocaml#13410 |
|
@xavierleroy will that fox go in an official release soon? @glondu depending on the answer, perhaps the Debian package for OCaml will either be that new version or a patched version? |
|
I've patched the Debian package. |
|
coq-elpi now builds fine. Thanks! |
https://buildd.debian.org/status/fetch.php?pkg=coq-elpi&arch=ppc64el&ver=2.1.0-1%2Bb4&stamp=1723353304&raw=0
I have no clue on how to debug this. Any idea?
Also reported as https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1078549
The text was updated successfully, but these errors were encountered: