Zulip Chat Archive

Stream: general

Topic: Replacing the `a` bug by the `ᾰ` bug


Gabriel Ebner (Oct 27 2020 at 17:26):

@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 (Oct 27 2020 at 17:26):

Thanks to @Reid Barton for the implementation.

Eric Wieser (Oct 27 2020 at 17:28):

Would not_the_a_bug be any better or worse a name than ?

Eric Wieser (Oct 27 2020 at 17:29):

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

Mario Carneiro (Oct 27 2020 at 17:29):

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

Johan Commelin (Oct 27 2020 at 17:30):

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

Johan Commelin (Oct 27 2020 at 17:30):

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

Johan Commelin (Oct 27 2020 at 17:31):

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

Johan Commelin (Oct 27 2020 at 17:31):

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

Mario Carneiro (Oct 27 2020 at 17:31):

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

Mario Carneiro (Oct 27 2020 at 17:32):

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 (Oct 27 2020 at 17:34):

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 (Oct 27 2020 at 17:34):

There is a PR underway

Johan Commelin (Oct 27 2020 at 17:35):

Ah, Gabriel linked to it in OP: #4802

Mario Carneiro (Oct 27 2020 at 17:37):

-     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 (Oct 27 2020 at 17:37):

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 (Oct 27 2020 at 17:38):

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 (Oct 27 2020 at 17:39):

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

Reid Barton (Oct 27 2020 at 17:40):

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 (Oct 27 2020 at 17:47):

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 (Oct 27 2020 at 17:50):

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 (Oct 27 2020 at 17:51):

Were those named a before?

Gabriel Ebner (Oct 27 2020 at 17:51):

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 (Oct 27 2020 at 17:52):

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

Yury G. Kudryashov (Oct 27 2020 at 17:53):

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

Yury G. Kudryashov (Oct 27 2020 at 17:53):

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

Yury G. Kudryashov (Oct 27 2020 at 17:53):

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

Johan Commelin (Oct 27 2020 at 17:54):

This weird unicode alpha will encourage that policy

Eric Wieser (Oct 27 2020 at 17:58):

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

Kevin Buzzard (Oct 27 2020 at 17:58):

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 (Oct 27 2020 at 18:02):

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 (Oct 27 2020 at 18:03):

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 (Oct 27 2020 at 18:03):

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

Gabriel Ebner (Oct 27 2020 at 18:03):

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

Yury G. Kudryashov (Oct 27 2020 at 18:03):

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

Mario Carneiro (Oct 27 2020 at 18:03):

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 (Oct 27 2020 at 18:04):

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

Yury G. Kudryashov (Oct 27 2020 at 18:04):

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

Mario Carneiro (Oct 27 2020 at 18:04):

it already does that

Yury G. Kudryashov (Oct 27 2020 at 18:05):

Then why do we have a bug?

Mario Carneiro (Oct 27 2020 at 18:06):

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

Mario Carneiro (Oct 27 2020 at 18:08):

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 (Oct 27 2020 at 18:08):

Right, this is exactly the issue

Kevin Buzzard (Oct 27 2020 at 18:09):

TIL \all works for \forall

Mario Carneiro (Oct 27 2020 at 18:12):

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 (Oct 27 2020 at 18:12):

that's what induction does, basically

Mario Carneiro (Oct 27 2020 at 18:12):

alternatively, we could have an rcases pattern style name list

Alex Peattie (Oct 27 2020 at 18:16):

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 (Oct 27 2020 at 18:17):

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

Mario Carneiro (Oct 27 2020 at 18:21):

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

Kevin Lacker (Oct 27 2020 at 18:21):

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 (Oct 27 2020 at 18:21):

these are the pretty printed names

Mario Carneiro (Oct 27 2020 at 18:22):

the unique name is already that

Reid Barton (Oct 27 2020 at 18:22):

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 (Oct 27 2020 at 18:23):

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

Reid Barton (Oct 27 2020 at 18:24):

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

Kevin Lacker (Oct 27 2020 at 18:24):

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 (Oct 27 2020 at 18:25):

"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 (Oct 27 2020 at 18:25):

Should we add a style linter that forbids ᾰ?

Kevin Lacker (Oct 27 2020 at 18:26):

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

Johan Commelin (Oct 27 2020 at 18:28):

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

Kevin Lacker (Oct 27 2020 at 18:30):

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

Johan Commelin (Oct 27 2020 at 18:31):

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

Gabriel Ebner (Oct 27 2020 at 18:32):

Not too hard.

Johan Commelin (Oct 27 2020 at 18:33):

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

Reid Barton (Oct 27 2020 at 18:33):

I wonder what would happen if we used _

Gabriel Ebner (Oct 27 2020 at 18:33):

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

Gabriel Ebner (Oct 27 2020 at 18:34):

Reid Barton (Oct 27 2020 at 18:35):

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 (Oct 27 2020 at 18:36):

Johan Commelin (Oct 27 2020 at 18:37):

Actually no.

Kevin Lacker (Oct 27 2020 at 18:37):

<wrong comment removed>

Johan Commelin (Oct 27 2020 at 18:37):

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

Johan Commelin (Oct 27 2020 at 18:38):

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 (Oct 27 2020 at 18:38):

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

Johan Commelin (Oct 27 2020 at 18:38):

The search on zulip will point you to this thread

Reid Barton (Oct 27 2020 at 18:39):

that might still be too confusing though...

Kevin Lacker (Oct 27 2020 at 18:40):

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 (Oct 27 2020 at 18:41):

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

Johan Commelin (Oct 27 2020 at 18:42):

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 (Oct 27 2020 at 18:43):

And it is easy to lint against.

Bryan Gin-ge Chen (Oct 27 2020 at 18:43):

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

Bryan Gin-ge Chen (Oct 27 2020 at 18:44):

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

Mario Carneiro (Oct 27 2020 at 18:58):

Gabriel Ebner said:

Should we add a style linter that forbids ᾰ?

How would we nolint a style linter?

Gabriel Ebner (Oct 27 2020 at 19:00):

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

Mario Carneiro (Oct 27 2020 at 19:03):

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

Mario Carneiro (Oct 27 2020 at 19:04):

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

Johan Commelin (Oct 27 2020 at 19:47):

I guess we can do that

Johan Commelin (Oct 28 2020 at 09:00):

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

Johan Commelin (Oct 28 2020 at 09:00):

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

Gabriel Ebner (Oct 28 2020 at 09:29):

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

Gabriel Ebner (Oct 28 2020 at 10:28):

lean#493

Gabriel Ebner (Oct 28 2020 at 10:36):

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 (Oct 28 2020 at 10:57):

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

Johan Commelin (Oct 29 2020 at 07:01):

@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 (Oct 29 2020 at 07:01):

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

Gabriel Ebner (Oct 29 2020 at 08:53):

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 (Oct 29 2020 at 08:54):

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 (Oct 29 2020 at 08:55):

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

Gabriel Ebner (Oct 29 2020 at 09:07):

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 (Oct 29 2020 at 09:08):

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 (Oct 29 2020 at 09:10):

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 (Oct 29 2020 at 09:21):

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 (Oct 29 2020 at 09:23):

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 (Oct 29 2020 at 09:23):

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

Johan Commelin (Oct 29 2020 at 09:25):

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

Kevin Buzzard (Oct 29 2020 at 09:47):

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 (Oct 29 2020 at 12:22):

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

Johan Commelin (Oct 29 2020 at 12:22):

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

Johan Commelin (Oct 29 2020 at 12:22):

It looks like it simply hangs

Johan Commelin (Oct 29 2020 at 12:24):

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

Johan Commelin (Oct 29 2020 at 12:25):

So it doesn't hang completely

Johan Commelin (Oct 29 2020 at 12:25):

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

Gabriel Ebner (Oct 29 2020 at 12:31):

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

Johan Commelin (Oct 29 2020 at 12:31):

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

Johan Commelin (Oct 29 2020 at 12:31):

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 (Oct 29 2020 at 12:32):

Can you try rm **/*.olean?

Johan Commelin (Oct 29 2020 at 12:33):

Ooh, that seems to have done it

Johan Commelin (Oct 29 2020 at 12:33):

Does that mean the cache is poisened?

Gabriel Ebner (Oct 29 2020 at 13:05):

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

Johan Commelin (Oct 29 2020 at 13:06):

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

Johan Commelin (Oct 29 2020 at 13:16):

@Gabriel Ebner Now it's hanging on

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

Johan Commelin (Oct 29 2020 at 13:16):

(For the second time in a row)

Johan Commelin (Oct 29 2020 at 13:19):

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

Johan Commelin (Oct 29 2020 at 13:44):

src/ring_theory/witt_vector compiles

Johan Commelin (Oct 29 2020 at 13:56):

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

Johan Commelin (Oct 29 2020 at 14:01):

Ok, it compiles (-;

Johan Commelin (Oct 29 2020 at 14:02):

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

Johan Commelin (Oct 29 2020 at 14:11):

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

Bhavik Mehta (Oct 29 2020 at 14:17):

Johan Commelin said:

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

This works for me!

Johan Commelin (Oct 29 2020 at 14:18):

Snap... your machine is faster...

Bhavik Mehta (Oct 29 2020 at 14:18):

I think I started before you :)

Johan Commelin (Oct 29 2020 at 14:18):

Mine is also just done

Johan Commelin (Oct 29 2020 at 14:18):

Aah, ok

Johan Commelin (Oct 29 2020 at 14:18):

lean --make src/data

Johan Commelin (Oct 29 2020 at 14:27):

lean --make src/algebra

Johan Commelin (Oct 29 2020 at 14:28):

lean --make src/computability/

Johan Commelin (Oct 29 2020 at 14:36):

lean --make src/control/

Johan Commelin (Oct 29 2020 at 14:39):

lean --make src/combinatorics/

Johan Commelin (Oct 29 2020 at 14:41):

lean --make src/field_theory/

Johan Commelin (Oct 29 2020 at 14:42):

lean --make src/geometry/

Johan Commelin (Oct 29 2020 at 14:51):

lean --make src/number_theory/

Johan Commelin (Oct 29 2020 at 14:53):

lean --make src/representation_theory/

Johan Commelin (Oct 29 2020 at 14:54):

lean --make src/topology/

Johan Commelin (Oct 29 2020 at 15:03):

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

Johan Commelin (Oct 29 2020 at 15:04):

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

Johan Commelin (Oct 29 2020 at 15:04):

Working on lean --make src/group_theory/

Johan Commelin (Oct 29 2020 at 15:09):

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

Johan Commelin (Oct 29 2020 at 15:12):

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

Johan Commelin (Oct 29 2020 at 15:12):

lean --make src/order/

Johan Commelin (Oct 29 2020 at 15:13):

lean --make src/set_theory

Johan Commelin (Oct 29 2020 at 15:14):

lean --make src/tactic/

Johan Commelin (Oct 29 2020 at 15:16):

There's a whole bunch of tests failing.

Johan Commelin (Oct 29 2020 at 15:17):

src/ is now building without errors

Johan Commelin (Oct 29 2020 at 15:30):

Aha, those expected outputs are not so bad

Johan Commelin (Oct 29 2020 at 15:30):

Fixed them

Johan Commelin (Oct 29 2020 at 15:33):

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


Last updated: Dec 20 2023 at 11:08 UTC