some test in ci/coq-tests.el fails sporadically

[hendriktews]

See for instance the test on #536, started around 6pm. When rerun on 10pm these tests succeeded.

[erikmd]

Hi @hendriktews, thanks for opening this! yes that's an issue I had noticed and which should definitely be solved…

see also FYI the other issue I had already raised in PR #506:
much more tests had failed, but only with Coq 8.12, cf. this job
https://github.com/ProofGeneral/PG/actions/runs/153948280
but please, do not restart the jobs for the moment in the run
https://github.com/ProofGeneral/PG/actions/runs/153948280 to keep track of that issue,
I guess we should first try to reproduce the issue locally, and finally add commits in the PR #506 to test Coq 8.13 as well…

[hendriktews]

I suggest that we download the logs and attach them here, when there is another sporadic failure.

[hendriktews]

Another sporadic error: 081_coq-test-regression-show-proof-diffs fails on #540 in the run on Jan 9:

2021-01-09T13:31:47.9313750Z Test 081_coq-test-regression-show-proof-diffs condition:
2021-01-09T13:31:47.9314611Z     (ert-test-failed
2021-01-09T13:31:47.9315020Z      ((should
2021-01-09T13:31:47.9315550Z        (string-match-p regexp
2021-01-09T13:31:47.9316125Z 		       (string-trim ...)))
2021-01-09T13:31:47.9316499Z       :form
2021-01-09T13:31:47.9317130Z       (string-match-p "(fun (A : Prop) (proof_of_A : A) => \\?Goal)" "")
2021-01-09T13:31:47.9317638Z       :value nil))
2021-01-09T13:31:47.9322793Z ##[error]   FAILED  10/10  081_coq-test-regression-show-proof-diffs

Apparently, the response buffer is empty. Are you sure that (proof-shell-wait) waits long enough? Full log:
log-test-8.9-minimal.zip

[hendriktews]

This time it hit 020_coq-test-definition backtrace twice in PR #559. For 8.10:

2021-03-16T21:14:22.3721762Z Test 020_coq-test-definition condition:
2021-03-16T21:14:22.3722574Z     (ert-test-failed
2021-03-16T21:14:22.3723075Z      ((should
2021-03-16T21:14:22.3723737Z        (string-match-p regexp
2021-03-16T21:14:22.3724478Z 		       (string-trim ...)))
2021-03-16T21:14:22.3724929Z       :form
2021-03-16T21:14:22.3725629Z       (string-match-p "trois is defined" "")
2021-03-16T21:14:22.3726211Z       :value nil))
2021-03-16T21:14:22.3732087Z ##[error]   FAILED   2/10  020_coq-test-definition

For 8.11:

2021-03-16T21:14:33.6778849Z Test 020_coq-test-definition condition:
2021-03-16T21:14:33.6779558Z     (ert-test-failed
2021-03-16T21:14:33.6780007Z      ((should
2021-03-16T21:14:33.6781051Z        (string-match-p regexp
2021-03-16T21:14:33.6781930Z 		       (string-trim ...)))
2021-03-16T21:14:33.6782686Z       :form
2021-03-16T21:14:33.6783493Z       (string-match-p "trois is defined" "")
2021-03-16T21:14:33.6784027Z       :value nil))
2021-03-16T21:14:33.6790766Z ##[error]   FAILED   2/10  020_coq-test-definition

Again, this looks like a timing issue, because the response buffer seems to be empty. Logs are attached.
557-error-021-2021-03-16.zip

[hendriktews]

The second run on #559 produced another error on 020_coq-test-definition, this time only for 8.10:

2021-03-17T07:20:12.0182635Z Test 020_coq-test-definition condition:
2021-03-17T07:20:12.0183370Z     (ert-test-failed
2021-03-17T07:20:12.0183820Z      ((should
2021-03-17T07:20:12.0184450Z        (string-match-p regexp
2021-03-17T07:20:12.0185437Z 		       (string-trim ...)))
2021-03-17T07:20:12.0186145Z       :form
2021-03-17T07:20:12.0186980Z       (string-match-p "trois is defined" "")
2021-03-17T07:20:12.0187493Z       :value nil))
2021-03-17T07:20:12.0193776Z ##[error]   FAILED   2/10  020_coq-test-definition

logs: 559-error-020-2021-03-17.zip
The third run succeeded then.

[hendriktews]

Has anybody seen an instance of this since we merged #564? I suspect this issue has also been fixed by this PR.

[hendriktews]

was seemingly fixed by #564, closing