test/observe failure

Stream: mathlib4

[Ralf Stephan]

What could be the reason? There is not even a line 17 in that file.

Test failed: `lake env lean ./test/observe.lean` produced:
`library_search` stopped because it was running out of time.
You may get better results using `set_option maxHeartbeats 0`.
Error: ./test/observe.lean:17:4: error: observe did not find a solution

This is from #14286. Any ideas welcome.

[Mauricio Collares]

https://github.com/leanprover-community/mathlib4/blob/master/test%2Fobserve.lean has 21 lines

[Ralf Stephan]

Okay thanks, I confused files (there is also one in Libraysearch). Gives me an idea now.