library_search in 3.16.5

Stream: general

[Dan Stanescu]

I just did leanproject up to 3.16.5 and neither library_search nor suggest work any more. Maybe I missed an announcement, is this supposed to happen?

[Alex J. Best]

I think some imports were moved around, try adding import tactic.basic to the top of your files.

[Dan Stanescu]

Thank you, that was it!

[Alex J. Best]

Previously a lot of files imported tactics by default, so you often got tactics for free by importing any random file without explicitly importing them yourself, now there was a bit of cleanup.

[Dan Stanescu]

I had import tactic but that was not enough.

[Bryan Gin-ge Chen]

That's very strange. import tactic should import strictly more than import tactic.basic.

[Dan Stanescu]

That is what I thought too, but I can totally confirm that was my experience. I tried four times, recreating the directory from scratch. I was very surprised.

[Dan Stanescu]

I did have the same kind of experience some time ago when trying to use tactic.explode. It didn't work when only importing tactic, but it did work when explicitly importing tactic.explode.

[Dan Stanescu]

But that had changed in the meantime.

[Bryan Gin-ge Chen]

OK, I just opened #3284 to fix this.

[Bryan Gin-ge Chen]

Thanks for the report!