Stream: Coq devs & plugin devs

Topic: Minimize bug without location


view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:48):

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?

view this post on Zulip Jason Gross (Mar 04 2023 at 20:50):

Stick idtac "File: ""..."" line ...:"; idtac "Error" on the line before the stack overflow, mimicking the format of Coq's errors

view this post on Zulip Jason Gross (Mar 04 2023 at 20:51):

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

view this post on Zulip Jason Gross (Mar 04 2023 at 20:52):

Or submit a patch to Coq to attach locations to stack overflows

view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:53):

I have Coq vendored so I could quickly patch it

view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:55):

Anyone know how to get a location attached to a stackoverflow?

view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:56):

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

view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:56):

And this stack trace continues for a while

view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:58):

@Jason Gross I like the ltac trick but I couldn't get that to work either

view this post on Zulip Jason Gross (Mar 04 2023 at 20:59):

I like the ltac trick but I couldn't get that to work either

What's the failure mode?

view this post on Zulip Ali Caglayan (Mar 04 2023 at 20:59):

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.

view this post on Zulip Jason Gross (Mar 04 2023 at 20:59):

That's the wrong format

view this post on Zulip Jason Gross (Mar 04 2023 at 21:00):

right format looks like

File "./theories/ToTemplate/Coq/FSets.v", line 73, characters 310-311:
Error: Cannot infer this placeholder of type

view this post on Zulip Ali Caglayan (Mar 04 2023 at 21:01):

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.

view this post on Zulip Ali Caglayan (Mar 04 2023 at 21:02):

Ah I am missing a ","

view this post on Zulip Jason Gross (Mar 04 2023 at 21:02):

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'

view this post on Zulip Ali Caglayan (Mar 04 2023 at 21:02):

No thats not it

view this post on Zulip Ali Caglayan (Mar 04 2023 at 21:02):

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.

view this post on Zulip Jason Gross (Mar 04 2023 at 21:02):

No : after File

view this post on Zulip Ali Caglayan (Mar 04 2023 at 21:03):

Ok were good its chugging away

view this post on Zulip Ali Caglayan (Mar 04 2023 at 21:03):

Thanks!

view this post on Zulip Ali Caglayan (Mar 04 2023 at 22:01):

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