Parser stackoverflows on large files

[anton-trunov]

Description of the problem

Consider the following snippet with a lot of identical lines:

Definition foo :=
let x : nat := 0 in
let x : nat := 0 in
let x : nat := 0 in
...
let x : nat := 0 in
x.

It can be generated with the following script (the file is called coq_stress.v):

echo "Definition foo :=\n" > coq_stress.v; perl -e 'print "let x := 0 in\n" x 6288' >> coq_stress.v; echo "x.\n" >> coq_stress.v

Note: 6288 is the number of let x := 0 in in coq_stress.v.

When I run it like so

ulimit -n 24000; coqc -q -debug coq_stress.v

I get

Error:
Stack overflow.
frame @ file "toplevel/coqc.ml", line 67, characters 4-25
frame @ file "toplevel/coqc.ml", line 45, characters 2-81
frame @ file "list.ml", line 110, characters 12-15
frame @ file "toplevel/ccompile.ml", line 214, characters 2-39
frame @ file "toplevel/ccompile.ml", line 148, characters 18-89
frame @ file "toplevel/vernac.ml", line 170, characters 30-88
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "toplevel/vernac.ml", line 114, characters 6-19
frame @ file "toplevel/vernac.ml", line 97, characters 6-89
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 17, characters 14-17
raise @ unknown
frame @ file "vernac/vernacstate.ml", line 22, characters 10-35
raise @ file "clib/exninfo.ml", line 65, characters 2-15

The discussion with @ejgallego and @JasonGross on Zulip
showed this happens deep in the parser mutual loop:

Raised by primitive operation at file "list.ml", line 180, characters 12-23
Called from file "parsing/cLexer.ml", line 401, characters 25-47
Called from file "parsing/cLexer.ml", line 665, characters 19-30
Called from file "parsing/cLexer.ml", line 819, characters 26-48
Called from file "stream.ml", line 86, characters 21-35
Called from file "stream.ml" (inlined), line 95, characters 14-25
Called from file "gramlib/grammar.ml", line 1390, characters 10-26
Called from file "gramlib/grammar.ml", line 1202, characters 28-37
Called from file "gramlib/grammar.ml", line 1423, characters 27-36
Called from file "gramlib/grammar.ml", line 1202, characters 28-37
Called from file "gramlib/grammar.ml", line 1423, characters 27-36
Called from file "gramlib/grammar.ml", line 1139, characters 10-17
Called from file "gramlib/grammar.ml" (inlined), line 1267, characters 15-61
Called from file "gramlib/grammar.ml", line 1269, characters 23-37
Called from file "gramlib/grammar.ml", line 1274, characters 17-31
Called from file "gramlib/grammar.ml", line 1175, characters 21-30
Called from file "gramlib/grammar.ml", line 1423, characters 27-36
Called from file "gramlib/grammar.ml", line 1175, characters 21-30
Called from file "gramlib/grammar.ml", line 1224, characters 6-15
Called from file "gramlib/grammar.ml" (inlined), line 1198, characters 19-57
Called from file "gramlib/grammar.ml", line 1205, characters 29-43
Called from file "gramlib/grammar.ml", line 1224, characters 6-15

As noted by @ejgallego:

This deserves a double bug report, first for the lost backtrace, second for the stack overflow

Coq Version

8.11.1

[ejgallego]

Indeed this is a legitimate stack overflow, there are many strategies that could be used to improve the parser here, in terms of tail-call and stack use.

[silene]

Since OCaml 5 no longer uses the system stack for OCaml code, this issue becomes moot.

[ejgallego]

How does this issue become moot @silene ? AFAICT Coq's parser is still not tail-recursive, so the issue is there.

[silene]

The stack for programs compiled with OCaml 5 is "infinite" (for a large enough definition of infinite), so tail-recursion does not bring much to the table. Perhaps you have an example that does not work on a Coq system compiled with OCaml 5, but at the very least, the test case in this report does pass now.

[ejgallego]

That's interesting, I wasn't aware of the new stack setup OCaml upstream.

Indeed your cleanups make sense, on the other hand we still have quite a few pieces of doc hanging around that are now incorrect for OCaml 5 .