I managed to run into a stack overflow in the wild, however Coq is not reporting a location so the bug minimizer doesn't know what to do. @Jason Gross any ideas how I can get the bug minimizer to accept the error?
Stick idtac "File: ""..."" line ...:"; idtac "Error"
on the line before the stack overflow, mimicking the format of Coq's errors
It'll go better if the line numbers are correct, but I'm pretty sure I made it robust to incorrect line numbers on the error message
Or submit a patch to Coq to attach locations to stack overflows
I have Coq vendored so I could quickly patch it
Anyone know how to get a location attached to a stackoverflow?
The overflow I am getting is here:
Error:
Stack overflow.
Raised by primitive operation at Stdlib.max in file "stdlib.ml", line 75, characters 17-23
Called from Gramlib__LStream.peek in file "coq-lsp/vendor/coq/gramlib/lStream.ml", line 59, characters 45-91
Called from Gramlib__Grammar.GMake.parser_of_token_list.(fun) in file "coq-lsp/vendor/coq/gramlib/grammar.ml", line 1318, characters 10-42
Called from Gramlib__Grammar.GMake.parser_of_tree.(fun) in file "coq-lsp/vendor/coq/gramlib/grammar.ml", line 1194, characters 16-32
Called from Gramlib__Grammar.GMake.start_parser_of_levels.(fun) in file "coq-lsp/vendor/coq/gramlib/grammar.ml", line 1525, characters 27-43
Called from Gramlib__Grammar.GMake.parser_of_tree.(fun) in file "coq-lsp/vendor/coq/gramlib/grammar.ml", line 1201, characters 21-37
Called from Gramlib__Grammar.GMake.start_parser_of_levels.(fun) in file "coq-lsp/vendor/coq/gramlib/grammar.ml", line 1525, characters 27-43
And this stack trace continues for a while
@Jason Gross I like the ltac trick but I couldn't get that to work either
I like the ltac trick but I couldn't get that to work either
What's the failure mode?
This file produces the following output when Coq'ed:
File: "foobar" line 2:4
Error: Stack overflow.
Does this output display the correct error? [(y)es/(n)o] y
The current state of the file does not have a recognizable error.
Please enter a regular expression which matches on the output. Leave blank to re-coq the file.
That's the wrong format
right format looks like
File "./theories/ToTemplate/Coq/FSets.v", line 73, characters 310-311:
Error: Cannot infer this placeholder of type
hmm still not working:
File: "./foobar.v" line 2, characters 4-5:
Error: Stack overflow.
Does this output display the correct error? [(y)es/(n)o] y
The current state of the file does not have a recognizable error.
Please enter a regular expression which matches on the output. Leave blank to re-coq the file.
Ah I am missing a ","
It needs to match the regex at https://github.com/JasonGross/coq-tools/blob/9e56b1d73d247ffc992a10d617df1e07094b0ed2/diagnose_error.py#L16
'File "[^"]+", line ([0-9]+), characters ([0-9]+)-([0-9]+):\n'
No thats not it
File: "./foobar.v", line 2, characters 4-5:
Error: Stack overflow.
Does this output display the correct error? [(y)es/(n)o] y
The current state of the file does not have a recognizable error.
Please enter a regular expression which matches on the output. Leave blank to re-coq the file.
No :
after File
Ok were good its chugging away
Thanks!
OK I have managed to minimise the bug by hand even further https://github.com/coq/coq/issues/17342
Last updated: Oct 13 2024 at 01:02 UTC