Stream: Coq devs & plugin devs

Topic: Async test-suite failure


view this post on Zulip Théo Zimmermann (May 23 2020 at 14:41):

It seems that the async test-suite is consistently failing with the four output test failures:

view this post on Zulip Théo Zimmermann (May 23 2020 at 14:41):

2736 FAILURES
2737     output/ErrorLocation_12152_1.v...Error! (unexpected output)
2738     output/ErrorLocation_12152_2.v...Error! (unexpected output)
2739     output/ErrorLocation_12255.v...Error! (unexpected output)
2740     output/interleave_options_bad_order.v...Error! (unexpected output)

view this post on Zulip Théo Zimmermann (May 23 2020 at 14:41):

Is this a known issue?

view this post on Zulip Théo Zimmermann (May 23 2020 at 14:41):

cc @Enrico Tassi

view this post on Zulip Enrico Tassi (May 24 2020 at 16:46):

Can you point me to the log (artifacts). The first for example is very simple

view this post on Zulip Enrico Tassi (May 24 2020 at 16:58):

==========> TESTING output/ErrorLocation_12152_1.v <==========
--- output/ErrorLocation_12152_1.out    2020-05-24 15:24:17.000000000 +0000
+++ output/ErrorLocation_12152_1.out.real   2020-05-24 15:31:36.000000000 +0000
@@ -1,3 +1 @@
-File "stdin", line 3, characters 0-7:
-Error: No product even after head-reduction.
-
+Error: There are pending proofs: Unnamed_thm.
0m0.000000s 0m0.000000s
0m0.050000s 0m0.030000s
==========> FAILURE <==========
    output/ErrorLocation_12152_1.v...Error! (unexpected output)

The test has an unfinished proof which is quite weird. Without more verbose output I cannot say for sure, but it is looking for problems: there is an error in the main document (unfinished proof) and an error in a proof (no product). If you want to race... I suggest adding the Qed and also adding Fail (it also means we don't care if .out tests fail badly, as long as they print what we exepect... )

view this post on Zulip Enrico Tassi (May 24 2020 at 18:25):

Théo Zimmermann said:

Is this a known issue?

Not known to me, also this test was added not a long ago

view this post on Zulip Théo Zimmermann (May 25 2020 at 12:45):

OK thanks, indeed: these are all new tests, so not surprising (given that async is in allow failure mode) that they are unreliable and this was not noticed.

view this post on Zulip Théo Zimmermann (May 25 2020 at 12:52):

Indeed, I do confirm that these tests are failing consistently ever since they were introduced.

view this post on Zulip Théo Zimmermann (May 25 2020 at 12:53):

Here's an example (latest pipeline on master): https://gitlab.com/coq/coq/-/jobs/565419053

view this post on Zulip Théo Zimmermann (May 25 2020 at 12:58):

I understand the suggestion about Qed, but I'm not sure of the one about Fail since adding Fail to a command prevents having precise error locations.

view this post on Zulip Théo Zimmermann (May 25 2020 at 13:01):

Regarding the interleave test, the artifact is:

==========> TESTING output/interleave_options_bad_order.v <==========
--- output/interleave_options_bad_order.out 2020-05-14 21:45:08.552458662 +0000
+++ output/interleave_options_bad_order.out.real    2020-05-24 17:34:12.867368215 +0000
@@ -1,4 +1,6 @@
 While loading initial state:
 Warning: There is no flag or option with this name: "Extraction Optimize".
 [unknown-option,option]
+Warning: There is no flag or option with this name: "Extraction Optimize".
+[unknown-option,option]
 Extraction Optimize is on
0m0.000000s 0m0.000000s
0m0.050000s 0m0.040000s
==========> FAILURE <==========
    output/interleave_options_bad_order.v...Error! (unexpected output)

view this post on Zulip Théo Zimmermann (May 25 2020 at 13:03):

So it looks like the warning of the initial state is repeated. Could this be an async bug?

view this post on Zulip Enrico Tassi (May 25 2020 at 18:39):

This one looks very weird, and I don't see to have the same behavior here:

gares@ollypat:~/COQ/master$ bin/coqtop < test-suite/output/interleave_options_bad_order.v
Welcome to Coq ollypat:/home/gares/COQ/master,master (ea6cb6b542e8c356192bb77f234586e0f6d55c8c)

Coq < Coq < Coq < Toplevel input, characters 74-99:
> Test Extraction Optimize.
> ^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
There is no flag, option or table with this name: "Extraction Optimize".

Coq <
gares@ollypat:~/COQ/master$ bin/coqtop -async-proofs on < test-suite/output/interleave_options_bad_order.v
Welcome to Coq ollypat:/home/gares/COQ/master,master (ea6cb6b542e8c356192bb77f234586e0f6d55c8c)

Coq < Coq < Coq < Toplevel input, characters 74-99:
> Test Extraction Optimize.
> ^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
There is no flag, option or table with this name: "Extraction Optimize".

Coq <

view this post on Zulip Gaëtan Gilbert (May 25 2020 at 19:14):

You didn't use the -ri Extraction (from the first line of the file)

view this post on Zulip Gaëtan Gilbert (May 25 2020 at 19:17):

Théo Zimmermann said:

So it looks like the warning of the initial state is repeated. Could this be an async bug?

Probably a worker is started and gets the same bad options as the main process so the warning gets duplicated
Not a bug IMO, the easiest solution may be to disable async for that test (like eg the unifconstraints output test)

view this post on Zulip Enrico Tassi (May 25 2020 at 19:57):

oh, right!

view this post on Zulip Enrico Tassi (May 25 2020 at 19:58):

but it is also not necessary to pass -ri to workers, since they get a system state (that includes required stuff) together with a job

view this post on Zulip Théo Zimmermann (May 25 2020 at 20:26):

So does this mean that something could be fixed in the async implementation?

view this post on Zulip Gaëtan Gilbert (May 25 2020 at 20:32):

Do we pass -set/-unset? if yes maybe we should stop

view this post on Zulip Enrico Tassi (May 25 2020 at 20:34):

The current implementation is fragile, since options are filtered "by hand" on a "I guess so" basis. https://github.com/coq/coq/blob/8b3ce7442dcbcdf3d6b43efd0360ead334819913/stm/asyncTaskQueue.ml#L121 . I think we should "flag" all options with a bit that tells if they have to be passes to the workers in a single place (which is not the code spawning a worker, but the code declaring the option).

We pass to the workers a summary, so anything that is stored there does not need to be passed, at least in theory.

view this post on Zulip Enrico Tassi (May 25 2020 at 20:40):

I'm sorry I've missed coq/coq#12005, otherwise I would have told you this earlier


Last updated: Oct 16 2021 at 07:02 UTC