import refactor and library_search

Stream: general

[Patrick Massot]

Presumably since #3235, library_search randomly fails to be available in mathlib. This is really a PITA. Is there any hope to fix that?

[Johan Commelin]

I guess we should add import tactic.suggest to tactic/default.lean.

[Kevin Buzzard]

It's not just library_search, I am refactoring subgroups and #where is also often missing. I have taken to doing this:

import group_theory.coset
...
import tactic
#eval "remove this import"

[Johan Commelin]

tactic.basic contains this sort of stuff

[Johan Commelin]

default imports basic, for the record.

[Alex J. Best]

since #3284 - 5 days ago only though

[Scott Morrison]

Okay, I agree this was a mistake. I will put this on my list.

[Scott Morrison]

I'm doing some experiments, but I think this is viable:

1. import tactic.basic "as early as possible" (i.e. in any file that tactic.basic doesn't depend on, and which imports any tactic strictly between tactic.core and tactic.basic, just import tactic.basic itself
2. add both tactic.finish and tactic.tauto to tactic.basic (neither requires adding any dependencies)

[Scott Morrison]

3. we can also add norm_cast to tactic.basic for free

[Scott Morrison]

#3333