Zulip Chat Archive

Stream: general

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


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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 17:26):

Thanks to @Reid Barton for the implementation.

view this post on Zulip Eric Wieser (Oct 27 2020 at 17:28):

Would not_the_a_bug be any better or worse a name than ?

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 17:29):

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 17:30):

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

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

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 17:31):

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 17:31):

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

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

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 17:34):

There is a PR underway

view this post on Zulip Johan Commelin (Oct 27 2020 at 17:35):

Ah, Gabriel linked to it in OP: #4802

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

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

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

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

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

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

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

view this post on Zulip Eric Wieser (Oct 27 2020 at 17:51):

Were those named a before?

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

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

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

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 17:53):

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

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 17:53):

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 17:54):

This weird unicode alpha will encourage that policy

view this post on Zulip Eric Wieser (Oct 27 2020 at 17:58):

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

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

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

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

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 18:03):

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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 18:03):

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

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 18:03):

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

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

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

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 18:04):

it already does that

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 18:05):

Then why do we have a bug?

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

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

view this post on Zulip Reid Barton (Oct 27 2020 at 18:08):

Right, this is exactly the issue

view this post on Zulip Kevin Buzzard (Oct 27 2020 at 18:09):

TIL \all works for \forall

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 18:12):

that's what induction does, basically

view this post on Zulip Mario Carneiro (Oct 27 2020 at 18:12):

alternatively, we could have an rcases pattern style name list

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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 18:17):

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 18:21):

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

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 18:21):

these are the pretty printed names

view this post on Zulip Mario Carneiro (Oct 27 2020 at 18:22):

the unique name is already that

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

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

view this post on Zulip Reid Barton (Oct 27 2020 at 18:24):

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

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

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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 18:25):

Should we add a style linter that forbids ᾰ?

view this post on Zulip Kevin Lacker (Oct 27 2020 at 18:26):

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:28):

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

view this post on Zulip Kevin Lacker (Oct 27 2020 at 18:30):

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:31):

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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 18:32):

Not too hard.

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:33):

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

view this post on Zulip Reid Barton (Oct 27 2020 at 18:33):

I wonder what would happen if we used _

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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 18:34):

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:36):

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:37):

Actually no.

view this post on Zulip Kevin Lacker (Oct 27 2020 at 18:37):

<wrong comment removed>

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

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

view this post on Zulip 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 «_»

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:38):

The search on zulip will point you to this thread

view this post on Zulip Reid Barton (Oct 27 2020 at 18:39):

that might still be too confusing though...

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

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

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 18:43):

And it is easy to lint against.

view this post on Zulip Bryan Gin-ge Chen (Oct 27 2020 at 18:43):

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

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

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

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 19:00):

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 19:03):

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 19:04):

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

view this post on Zulip Johan Commelin (Oct 27 2020 at 19:47):

I guess we can do that

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:00):

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

view this post on Zulip Johan Commelin (Oct 28 2020 at 09:00):

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

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

view this post on Zulip Gabriel Ebner (Oct 28 2020 at 10:28):

lean#493

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

view this post on Zulip Anne Baanen (Oct 28 2020 at 10:57):

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Gabriel Ebner (Oct 29 2020 at 09:23):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 09:25):

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

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

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

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 12:22):

It looks like it simply hangs

view this post on Zulip Johan Commelin (Oct 29 2020 at 12:24):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 12:25):

So it doesn't hang completely

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

view this post on Zulip Gabriel Ebner (Oct 29 2020 at 12:31):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 12:31):

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

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

view this post on Zulip Gabriel Ebner (Oct 29 2020 at 12:32):

Can you try rm **/*.olean?

view this post on Zulip Johan Commelin (Oct 29 2020 at 12:33):

Ooh, that seems to have done it

view this post on Zulip Johan Commelin (Oct 29 2020 at 12:33):

Does that mean the cache is poisened?

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 13:06):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 13:16):

@Gabriel Ebner Now it's hanging on

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 13:16):

(For the second time in a row)

view this post on Zulip Johan Commelin (Oct 29 2020 at 13:19):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 13:44):

src/ring_theory/witt_vector compiles

view this post on Zulip Johan Commelin (Oct 29 2020 at 13:56):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:01):

Ok, it compiles (-;

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:02):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:11):

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

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:18):

Snap... your machine is faster...

view this post on Zulip Bhavik Mehta (Oct 29 2020 at 14:18):

I think I started before you :)

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:18):

Mine is also just done

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:18):

Aah, ok

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:18):

lean --make src/data

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:27):

lean --make src/algebra

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:28):

lean --make src/computability/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:36):

lean --make src/control/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:39):

lean --make src/combinatorics/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:41):

lean --make src/field_theory/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:42):

lean --make src/geometry/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:51):

lean --make src/number_theory/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:53):

lean --make src/representation_theory/

view this post on Zulip Johan Commelin (Oct 29 2020 at 14:54):

lean --make src/topology/

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:03):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:04):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:04):

Working on lean --make src/group_theory/

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:09):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:12):

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

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:12):

lean --make src/order/

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:13):

lean --make src/set_theory

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:14):

lean --make src/tactic/

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:16):

There's a whole bunch of tests failing.

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:17):

src/ is now building without errors

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:30):

Aha, those expected outputs are not so bad

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:30):

Fixed them

view this post on Zulip Johan Commelin (Oct 29 2020 at 15:33):

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


Last updated: May 10 2021 at 00:31 UTC