Replacing the `a` bug by the `ᾰ` bug

Stream: general

[Gabriel Ebner]

@Johan Commelin has suggested to replace the infamous a bug by the similar, but hopefully less common, ᾰ bug.
#4802, lean#490, lean#437
I'd like to finally close this issue. Any opinions?

[Gabriel Ebner]

Thanks to @Reid Barton for the implementation.

[Eric Wieser]

Would not_the_a_bug be any better or worse a name than ᾰ?

[Eric Wieser]

seeing ᾰ appear in the tactic state is probably harder for a new user to look up than not_the_a_bug

[Mario Carneiro]

The point is that no one will accidentally use ᾰ, while accidental use of a is common

[Johan Commelin]

And Mario pointed out that we still want to support autogenerated names

[Johan Commelin]

They are all over the place in your tactic state. You just don't want them to appear explicitly in proof scripts.

[Johan Commelin]

But having not_the_a_bug in 10 different places in your tactic state would be visually annoying

[Johan Commelin]

(Before the weird unicode alpha, I had suggested xyzzy, deadbeaf, and fixme.)

[Mario Carneiro]

We should probably add documentation for this somewhere, because it's really weird

[Mario Carneiro]

I don't have any idea where to put the docs though except perhaps on the source line that introduces the binder name

[Kevin Buzzard]

I am also very keen to close this issue. It still trips people up. But my understanding is that it will be hard to fix mathlib -- is this correct?

[Johan Commelin]

There is a PR underway

[Johan Commelin]

Ah, Gabriel linked to it in OP: #4802

[Mario Carneiro]

-     by_contradiction,
-     have := min_fac_prime a,
+     by_contradiction hn,
+     have := min_fac_prime hn,

Can we have by_contradiction name its hypothesis h by default?

[Kevin Buzzard]

Right, and it fails after 2 minutes. How problematic is the change for mathlib? I thought Reid was saying that it would be an absolute pain.

[Jannis Limperg]

Does this change the name Lean uses to elaborate function arrows in general? If so, then name.is_likely_generated_binder_name, name.is_likely_generated_binder_simple_name and the associated library note in mathlib's meta.expr need to be updated to match.

[Reid Barton]

I think fixing mathlib will merely be annoying if you give yourself the option to just use ᾰ when things look bleak otherwise.

[Reid Barton]

oh I didn't think of using the ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨h_a, h_x⟩› syntax, that could help too

[Reid Barton]

but you can see at https://github.com/leanprover-community/mathlib/pull/4802/files#diff-bd5a0541cce36467731f8b5c749edac7f2dea9835cbdbe17ec5b1b1b2b5fe89cL349 that things went a bit off track, in that an apply became a simp *

[Gabriel Ebner]

TBH, the instance naming change is more painful than the ᾰ. Stuff that should work but doesn't:

• instance : functor (set : Type → Type)
• instance (F : C ⇒ D) : faithful F.op

[Eric Wieser]

Were those named a before?

[Gabriel Ebner]

Mario Carneiro said:

-     by_contradiction,
-     have := min_fac_prime a,
+     by_contradiction hn,
+     have := min_fac_prime hn,

Can we have by_contradiction name its hypothesis h by default?

Yeah, by_contradiction should also use choice. PRs welcome. lean#433 But I'm not sure h is really an improvement over ᾰ.

[Gabriel Ebner]

The instances were called functor and faithful before (in whatever namespace you happened to be at the moment).

[Yury G. Kudryashov]

Can we ensure that these tactics do not reuse an existing name instead of using weird unicode?

[Yury G. Kudryashov]

It would be nice to have a policy "name your variables" too.

[Yury G. Kudryashov]

(if you're going to use them by name)

[Johan Commelin]

This weird unicode alpha will encourage that policy

[Eric Wieser]

An explicit "don't do this character" like 🚫 might be even more effective...

[Kevin Buzzard]

Of course, "name your variables" is easier said than done for tactics like split_ifs, which can sometimes generate a whole bunch of cases.

[Johan Commelin]

Eric Wieser said:

An explicit "don't do this character" like 🚫 might be even more effective...

But I think this is not a legal identifier... So then you need french quotes around it.

[Mario Carneiro]

Yeah, by_contradiction should also use choice. PRs welcome. lean#433 But I'm not sure h is really an improvement over ᾰ.

The difference is that it's a user tactic. ᾰ isn't supposed to be the canonical autogenerated name, only the one that is used in pi binders in tactics

[Yury G. Kudryashov]

It's "name your variables or don't refer to them by names"

[Gabriel Ebner]

What should intro do on ⊢ ∀ x : ᾰ, x = x?

[Yury G. Kudryashov]

E.g., you can use \f<type\f>

[Mario Carneiro]

have has a documented default name this, by_cases has a documented default name h, by_contradiction should also have a documented default name (perhaps h or hn)

[Mario Carneiro]

I think intro should introduce the variable in the binder, so that's one way to get a ᾰ variable

[Yury G. Kudryashov]

Can it use default_name_1 if there is a variable named default_name in the context?

[Mario Carneiro]

it already does that

[Yury G. Kudryashov]

Then why do we have a bug?

[Mario Carneiro]

because if you write have : \all a : nat, 0 < 1 -> a < a, a will have type 0 < 1

[Mario Carneiro]

I'm not sure exactly when the decision is made on what to name the 0 < 1 binder there. If it is at parse time (making a pexpr) then we don't have the context so we don't know what to avoid

[Reid Barton]

Right, this is exactly the issue

[Kevin Buzzard]

TIL \all works for \forall

[Mario Carneiro]

Kevin Buzzard said:

Of course, "name your variables" is easier said than done for tactics like split_ifs, which can sometimes generate a whole bunch of cases.

The catchall solution for such tactics is to give them an unstructured name list to pull from whenever they need a name

[Mario Carneiro]

that's what induction does, basically

[Mario Carneiro]

alternatively, we could have an rcases pattern style name list

[Alex Peattie]

Eric Wieser said:

seeing ᾰ appear in the tactic state is probably harder for a new user to look up than not_the_a_bug

From a totally naive POV, I agree that something more searchable than ᾰ would be good... I think xyzzy could be a good choice because it's clear that it's a "magic value" from its usage elsewhere, without being something that people are likely to accidentally pick. Or maybe even something like _unnamed?

[Gabriel Ebner]

Zulip search works just fine: https://leanprover.zulipchat.com/#narrow/search/.E1.BE.B0

[Mario Carneiro]

Probably not now, but a possible future option could be a way to set this

[Kevin Lacker]

if you want to prevent people from using the name generated, just have it generate a different name every time. a<random number>

[Mario Carneiro]

these are the pretty printed names

[Mario Carneiro]

the unique name is already that

[Reid Barton]

Whatever name we choose will also show up in the proof state, even for "finished" proofs, and perhaps also in the types of hypotheses

[Mario Carneiro]

I don't want to be staring at a state trying to distinguish a23425.34 from a94674.1

[Reid Barton]

maybe don't use structures with 34 fields then :upside_down:

[Kevin Lacker]

ok. it sounds like you do occasionally want to use this name then. i suggest "gen1", "gen2" etc like a lisp gensym. unicode-junk and nonsense like "xyzzy" will end up being annoying in the end

[Kevin Lacker]

"gen" also hints at "generated" so it's a small clue what it is, and "gen1" is nowhere used in mathlib right now

[Gabriel Ebner]

Should we add a style linter that forbids ᾰ?

[Kevin Lacker]

is that going to show up in the types of hypotheses?

[Johan Commelin]

@Kevin Lacker I think Gabriel means that git grep "ᾰ" should return nothing.

[Kevin Lacker]

oh i get it. in that case yeah a style linter

[Johan Commelin]

@Gabriel Ebner How hard is it to make 🚫 a legal identifier?

[Gabriel Ebner]

Not too hard.

[Johan Commelin]

Then that might be even better than this weird alpha, right?

[Reid Barton]

I wonder what would happen if we used _

[Gabriel Ebner]

You can't search for the emoji on zulip: https://leanprover.zulipchat.com/#narrow/search/.F0.9F.9A.AB

[Gabriel Ebner]

⃠

[Reid Barton]

we could probably carve out an exception for _ for whatever is causing _x to break, since nobody is going to name a structure field the empty string anyways

[Johan Commelin]

…

[Johan Commelin]

Actually no.

[Kevin Lacker]

<wrong comment removed>

[Johan Commelin]

I would love to reserve … for "don't try type class inference on this variable, but make it into a goal".

[Johan Commelin]

Kevin Lacker said:

if git grep "ᾰ" returns nothing, then searching on zulip won't yield anything either, even if the search does work

What do you mean? The linter should raise an error if git grep "crazy-alpha" returns something.

[Reid Barton]

interestingly the pretty-printer displays the identifier _ as _, even though you can't actually write _ to refer to «_»

[Johan Commelin]

The search on zulip will point you to this thread

[Reid Barton]

that might still be too confusing though...

[Kevin Lacker]

why not name it something long, just to discourage people from writing it. there's no need for it to be super short if it isn't part of a proof. like autogenerated_variable_1

[Reid Barton]

You will see it in the proof state often, and a long name will make whatever it appears in hard to read

[Johan Commelin]

Kevin Lacker said:

why not name it something long, just to discourage people from writing it. there's no need for it to be super short if it isn't part of a proof. like autogenerated_variable_1

Crazy alpha will also discourage people from writing it.

[Johan Commelin]

And it is easy to lint against.

[Bryan Gin-ge Chen]

We definitely do need to document this somewhere that's easy to find though.

[Bryan Gin-ge Chen]

Maybe we could hack the widget tactic state to display a friendly pop-up or something.

[Mario Carneiro]

Gabriel Ebner said:

Should we add a style linter that forbids ᾰ?

How would we nolint a style linter?

[Gabriel Ebner]

Adding a line in copy-mod-doc-exceptions.txt is currently the only supported way.

[Mario Carneiro]

It shouldn't be too hard to grep for @[nolint autogenerated_names]

[Mario Carneiro]

maybe with some rule like "the nolint extends until the next double newline"

[Johan Commelin]

I guess we can do that

[Johan Commelin]

@Gabriel Ebner Can we crowdsource the work for #4802 ?

[Johan Commelin]

There are two issues, right? The instance names and the a-bug?

[Gabriel Ebner]

I'll now look at improving the instance naming heuristic, this should hopefully cut the work in half.

[Gabriel Ebner]

lean#493

[Gabriel Ebner]

Are there any objections against merging lean#490? Since ᾰ intentionally doesn't appear in mathlib, we can repaint this bikeshed later if we want to.

[Anne Baanen]

I'm OK with the result of both changes. Haven't studied their implementation closely though.

[Johan Commelin]

@Gabriel Ebner I fear that it will take a lot of work to get rid of all autogenerated variables. Maybe this is a crazy dream, but would it be possible to ask Lean to modify the source code and use ᾰ when it hits an error?

[Johan Commelin]

I guess this is made more difficult by the fact that we also have the instance names changing independently.

[Gabriel Ebner]

Johan Commelin said:

Gabriel Ebner I fear that it will take a lot of work to get rid of all autogenerated variables. Maybe this is a crazy dream, but would it be possible to ask Lean to modify the source code and use ᾰ when it hits an error?

I'm not sure what change you expect Lean to do. Neither ᾰ nor a should be used in the source code. So there needs to be more than just superficial changes.

[Johan Commelin]

Can't we remove the ᾰ incrementally? When we introduced the docstring linter, that PR also didn't add docstrings to every def in mathlib.

[Johan Commelin]

Even though your effort is very noble, I feel like it will take you 2 months to fix all of mathlib.

[Gabriel Ebner]

On the contrary, I feel like I'm making progress. It's pretty mindless so I'm mostly limited by how fast I get back errors from CI.

[Gabriel Ebner]

If this is the attitude we have for the Lean 4 migration, then we can rebrand the "community edition" as "eternal mathlib edition".

[Johan Commelin]

Well, it there are 500 crazy alphas in mathlib, then we can crowdsource a sprint to get rid of them. Now I feel like it's harder to parallelize the work.

[Kevin Buzzard]

I am prepared to put in some hours to get rid of the a bug, for sure. I don't understand how to embark on this at this point but I'm sure this can be explained to me

[Kevin Buzzard]

When I last embarked upon a major mathlib refactor (with Scott, removing some deprecated import) I would fix a file and then compile locally, it seemed quicker than relying on CI.

[Gabriel Ebner]

Ok, I'll leave it to you then. BTW, linear algebra compiles now.

[Johan Commelin]

Ooh wow, then it's maybe going faster than I expected. Sorry for the misunderstanding.

[Kevin Buzzard]

How can I help? My course finishes tomorrow so the amount of time I have for Lean will creep up a little more

[Johan Commelin]

I'm trying to build this locally with 3.23.0, but lean isn't showing any output.

[Johan Commelin]

Also, I don't see it in top, whereas usually it would eat up all available CPU

[Johan Commelin]

It looks like it simply hangs

[Johan Commelin]

$ lean --version
Lean (version 3.23.0, commit ed6accfb611b, Release)

[Johan Commelin]

So it doesn't hang completely

[Johan Commelin]

But if I run lean --make src/ there is no output at all, even after several minutes.

[Gabriel Ebner]

It works here and it works on CI. Could you maybe try again?

[Johan Commelin]

Yes, I did. It also doesn't work in VScode

[Johan Commelin]

First I thought that I should maybe update elan. But as you can see above, I do have the correct version of Lean

[Gabriel Ebner]

Can you try rm **/*.olean?

[Johan Commelin]

Ooh, that seems to have done it

[Johan Commelin]

Does that mean the cache is poisened?

[Gabriel Ebner]

This shouldn't happen actually. The import code checks that the olean file comes from the same lean version.

[Johan Commelin]

I had even run leanproject get-mathlib-cache (after CI had finished its mathlib build)

[Johan Commelin]

@Gabriel Ebner Now it's hanging on

mathlib_a/src/order/bounded_lattice.lean: saving olean

[Johan Commelin]

(For the second time in a row)

[Johan Commelin]

Aha, apparently there was an olean.lock file blocking it

[Johan Commelin]

src/ring_theory/witt_vector compiles

[Johan Commelin]

I will try to fix ring_theory/* and whatever else I meet on my way there

[Johan Commelin]

Ok, it compiles (-;

[Johan Commelin]

Now I'll try lean --make src/algebraic_geometry/

[Johan Commelin]

Done. Now I'm trying lean --make src/category_theory/

[Bhavik Mehta]

Johan Commelin said:

Done. Now I'm trying lean --make src/category_theory/

This works for me!

[Johan Commelin]

Snap... your machine is faster...

[Bhavik Mehta]

I think I started before you :)

[Johan Commelin]

Mine is also just done

[Johan Commelin]

Aah, ok

[Johan Commelin]

lean --make src/data

[Johan Commelin]

lean --make src/algebra

[Johan Commelin]

lean --make src/computability/

[Johan Commelin]

lean --make src/control/

[Johan Commelin]

lean --make src/combinatorics/

[Johan Commelin]

lean --make src/field_theory/

[Johan Commelin]

lean --make src/geometry/

[Johan Commelin]

lean --make src/number_theory/

[Johan Commelin]

lean --make src/representation_theory/

[Johan Commelin]

lean --make src/topology/

[Johan Commelin]

Stuff in src/topology/sheaves/sheaf_condition is really way too slow

[Johan Commelin]

If someone is looking for a little :racecar: :rocket: challenge, then :up:

[Johan Commelin]

Working on lean --make src/group_theory/

[Johan Commelin]

lean --make src/deprecated/
lean --make src/dynamics/
lean --make src/analysis/

[Johan Commelin]

lean --make src/measure_theory/
lean --make src/meta

[Johan Commelin]

lean --make src/order/

[Johan Commelin]

lean --make src/set_theory

[Johan Commelin]

lean --make src/tactic/

[Johan Commelin]

There's a whole bunch of tests failing.

[Johan Commelin]

src/ is now building without errors

[Johan Commelin]

Aha, those expected outputs are not so bad

[Johan Commelin]

Fixed them

[Johan Commelin]

Looks like everything builds now. Let's wait for the linter.