Zulip Chat Archive

Stream: new members

Topic: notation names


Mike Shulman (Oct 20 2022 at 17:01):

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 (Oct 20 2022 at 17:02):

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 (Oct 20 2022 at 17:04):

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 (Oct 20 2022 at 17:07):

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 (Oct 20 2022 at 17:08):

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

Mike Shulman (Oct 20 2022 at 17:08):

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

Matthew Ballard (Oct 20 2022 at 17:09):

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

Mike Shulman (Oct 20 2022 at 17:09):

what.

Matthew Ballard (Oct 20 2022 at 17:10):

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

Mike Shulman (Oct 20 2022 at 17:10):

Will it also work in Lean 3?

Matthew Ballard (Oct 20 2022 at 17:12):

Eg. EmptyCollection exists to supply

Alex J. Best (Oct 20 2022 at 17:12):

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

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

Matthew Ballard (Oct 20 2022 at 17:13):

Is ¬ reserved this way in Lean 3?

Alex J. Best (Oct 20 2022 at 17:15):

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 (Oct 20 2022 at 17:35):

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 (Oct 20 2022 at 17:49):

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 (Oct 20 2022 at 17:49):

Yes. You only need a browser in class.

Matthew Ballard (Oct 20 2022 at 17:50):

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

Matthew Ballard (Oct 20 2022 at 17:52):

Are you using mathlib while teaching?

Mike Shulman (Oct 20 2022 at 18:18):

Sometimes.

Matthew Ballard (Oct 20 2022 at 18:24):

  • 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 (Oct 20 2022 at 18:24):

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 (Oct 20 2022 at 18:31):

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 (Oct 20 2022 at 18:43):

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 (Oct 20 2022 at 18:45):

But I would like to be proven wrong

Matthew Ballard (Oct 20 2022 at 19:50):

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 (Oct 20 2022 at 19:55):

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 (Oct 20 2022 at 19:59):

Huh. The Lean 4 extension works great.

Alex J. Best (Oct 20 2022 at 20:04):

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 (Oct 20 2022 at 20:05):

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

Alex J. Best (Oct 20 2022 at 20:06):

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 (Oct 20 2022 at 20:06):

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

Alex J. Best (Oct 20 2022 at 20:08):

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

Matthew Ballard (Oct 20 2022 at 20:08):

Oh, I dont think . is codespaces.

Matthew Ballard (Oct 20 2022 at 20:09):

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

Matthew Ballard (Oct 20 2022 at 20:13):

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 (Oct 28 2022 at 21:08):

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

Kevin Buzzard (Oct 28 2022 at 21:25):

Do you have a bunch of olean files in _target ?

Mike Shulman (Oct 31 2022 at 17:36):

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

Kevin Buzzard (Oct 31 2022 at 20:42):

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.


Last updated: Dec 20 2023 at 11:08 UTC