Stream: general

Topic: Tests fail

Yury G. Kudryashov (Jun 09 2020 at 20:30):

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

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


Bryan Gin-ge Chen (Jun 09 2020 at 20:32):

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

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


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).

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.

Bryan Gin-ge Chen (Jun 09 2020 at 20:45):

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

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.

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.

Sebastien Gouezel (Jun 09 2020 at 21:18):

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

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!

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.

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.

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.

Scott Morrison (Jun 10 2020 at 02:08):

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

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?

Scott Morrison (Jun 10 2020 at 13:29):

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

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.

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.

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?

Scott Morrison (Jun 12 2020 at 03:52):

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

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.

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