Touchy compilation #869
Description
My Debian package for coq-elpi's construction is failing quite often, because of a timeout:
File "./apps/tc/tests/tlc.v", line 44, characters 4-49:
Error:
Timeout!
Raised at Unicode.next_utf8 in file "clib/unicode.ml", line 153, characters 16-34
Called from Unicode.ident_refutation.aux in file "clib/unicode.ml", line 258, characters 26-39
Called from Unicode.ident_refutation in file "clib/unicode.ml", line 262, characters 16-21
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from VernacControl.under_control in file "vernac/vernacControl.ml", line 206, characters 10-60
Called from Vernacinterp.interp_control_gen in file "vernac/vernacinterp.ml", lines 36-40, characters 4-7
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 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 Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 151, 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 165, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2025, characters 20-47
Called from Stm.Reach.known_state.resilient_tactic in file "stm/stm.ml", line 1964, characters 10-14
Called from Stm.State.define in file "stm/stm.ml", line 963, 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 2203-2204, characters 4-74
Called from Stm.observe in file "stm/stm.ml", line 2295, 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 83, 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 127-145, characters 8-12
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 150, 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 227, characters 30-83
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 68, characters 18-78
Called from Ccompile.compile in file "toplevel/ccompile.ml" (inlined), line 107, characters 2-59
Called from Ccompile.compile_file in file "toplevel/ccompile.ml", line 116, characters 4-61
Called from Coqc.coqc_main in file "toplevel/coqc.ml", lines 38-39, characters 2-56
Called from Coqc.coqc_run in file "toplevel/coqc.ml", line 54, characters 4-36
as I see this on my own box with little load, I'm worried none of the build bot will ever manage to get through, especially on exotic architectures. I patched to increase the timeout length to stabilize things.