Tests fail

Stream: general

[Yury G. Kudryashov]

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

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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

[Sebastien Gouezel]

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]

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

[Scott Morrison]

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]

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]

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]

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

[Rob Lewis]

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]

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