## Stream: general

### Topic: import refactor and library_search

#### Patrick Massot (Jul 08 2020 at 18:09):

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 (Jul 08 2020 at 18:11):

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

#### Kevin Buzzard (Jul 08 2020 at 18:11):

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 (Jul 08 2020 at 18:14):

tactic.basic contains this sort of stuff

#### Johan Commelin (Jul 08 2020 at 18:14):

default imports basic, for the record.

#### Alex J. Best (Jul 08 2020 at 18:25):

since #3284 - 5 days ago only though

#### Scott Morrison (Jul 09 2020 at 00:41):

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

#### Scott Morrison (Jul 09 2020 at 00:59):

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 (Jul 09 2020 at 01:04):

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

#### Scott Morrison (Jul 09 2020 at 02:20):

#3333

Last updated: May 13 2021 at 21:12 UTC