379/1325 Test #283: leantest_non_meta_rec_fn.lean ...............................***Failed 0.05 sec
-- testing non_meta_rec_fn.lean
-- using result from test_all.sh
--- non_meta_rec_fn.lean.expected.out 2019-10-17 20:25:29.000000000 +0000
+++ non_meta_rec_fn.lean.produced.out 2019-10-17 20:34:55.000000000 +0000
@@ -1,4 +1,4 @@
-non_meta_rec_fn.lean:3:36: error: failed to prove recursive application is decreasing, well founded relation
+non_meta_rec_fn.lean:3:0: error: failed to prove recursive application is decreasing, well founded relation
@has_well_founded.r true (@has_well_founded_of_has_sizeof true (default_has_sizeof true))
Possible solutions:
- Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
ERROR: file non_meta_rec_fn.lean.produced.out does not match non_meta_rec_fn.lean.expected.out
It seems to happen randomly; I think I've seen it go away after the job was restarted.
Here are a bunch of other instances I found in the travis "build history" tab which go back several months:
Sometimes the macOS clang++ travis build fails during the
cteststep inleantest_non_meta_rec_fn.leanlike this:It seems to happen randomly; I think I've seen it go away after the job was restarted.
cf. #69 (comment)
Here are a bunch of other instances I found in the travis "build history" tab which go back several months: