import tactic

Stream: mathlib4

[Kevin Buzzard]

In lean 3 whenever I am teaching I start my files with import tactic. It's a great, easy to remember, useful import which gets everything I need to do logic, natural numbers, all the basic stuff. It does basic group theory, equivalence relations etc etc. It imports a really nice chunk of mathlib. It was written once and got out of date: I don't think it imported stuff like slim_check or omega and one would occasionally run into other tactics which we'd forgotten to put in there, but who cares. It worked modulo obscure edge cases and that was exactly what I needed for teaching.

Is it possible to emulate this experience in mathlib4 by me or someone else writing Mathlib/Tactic.lean which imports all of the tactic files which are there today, and who cares if it gets out of date? I'm writing basic logic files and I've just to import Mathlib.Tactic.LeftRight so I can port the or sheet! I don't want to have to put beginners through seeing that.

[Patrick Massot]

I agree we need that. I would merge a PR adding it. A couple of weeks ago there was a crazy discussion where Martin felt he needed to explain what to import in a beginner tactic cheat sheet. This shouldn't be needed. It should be import Tactic.

[Jireh Loreaux]

I'm not exactly disagreeing that having this would be nice, but I think the issue is that we want to prevent people from writing import Tactic in mathlib. Of course, we could demand that reviewers don't merge PRs with this, but I think it's hard to avoid it being abused (even unintentionally).

Kevin, as at least a temporary workaround, couldn't you just create a file in your project repo called Tactic.lean and import all the relevant pieces you want into that?

[Yaël Dillies]

The problem is that we also don't want a rogue file in no folder, and it needs to be under Mathlib. So it seems the best we can do is import Mathlib.Tactic.Basic.

[Sebastian Ullrich]

Jireh Loreaux said:

I'm not exactly disagreeing that having this would be nice, but I think the issue is that we want to prevent people from writing import Tactic in mathlib. Of course, we could demand that reviewers don't merge PRs with this, but I think it's hard to avoid it being abused (even unintentionally).

That sounds like something that could be trivially linted against inside mathlib

[Yaël Dillies]

In fact, we already did so for other imports.

[Kevin Buzzard]

import Mathlib.Tactic.Basic does not even import left and right which I typically cover in lecture 1 of an introductory lean course for undergraduates (that was what motivated me to start this thread)

[Yaël Dillies]

Oh wait, that's already a file!

[Kevin Buzzard]

It's too basic

[Kevin Buzzard]

It's what I was using instead of import tactic

[Adam Topaz]

we could put a file called Tactic.lean with the relevant imports in the Mathlib folder, and use import Mathlib.Tactic

[Adam Topaz]

does Lean4 support Default.lean files?

[Kyle Miller]

Incidentally, there's both Mathlib.Tactic.Basic and Mathlib.Tactic.Core, and I'm not sure what is supposed to go in each.

[Kyle Miller]

Could there be a comprehensive Mathlib.Tactic.All, Mathlib.AllTactics, or Mathlib.Tactics?

[Adam Topaz]

why not just Mathlib.Tactic?

[Adam Topaz]

Mathlib.Tactic.All also sounds good to me!

[Kevin Buzzard]

We have import Mathlib for "import all of mathlib" after all. That's probably also banned in mathlib.

[Patrick Massot]

Writing a linter to prevent import Tactic in mathlib should be very easy.

[Mario Carneiro]

The obvious and canonical solution to this is to port tactic -> Mathlib.Tactic just like every other file in mathlib

[Mario Carneiro]

We don't need a Default.lean file, it would just be Mathlib/Tactic.lean

[Mario Carneiro]

As for the list getting out of date, that is hopefully something that can be solved by a PR; I don't think it was really ever "curated" because it doesn't get much use inside mathlib itself so people that use it (e.g. in classes and downstream projects) need to provide input for maintenance

[Mario Carneiro]

Kevin Buzzard said:

We have import Mathlib for "import all of mathlib" after all. That's probably also banned in mathlib.

We don't even need a lint for this one, as lean itself will get angry if you do it since it is a circular reference

[Yaël Dillies]

But then are we going to end up with default files outside the folders they belong to?

[Mario Carneiro]

yes

[Yaël Dillies]

That sounds bad.

[Mario Carneiro]

:shrug:

[Kyle Miller]

How difficult would it be for Mathlib/Tactic.lean to be required to import all of Mathlib/Tactic, and (bonus) have Mathlib.lean import just Mathlib.Tactic?

[Mario Carneiro]

it would complicate the one-liner which calculates Mathlib.lean

[Mario Carneiro]

you could use a similar one-liner to calculate Mathlib.Tactic, or even calculate all "default" files (lean files with the same name as a directory)

[Mario Carneiro]

I think it would actually make import Mathlib.Tactic less useful though, since the original import tactic did not contain everything on purpose

[Mario Carneiro]

On the other hand, one of the things we have talked about re: improving precompilation is to reduce the number of entry points, in which case having a one-stop shop Mathlib.Tactic containing everything we want to compile would be a good thing, even inside mathlib

[Mario Carneiro]

Some of the tactics are more (mathematically) advanced though and this plays havoc with our dependency graph

[Yaël Dillies]

Can we change the way import works so that import x imports x.lean if it exists, or x/y.lean for all y else?

[Yaël Dillies]

That sounds like the only way to effectively have all those default files without cluttering every folder which has subfolders.

[Mario Carneiro]

To some extent this is a design decision, you don't necessarily want to require directory traversals to build things

[Mario Carneiro]

Plus, I actually have a file called Mathlib/Test.lean in which I put random crap people ask me on zulip, and I wouldn't want it to be impossible for that file to exist without getting built by lake build

[Mario Carneiro]

currently I can do this by just not putting it in Mathlib.lean and adding it to .git/info/exclude so it isn't pushed in PRs

[Kyle Miller]

I'm not sure there's really any issue regarding clutter, but one concrete problem I can think of is that it's a little inconvenient to move modules around since you have to remember to move its sibling. (Of course, if you move a module you also have to update imports everywhere too.)

[Mario Carneiro]

"build everything in the directory" might be right for a pristine copy of mathlib but it is probably less likely to be correct for many peoples' mathlib development setups, so separating the two (and checking that they agree in CI) seems like the right approach

[Mario Carneiro]

Kyle Miller said:

I'm not sure there's really any issue regarding clutter, but one concrete problem I can think of is that it's a little inconvenient to move modules around since you have to remember to move its sibling. (Of course, if you move a module you also have to update imports everywhere too.)

This could be a code assist BTW

[Scott Morrison]

I'm not sure why we are talking about default files here. There's no proposal to generally introduce default files, there's just a single file, Mathlib/Tactic.lean.

[Eric Wieser]

I think @Yaël Dillies is indirectly arguing the feature should be reintroduced; which I'm sympathetic to, but isn't really relevant to this conversation (or a good use of Lean4 dev time)

[Kevin Buzzard]

mathlib4#3263

[Scott Morrison]

My quick merge is not a vote against adding CI that enforces that it imports everything. We can still do that. :-)