It seems that the async test-suite is consistently failing with the four output test failures:
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)
Is this a known issue?
cc @Enrico Tassi
Can you point me to the log (artifacts). The first for example is very simple
==========> 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... )
Théo Zimmermann said:
Is this a known issue?
Not known to me, also this test was added not a long ago
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.
Indeed, I do confirm that these tests are failing consistently ever since they were introduced.
Here's an example (latest pipeline on master): https://gitlab.com/coq/coq/-/jobs/565419053
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.
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)
So it looks like the warning of the initial state is repeated. Could this be an async bug?
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 <
You didn't use the -ri Extraction
(from the first line of the file)
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)
oh, right!
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
So does this mean that something could be fixed in the async implementation?
Do we pass -set/-unset? if yes maybe we should stop
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.
I'm sorry I've missed coq/coq#12005, otherwise I would have told you this earlier
Last updated: Oct 13 2024 at 01:02 UTC