search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
139 stars 51 forks source link

Compiling lens.v fails with stack overflow on ppc64el #678

Closed glondu closed 1 month ago

glondu commented 2 months ago

https://buildd.debian.org/status/fetch.php?pkg=coq-elpi&arch=ppc64el&ver=2.1.0-1%2Bb4&stamp=1723353304&raw=0

COQC theories/derive/lens.v
File "./theories/derive/lens.v", line 45, characters 0-15:
Error: Stack overflow.

I have no clue on how to debug this. Any idea?

Also reported as https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1078549

glondu commented 2 months ago

Note: this issue is new with OCaml 5.2.0. coq-elpi did build successfully with OCaml 4.14.1:

https://buildd.debian.org/status/fetch.php?pkg=coq-elpi&arch=ppc64el&ver=2.1.0-1%2Bb3&stamp=1722741374&raw=0

SnarkBoojum commented 2 months ago

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:

(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/re -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/str -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -Q apps/derive/elpi elpi.apps.derive.elpi -R apps/derive/theories elpi.apps.derive apps/derive/theories/derive/param1_functor.v)
File "./apps/derive/theories/derive/param1_functor.v", line 32, characters 0-15:
Error: Stack overflow.

(cd _build/default && /usr/bin/coqc -w -all -w -elpi -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/re -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/str -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/zarith -I apps/tc/src -I src -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -Q apps/tc/elpi elpi.apps.tc.elpi -R apps/tc/theories elpi.apps.tc apps/tc/theories/add_commands.v)
File "./apps/tc/theories/add_commands.v", line 64, characters 0-15:
Error: Stack overflow.

(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/re -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/str -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/powerpc64le-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -Q apps/derive/elpi elpi.apps.derive.elpi -Q apps/derive/theories elpi.apps.derive -R apps/eltac/theories elpi.apps.eltac apps/eltac/theories/injection.v)
File "./apps/eltac/theories/injection.v", line 20, characters 0-15:
Error: Stack overflow.

make[2]: *** [Makefile:16: build] Error 1
SnarkBoojum commented 2 months ago

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.

SkySkimmer commented 2 months ago

If you Set Debug "backtrace". before the failing line(s) it may say something informative.

SnarkBoojum commented 2 months ago

Here is a better backtrace:

COQC theories/derive/lens.v
File "./theories/derive/lens.v", line 46, characters 0-15:
Error:
Stack overflow.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 212, characters 16-41
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 226, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2179, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 959, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", lines 2321-2322, characters 4-74
Called from Stm.observe in file "stm/stm.ml", line 2418, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 79, characters 29-50
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 133, characters 16-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml", line 137, characters 6-32
Called from Vernac.load_vernac_core.loop in file "toplevel/vernac.ml", lines 123-141, characters 8-12
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 146, characters 6-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.load_vernac in file "toplevel/vernac.ml", line 222, characters 30-83
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 70, characters 18-78
Called from Ccompile.compile in file "toplevel/ccompile.ml" (inlined), line 126, characters 2-59
Called from Ccompile.compile_file in file "toplevel/ccompile.ml", line 135, characters 4-61
Called from Coqc.coqc_main in file "toplevel/coqc.ml", lines 48-49, characters 2-56
Called from Coqc.coqc_run in file "toplevel/coqc.ml", line 67, characters 4-36

make[5]: *** [Makefile.coq:848: theories/derive/lens.vo] Error 1
SkySkimmer commented 2 months ago

That seems short for a stack overflow, but IDK how to get something more complete.

SkySkimmer commented 2 months ago

(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

*)

)

SnarkBoojum commented 2 months ago

Could it be that the overflow happens outside of Coq's reach with elpi?

gares commented 2 months ago

What is weird is that I see no elpi stack frame

gares commented 2 months ago

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

gares commented 2 months ago

Am I right that ppc native backend was added in 5.2? Are there known limitations, like stack size consumption?

SnarkBoojum commented 2 months ago

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...

SkySkimmer commented 2 months ago

Note: this issue is new with OCaml 5.2.0. coq-elpi did build successfully with OCaml 4.14.1:

What about ocaml 5.1? Or is 5.2 the first post-5 version tested?

SnarkBoojum commented 2 months ago

It is the first OCaml 5 ; Debian is only transitioning out of OCaml 4 now.

gares commented 2 months ago

So it could be that the 5.2 ppc backend uses more stack than the 4.14 one.

SkySkimmer commented 2 months ago

cc @xavierleroy

xavierleroy commented 2 months ago

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 caml_raise_stack_overflow, to see where the Stack_overflow exception is actually raised?

gares commented 2 months ago

@glondu @SnarkBoojum I have no more access to the Debian cluster, so you will have to do it yourself.

SnarkBoojum commented 2 months ago

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:

set args -I ../../src -Q ../../theories elpi -Q elpi elpi.apps.derive -R theories elpi.apps -R tests elpi.apps.derive.tests -R examples elpi.apps.derive.examples theories/derive/lens.v
set logging file ~/gdb.log
set logging enabled on
break caml_raise_stack_overflow

then 'run'... and I got the same error, but no backtrace. What did I do wrong?

xavierleroy commented 2 months ago

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?

SnarkBoojum commented 2 months ago

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

xavierleroy commented 2 months ago

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) ?

SnarkBoojum commented 2 months ago

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

SnarkBoojum commented 2 months ago

Probably better link

glondu commented 2 months ago

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) ?

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):

opam init --bare --disable-sandboxing --no-setup
opam switch create 5.2.0
eval $(opam env --switch=5.2.0)
git clone https://github.com/LPCIC/coq-elpi.git
cd coq-elpi
opam pin .
xavierleroy commented 2 months ago

Thanks for the instructions, short and sweet. Analysis and fix at https://github.com/ocaml/ocaml/pull/13410

SnarkBoojum commented 2 months ago

@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?

glondu commented 2 months ago

I've patched the Debian package.

glondu commented 1 month ago

coq-elpi now builds fine. Thanks!