Stream: Elpi users & devs

Topic: Generating large Coq term of type `list N` in Elpi

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 11:02):

I'm trying to generate a long list of random natural numbers in Coq-Elpi, and it fails with a stack overflow when the length becomes larger (approx. 50,000). Is there any way to fix this? https://github.com/pi8027/stablesort/blob/master/benchmark/benchmark.v#L26

pred random-N-list i:int, i:int, o:term.
random-N-list 0 _ {{ @nil N }} :- !.
random-N-list N Bound {{ @cons N lp:H lp:T }} :- std.do! [
  n-constant {random.int Bound} H,
  random-N-list {calc (N - 1)} Bound T
].

view this post on Zulip Enrico Tassi (Apr 10 2021 at 11:32):

Hum, I would try removing std.do!

view this post on Zulip Enrico Tassi (Apr 10 2021 at 11:32):

Also, pass -bt to coqc and post the trace, it may help

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 11:38):

@Enrico Tassi I removed std.do, put a bang instead, and got the following trace:

Error:
Stack overflow.
Raised by primitive operation at Stdlib__hashtbl.find in file "hashtbl.ml", line 539, characters 9-23
Re-raised at Elpi__Util.Fork.fork.ensure_runtime in file "src/util.ml", line 456, characters 7-14
Called from Elpi__Runtime_trace_off.mk_outcome in file "src/runtime.ml", line 3447, characters 14-23
Called from Elpi__Runtime_trace_off.execute_once in file "src/runtime.ml", line 3464, characters 5-196
Called from Elpi__API.Execute.once in file "src/API.ml" (inlined), line 169, characters 4-55
Called from Coq_elpi_vernacular.run in file "src/coq_elpi_vernacular.ml", line 720, characters 11-53
Called from Coq_elpi_vernacular.run_and_print in file "src/coq_elpi_vernacular.ml", line 730, characters 8-60
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 28, characters 19-23
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 213, characters 24-64
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 82, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 262, characters 18-43
Called from Vernacinterp.vernac_timeout in file "vernac/vernacinterp.ml" (inlined), line 87, characters 4-7
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 260, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2153, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 956, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2295, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2477, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.finish in file "stm/stm.ml" (inlined), line 2488, characters 12-50
Called from Stm.process_transaction.(fun) in file "stm/stm.ml", line 2749, characters 22-45
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Stm.add in file "stm/stm.ml", line 2846, characters 8-50
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 61, characters 28-90
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, 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 82, characters 4-38
Called from Flags.with_option in file "lib/flags.ml" (inlined), line 26, characters 24-78
Called from Flags.silently in file "lib/flags.ml" (inlined), line 67, characters 19-40
Called from Vernac.load_vernac_core.loop in file "toplevel/vernac.ml", line 111, characters 8-69
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 115, characters 6-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 82, characters 4-38
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 119, characters 4-28
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 148, characters 18-89
Called from Ccompile.compile_files in file "toplevel/ccompile.ml" (inlined), line 227, characters 12-37
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from Coqc.coqc_main in file "toplevel/coqc.ml", line 47, characters 2-81

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 11:47):

Ah, this failure comes from somewhere else! Sorry, my bad.

view this post on Zulip Enrico Tassi (Apr 10 2021 at 11:48):

So, without std.do you consume less stack? (I was not sure)

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 11:52):

From what I observed, I don't think so. (and now I don't get where it fails...)

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 11:53):

I mean, if I put coq.say "something" after the possibly problematic call of random-N-list, I see "something" in the output.

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 12:01):

It seems to execute std.map here but does not reach the execution of its second argument c\ r\ sigma .... https://github.com/pi8027/stablesort/blob/master/benchmark/benchmark.v#L40

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 12:32):

I think I managed to minimize the problem but not entirely sure if this is the same problem:

From Coq Require Import NArith.
From elpi Require Import elpi.
From mathcomp Require Import all_ssreflect.

Definition length (T : Type) (xs : list T) : N :=
  (fix rec (xs : list T) (acc : N) :=
     if xs is _ :: xs then rec xs (N.succ acc) else acc) xs N.zero.

Eval vm_compute in length _ (nseq 50000 tt).

Elpi Command test.
Elpi Accumulate lp:{{

pred gen-unit-list i:int, o:term.
gen-unit-list 0 {{ @nil unit }} :- !.
gen-unit-list N {{ @cons unit tt lp:T }} :- !, gen-unit-list {calc (N - 1)} T.

main _ :-
  gen-unit-list 50000 NS,
  coq.reduction.vm.whd_all {{ @length unit lp:NS }} {{ N }} _.

}}.
Elpi Typecheck.

Elpi test. (* Stack overflow *)

And I see the following trace. Indeed, converting a large Coq term in the Elpi representation to a kernel term can cause this issue!

Error:
Stack overflow.
Raised by primitive operation at Coq_elpi_HOAS.get_options.locality in file "src/coq_elpi_HOAS.ml", line 630, characters 12-29
Called from Elpi__Data.BuiltInPredicate.ADT.adt in file "src/data.ml", line 1017, characters 18-79
Called from Coq_elpi_HOAS.in_coq_gref in file "src/coq_elpi_HOAS.ml", line 309, characters 20-59
Called from Coq_elpi_HOAS.lp2constr in file "src/coq_elpi_HOAS.ml" (inlined), line 1126, characters 12-62
Called from Coq_elpi_HOAS.lp2constr in file "src/coq_elpi_HOAS.ml", line 1188, characters 30-48
Called from Elpi__API.BuiltInData.map_acc.aux in file "src/API.ml", line 395, characters 24-29
Called from Coq_elpi_HOAS.lp2constr in file "src/coq_elpi_HOAS.ml", line 1189, characters 31-83
Called from Elpi__API.BuiltInData.map_acc.aux in file "src/API.ml", line 395, characters 24-29
Called from Coq_elpi_HOAS.lp2constr in file "src/coq_elpi_HOAS.ml", line 1189, characters 31-83
Called from Elpi__API.BuiltInData.map_acc.aux in file "src/API.ml", line 395, characters 24-29
Called from Coq_elpi_HOAS.lp2constr in file "src/coq_elpi_HOAS.ml", line 1189, characters 31-83
Called from Elpi__API.BuiltInData.map_acc.aux in file "src/API.ml", line 395, characters 24-29

view this post on Zulip Enrico Tassi (Apr 10 2021 at 14:20):

Indeed the readback/embed functions are not tail recursive for simplicity.

view this post on Zulip Enrico Tassi (Apr 10 2021 at 14:21):

If it is blocking, I can try to improve on that. But in the meanwhile you can run ulimit -s unlimited on your machine, that should suffice

view this post on Zulip Enrico Tassi (Apr 10 2021 at 14:22):

The reason is that there is a lot of non tail rec code in Coq already, if I improve the readback but then things blow up two calls later, not sure it is worth it

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 14:28):

Make sense. For me, the actual problem is that there is no other handy random number generator I can use inside Coq. I should probably rather think about implementing one in Gallina or writing a small plugin in ML.

view this post on Zulip Enrico Tassi (Apr 10 2021 at 15:06):

May I suggest to build smaller lists, and the append them using a galina program

view this post on Zulip Kazuhiko Sakaguchi (Apr 10 2021 at 16:35):

@Enrico Tassi That's possible. Also, it seems better to declare a constant for that long list to prevent a (costly) readback in the measurement (std.time), and then I want to declare that constant as in Definition ident := Eval vm_compute in large_list so that computation of that concatenation is done before the measurement (without causing a stack overflow by a readback). But I don't find a way to do this with coq.env.add-const.

view this post on Zulip Enrico Tassi (Apr 10 2021 at 16:38):

There is no suppor for := Eval this :-/

Last updated: Oct 13 2024 at 01:02 UTC