We are getting these failures when the testsuite runs:
99% tests passed, 18 tests failed out of 3582
Total Test time (real) = 1694.23 sec
The following tests FAILED:
167 - tests/lean/PPRoundtrip.lean (Failed)
491 - tests/lean/replaceLocalDeclInstantiateMVars.lean (Failed)
508 - tests/lean/scopedInstanceOutsideNamespace.lean (Failed)
510 - tests/lean/scopedMacros.lean (Failed)
1126 - tests/lean/run/983.lean (Failed)
1142 - tests/lean/run/ExprLens.lean (Failed)
1151 - tests/lean/run/PPTopDownAnalyze.lean (Timeout)
1203 - tests/lean/run/async_select_channel.lean (Failed)
1344 - tests/lean/run/collectLooseBVars.lean (Failed)
1544 - tests/lean/run/eqnsPrio.lean (Failed)
2322 - tests/lean/run/letToHave.lean (Failed)
2342 - tests/lean/run/library_suggestions_mepo.lean (Failed)
2813 - tests/lean/run/splitIfIssue.lean (Failed)
2929 - tests/lean/run/tactic_config.lean (Failed)
2985 - tests/lean/run/try_heartbeats.lean (Failed)
2989 - tests/lean/run/try_parallelism.lean (Failed)
2992 - tests/lean/run/try_user_suggestions.lean (Failed)
3071 - tests/lean/run/whereCmd.lean (Failed)
However, each of them succeeds when run standalone.
There is parallel contention going on that needs to be fixed.
Version: 4.29.0
We are getting these failures when the testsuite runs:
However, each of them succeeds when run standalone.
There is parallel contention going on that needs to be fixed.
Version: 4.29.0