Zulip Chat Archive

Stream: general

Topic: import refactor and library_search


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:11):

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

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:14):

tactic.basic contains this sort of stuff

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:14):

default imports basic, for the record.

view this post on Zulip Alex J. Best (Jul 08 2020 at 18:25):

since #3284 - 5 days ago only though

view this post on Zulip Scott Morrison (Jul 09 2020 at 00:41):

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

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Jul 09 2020 at 01:04):

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

view this post on Zulip Scott Morrison (Jul 09 2020 at 02:20):

#3333


Last updated: May 13 2021 at 21:12 UTC