notation names

Stream: new members

[Mike Shulman]

In Lean 3, what does the syntax

notation (name := foo)

mean? I haven't been able to find any documentation of it.

[Alex J. Best]

This is a recently added feature, for the port, so it isn't documented anywhere properly I think, see https://github.com/leanprover-community/lean/pull/754

[Mike Shulman]

Context: I wanted to define a version of negation that acts on types rather than props. This works fine in the Lean web editor:

def neg (A : Type) := A → empty
notation `¬` x := neg x

However, on some local installations (I haven't figured out what they have in common), this gives the error

invalid notation: notation already declared. Consider using 'notation (name := ...)'

which is where I learned about the existence of this syntax. On those installations, adding such an annotation to the above definition of negation does indeed fix the problem. However, on installations where the annotation isn't required (including the Lean web editor), including the annotation gives a unknown identifier error.

[Mike Shulman]

Ah, maybe the difference is that the web editor is still using Lean 3.46.0, and new installations that have Lean 3.47.0 require the annotation?

[Mike Shulman]

It's a shame if it's now impossible to write code that works in both versions.

[Mike Shulman]

Is there some other way to declare overloaded notations that would work in both 3.46 and 3.47?

[Matthew Ballard]

When I ran into this issue, I found it easier to implement an instance of the underlying notation typeclass.

[Mike Shulman]

what.

[Matthew Ballard]

This is Lean 4. Let me link to an example.

[Mike Shulman]

Will it also work in Lean 3?

[Matthew Ballard]

Eg. EmptyCollection exists to supply ∅

[Alex J. Best]

Maybe not for not it's defined as this in lean 3:

def not (a : Prop) := a → false
prefix `¬`:40 := not

[Matthew Ballard]

Is ¬ reserved this way in Lean 3?

[Alex J. Best]

Mike Shulman said:

Ah, maybe the difference is that the web editor is still using Lean 3.46.0, and new installations that have Lean 3.47.0 require the annotation?

The web editor thing certainly is annoying (iirc the issue is that it is now too big for the previous CI upload method or something).
What is your use case for the editor? I'd recommend sticking to the newest lean and using gitpod instead for a web-based play around, does that work for you?

[Matthew Ballard]

Yes. It is the upgrade in Lean 3.47.

rss-bot said:

chore(*): bump to lean 3.47.0 (mathlib#16252)

A major change is that notations now require names when they are shadowing another identical notation, even if it is a local notation. Also, because localized notations can be imported in a variety of contexts, there are some new best practices for them:

• localized notations should always have a (name := ...). Notation names are unrelated to declaration names, but the declaration name is a reasonable base for the notation name.
• localized notations should never use _ in the notation, because this gets desugared to a unique metavariable index, meaning that the notation will not be recognized as a duplicate of itself if open_locale is used when the notation is already available. Instead, you should use the hole! notation, which unfolds to _.

Another major change is that projection notation (x.foo) now always instantiates implicit arguments with metavariables, which is consistent with Lean 4. To simulate the older behavior, one can use either strict implicit arguments for the structure field (e.g. ∀ {{n}}, p n instead of ∀ {n}, p n) or, depending on specifics, writing λ _, x.foo to ensure the implicit argument is preserved as an argument.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Authored-by: digama0 (commit)

[Mike Shulman]

Alex J. Best said:

What is your use case for the editor? I'd recommend sticking to the newest lean and using gitpod instead for a web-based play around, does that work for you?

When I teach, I can open up the web editor in a browser on the classroom PC and livecode without having to configure or install anything. I don't know anything about gitpod, can I do that with it?

[Matthew Ballard]

Yes. You only need a browser in class.

[Matthew Ballard]

You will have to do a one time setup though (on some machine).

[Matthew Ballard]

Are you using mathlib while teaching?

[Mike Shulman]

Sometimes.

[Matthew Ballard]

• Sign up for GitPod
• Make a repo for your notes at GitHub
• Add this yaml file to it
• Add this bash script to /scripts folder
• Navigate to gitpod.io/#https://github.com/$USER/$REPO

[Matthew Ballard]

Caveats: untested and there is a time limit of 50 hours/month to the free plan. I don't assume you are teaching 50 hours/month.

[Alex J. Best]

I think that is CPU time anyways, so not necessarily easily estimable. Anecdotally though I use gitpod all the time for reviewing PRs and never run out provided everything is set up right. And im sure they have an eduction plan for free extra time too

[Matthew Ballard]

I think their hat tip to education is a limited-time free standard tier (100 hrs) when you sign up for education benefits with GitHub

[Matthew Ballard]

But I would like to be proven wrong

[Matthew Ballard]

Alternatively, there is also a free allowance for Codespaces. Based on the files in mathlib, I made a bare repo which gets you elan and leanproject (and nothing else) when you create a codespace.

[Alex J. Best]

Unfortunately (this is the case with mathlib's setup too it seems) the lean extension doesn't work in codespaces for web, so it seems less useful than a gitpod version

[Matthew Ballard]

Huh. The Lean 4 extension works great.

[Alex J. Best]

I get the same message "the lean4 extension is not available for vscode for the web", so we must have different set-ups somehow. How are you running codespaces?

[Matthew Ballard]

Oh. It seems that the Lean 3 extension is working for me too. :thinking:

[Alex J. Best]

Ah I see there are desktop and browser versions of codespaces, that must be the difference.
The browser one is what opens by default for me if I press . on a github repo.

[Alex J. Best]

So you could use this if you have vscode installed but not lean on that machine it seems

[Alex J. Best]

This default opening behaviour can be changed in https://github.com/settings/codespaces

[Matthew Ballard]

Oh, I dont think . is codespaces.

[Matthew Ballard]

I think its a bare-bones thing called vscode for web.

[Matthew Ballard]

To get a codespace, you can click on the green Code button on the GitHub repo page, navigate to the codespaces tab, and click Create a Codespace on ${branch}.

[Notification Bot]

22 messages were moved from this topic to #new members > lean in browser on classroom PC by Mike Shulman.

[Kevin Buzzard]

Do you have a bunch of olean files in _target ?

[Mike Shulman]

@Kevin Buzzard Who are you asking, and with reference to what?

[Kevin Buzzard]

You, and with reference to

Then when I open up a file that imports something from mathlib, it spins for a while and I get the "excessive memory consumption" error.