Zulip Chat Archive

Stream: general

Topic: Tests fail


view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 20:30):

#3009 fails tests after running for 1h but doesn't tell which test failed.

view this post on Zulip Bryan Gin-ge Chen (Jun 09 2020 at 20:31):

The raw log suggests maybe a github actions glitch:

2020-06-09T17:28:40.2021012Z ##[section]Starting: Request a runner to run this job
2020-06-09T17:28:40.4093459Z Can't find any online and idle self-hosted runner in current repository that matches the required labels: 'ubuntu-latest'
2020-06-09T17:28:40.4093511Z Can't find any online and idle self-hosted runner in current repository's account/organization that matches the required labels: 'ubuntu-latest'
2020-06-09T17:28:40.4093540Z Found online and idle hosted runner in current repository's account/organization that matches the required labels: 'ubuntu-latest'
2020-06-09T17:28:40.5977166Z ##[section]Finishing: Request a runner to run this job

view this post on Zulip Bryan Gin-ge Chen (Jun 09 2020 at 20:32):

Wait, maybe not. I guess the raw log is missing even the successful steps.

view this post on Zulip Bryan Gin-ge Chen (Jun 09 2020 at 20:43):

OK, I ran the test locally and also got a freeze. I put on-T100000 and got timeouts:

/mathlib/test/library_search/ring_theory.lean:19:3: error: (deterministic) timeout
/mathlib/test/library_search/ring_theory.lean:18:0: error: (deterministic) timeout

view this post on Zulip Bryan Gin-ge Chen (Jun 09 2020 at 20:44):

(By freeze I just mean that I got bored of waiting after 5+ mins of my laptop heating up).

view this post on Zulip Bryan Gin-ge Chen (Jun 09 2020 at 20:45):

Note that the tests succeeded for me with -T100000 in about 1-2 mins on master.

view this post on Zulip Bryan Gin-ge Chen (Jun 09 2020 at 20:45):

Maybe we should add -T100000 to the test build step too?

view this post on Zulip Yury G. Kudryashov (Jun 09 2020 at 20:47):

I don't know how to fix this, so probably I'll drop most of this PR.

view this post on Zulip Sebastien Gouezel (Jun 09 2020 at 21:17):

A failure of library_search doesn't necessarily indicate that there is a problem with your PR: maybe you have changed the type of something, and now there are much more lemmas that could apply, and library_search has to try all of them and takes a crazy amount of time to do this. If the build time doesn't increase, I wouldn't be worried.

view this post on Zulip Sebastien Gouezel (Jun 09 2020 at 21:18):

Maybe this is unveiling something weird with library_search. @Scott Morrison , what do you think?

view this post on Zulip Scott Morrison (Jun 10 2020 at 01:57):

Curious! set_option trace.suggest true allows one to see the list of lemmas that library_search thinks may be relevant. On master it finds 1394 lemmas, and succeeds, for the test

example {m n : } (H : m  n) : I.leading_coeff_nth m  I.leading_coeff_nth n :=
by library_search -- exact ideal.leading_coeff_nth_mono I H

while on Yury's branch it finds fewer, 1317, but nevertheless takes longer and fails with a timeout!

view this post on Zulip Scott Morrison (Jun 10 2020 at 01:58):

My guess is that typeclass search became more expensive on Yury's branch, but I'll check the differences between the two sets of lemmas as well.

view this post on Zulip Scott Morrison (Jun 10 2020 at 02:06):

Hrm, on master the 1394 are a strict superset of the lemmas it finds on the branch.

view this post on Zulip Scott Morrison (Jun 10 2020 at 02:08):

This does make me wonder --- if there a way for me to "save the instance cache", from one failed lemma application to the next? At the moment when library_search tries multiple lemmas, it backtracks the tactic_state after each failed unification of a lemma with the goal. Presumably this discards any work that was done trying to construct instances.

view this post on Zulip Scott Morrison (Jun 10 2020 at 02:08):

I wonder if there's any way to save this work instead, for subsequent lemma applications.

view this post on Zulip Sebastien Gouezel (Jun 10 2020 at 13:14):

I would vote for merging and dropping the test. I mean, I don't expect library_search to succeed on complicated examples like that where there is a lot of typeclass inference under the hood. Thoughts, anyone?

view this post on Zulip Scott Morrison (Jun 10 2020 at 13:29):

Sorry, I got distracted from diagnosing the change here, to orthogonal work on library_search.

view this post on Zulip Scott Morrison (Jun 10 2020 at 13:30):

I'm a bit worried that this test taking dramatically longer is a sign of a problem, and would like to compare the size of the output in trace class_instances true for both master and the branch.

view this post on Zulip Scott Morrison (Jun 10 2020 at 13:30):

It's late here however, so not tonight. I certainly won't object if Yury just removes that test and we merge. If I find anything later I'll report on it.

view this post on Zulip Sebastien Gouezel (Jun 10 2020 at 14:19):

Scott Morrison said:

This does make me wonder --- if there a way for me to "save the instance cache", from one failed lemma application to the next? At the moment when library_search tries multiple lemmas, it backtracks the tactic_state after each failed unification of a lemma with the goal. Presumably this discards any work that was done trying to construct instances.

I wonder if there's any way to save this work instead, for subsequent lemma applications.

I hope that simp does this, because it also tries to apply a bunch of lemmas in a given context. Maybe it's hidden deep in C++ code, though?

view this post on Zulip Scott Morrison (Jun 12 2020 at 03:52):

Happily #3038 makes this test fast again, so I've restored it there.

view this post on Zulip Rob Lewis (Jul 20 2020 at 13:05):

Was there any follow-up to this? Turns out #3009 caused some fairly severe type class slowdowns on @Johan Commelin 's witt vector branch. I'm trying to diagnose now.

view this post on Zulip Rob Lewis (Jul 20 2020 at 13:09):

Let me rephrase that, it's caused severe slowdowns; I'm no longer sure they're type class related.


Last updated: May 13 2021 at 06:15 UTC