Looking for help

Stream: new members

[Freek Wiedijk]

I would like to try Lean again, but I'm sure I will need help, both with Lean and on how to deal with Zulip. @Floris van Doorn advised me to use this channel for now, I hope that's okay. I plan to ask my questions as responses in this thread, is that reasonable?

[Freek Wiedijk]

For example, how do I configure Zulip, so that I won't be noticed about unread messages other than those explicitly mentioning me, and the ones in this thread? All those huge and steadily increasing numbers of unread messages I don't want to see.

[Yaël Dillies]

Hey! You can Mute channel

[Freek Wiedijk]

That's helpful! So if I also mute the #new members channel, will I still be notified of responses to my messages there?

[Freek Wiedijk]

I plan to unmute stuff selectively as I move on, but for now I would prefer not to be overwhelmed.

[Yaël Dillies]

I believe so. Just in case, you can also more selectively mute and unmute individual topics

[Freek Wiedijk]

But the menu command in your screenshot is just about catching up, as soon as someone posts something in a thread, it will be asking for attention again?

[Freek Wiedijk]

Anyway, I see that you can also unsubscribe from a channel as well. I'm now busy both muting and unsubscribing from all channels. Even that is daunting!

[Freek Wiedijk]

A more serious question: I would like to set up things so I have just one Lean installation in ~/.elan/toolchains on my system, and one mathlib in .lake/packages/mathlib. For that I plan to have a single "project" that contains that single mathlib, with all the real projects that I work on in subdirectories. So I would like to regularly run some command (lake update?) to update that "project" so that I get up-to-date.

[Freek Wiedijk]

Now, the question for me is what versions those should have. For Lean I would like to update (say nightly) to the "stable" version (at what point then the older Lean installation should be deleted). For mathlib, I would like it to be the version that matches the stable Lean version or the current version on master in git (I guess those are different?)

[Freek Wiedijk]

So how do I set up things that it will work like this?

[Floris van Doorn]

You can indeed choose to have 1 mega-project that all work will be on the same version of Mathlib + Lean. This might be a little tricky when collaborating, and only sharing a subset of your project with a collaborator, but I imagine it's doable.

I recommend that you stay on the stable version of Lean, which updates every month, and its corresponding Mathlib version. You can also stay on the release candidate for Lean (then you're 1 month ahead in Lean features) and can update Mathlib however frequently you want. It doesn't matter that much which one you choose, and you can easily switch. You can specify this in your lakefile.

To create a new project, run lake new MyProject math (more detailed instructions here). Then you can edit the lakefile.toml and add rev = "stable" under the mathlib dependency if you only want to update Lean once a month (no need to change anything if you always want the latest version.

[Floris van Doorn]

To actually update Mathlib/Lean just run lake update in your repo. You can then write a small script to uninstall previous versions of Lean (using elan toolchain uninstall ...), and delete the compressed .olean files you downloaded (the uncompressed ones are in your project directory and should be kept).

[Floris van Doorn]

You can specify the environment variables ELAN_HOME and XDG_CACHE_HOME (at the very start of the process) if you want to customize the location where the installed Lean toolchains and the compressed .oleans will be stored. Besides your project directory, these are the only directories with any Lean-related files (AFAIK). See also this thread

[Floris van Doorn]

There's been talk of specifying a custom directory where your dependencies are kept, but I don't know if there is an easy/workable solution for that (this would allow you to create multiple projects, but only have 1 location with the dependencies).

[Freek Wiedijk]

This is very helpful, I'll fiddle with this. I understand "stable" changes once a month? (Just for my curiosity: if I clone mathlib, and checkout master, how do I find what Lean version this belongs to?)

[Freek Wiedijk]

So what are the defaults for ELAN_HOME and XDG_CACHE_HOME? The first is ~/.elan, I guess, but what is the other?

[Moritz Firsching]

Freek Wiedijk said:

This is very helpful, I'll fiddle with this. I understand "stable" changes once a month? (Just for my curiosity: if I clone mathlib, and checkout master, how do I find what Lean version this belongs to?)

you can look in this file:
https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain

[Freek Wiedijk]

Very nice! So what if I have my "project", and then decide I want to go to master in .lake/packages/mathlib? What do I update, or what command do I utter (or both), to get my project in a state that that will work? I guess before lake update I need to change something. Is that again just editing lakefile.toml, like @Floris van Doorn wrote, or do I (also) need to issue some command?

[Moritz Firsching]

I think the recommended way is to copy exactly this toolchain file and then run lake update:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

[Moritz Firsching]

but his won't give you the stable version that was discussed above

[Moritz Firsching]

you then probably want to remove the rev="stable" again

[Freek Wiedijk]

Thanks again! So what is the relation between lakefile.toml and lean-toolchain? If the first has a rev="...", it updates the latter whenever lake update is run, and otherwise it leaves it alone?

[Freek Wiedijk]

And I see that lakefile.toml has sections, in which does this rev line belong? And is the format of this file documented somewhere?

[Jireh Loreaux]

file format description

[Ruben Van de Velde]

Freek Wiedijk said:

Thanks again! So what is the relation between lakefile.toml and lean-toolchain? If the first has a rev="...", it updates the latter whenever lake update is run, and otherwise it leaves it alone?

lake update will (should) always update the lean-toolchain to match the version of mathlib you're using. If you stick to the "stable" revision of mathlib, you only get a new version of mathlib once a month, which also comes with a new lean version

[Julian Berman]

Freek Wiedijk said:

So what are the defaults for ELAN_HOME and XDG_CACHE_HOME? The first is ~/.elan, I guess, but what is the other?

(Generally ~/.cache -- it's a thing which is widely used, not Lean specific, for "put all my cache stuff here". Just to round out the trio, there's also $MATHLIB_CACHE_DIR, which is Lean and even Mathlib specific, and defaults to $XDG_CACHE_HOME/mathlib, so really by setting $XDG_CACHE_HOME it's somewhat that that you're affecting).

[Freek Wiedijk]

I almost get it now... :blush:

Ruben Van de Velde said:

lake update will (should) always update the lean-toolchain to match the version of mathlib you're using. If you stick to the "stable" revision of mathlib, you only get a new version of mathlib once a month, which also comes with a new lean version

Ah, I thought the rev field was just about the Lean version! But I guess it is about the "package", which includes mathlib? So, what if I don't have rev and either modify lean-toolchain or .lake/packages/mathlib/lean-toolchain myself (the latter by going to a different gif revision), will the other automatically be updated? Or do I then need to give some lake command to fix things up?

[Freek Wiedijk]

And both the Lean system itself and mathlib have "stable" versions? Are these independent? So the mathlib one is updated once a month, but how about the system? I seem to remember that was more frequent (once a day?)?

[Kevin Buzzard]

You surely must have a lean-toolchain, isn't this the file which tells the system which version of lean to use when reading the lakefile.lean?

[Freek Wiedijk]

My project has no lakefile.lean, but instead a lakefile.toml, although I guess that is irrelevant for this. So what I would like to understand is how versions are determined when doing lake update, both with and without a rev entry in either of those files. And also, if I decide I want to move my project to specific versions, how to do it.

[Freek Wiedijk]

Also, there are two of these files in a project that may be inconsistent: lean-toolchain and .lake/packages/mathlib/lean-toolchain. So fiddling with those without knowing what you're doing probably is not too smart.

[Freek Wiedijk]

Another question: all the stuff popping up all the time when I move my mouse over a Lean file really gets on my nerves (also it tends to get in the way of stuff I'm trying to read). Is there a way to tell VS Code to only pop up like that if I am holding some modifier key?

[Floris van Doorn]

If you run lake update, Lean will update the dependencies to their specified versions (by default that is master). When updating, the lean-toolchain file is automatically updated to use the Lean version that Mathlib needs (this is a bit hacky, and might have changed since I last looked).

[Floris van Doorn]

Freek Wiedijk said:

Another question: all the stuff popping up all the time when I move my mouse over a Lean file really gets on my nerves (also it tends to get in the way of stuff I'm trying to read). Is there a way to tell VS Code to only pop up like that if I am holding some modifier key?

Not that I know, but I think I would like to have it as well, and I would start using it for teaching. I agree it's distracting sometimes.
There seems to be an option Lean4 › Infoview: Show Tooltip On Hover, but that only works in the infoview, not the source document. Maybe something like this could be added for the source file as well? (cc @Marc Huisinga)

[Marc Huisinga]

See the VS Code extension manual section on hovers, which describes the setting that VS Code provides for this: https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md#hovers

[Floris van Doorn]

Nice, thanks!

[Freek Wiedijk]

Another question (sorry to reuse this thread, if I should ask this in a new thread, just tell me):

I'd like something like this, because I want Lean to know that types like Fin 3 are non-empty:

import Mathlib.Data.Fin.Basic

class positive [LinearOrder α] [Zero α] (x : α) where
  pos : 0 < x

instance : positive (Nat.succ n) where
  pos := n.succ_pos

instance [positive n] : Nonempty (Fin n) :=
  .intro ⟨_, positive.pos⟩

and I feel sure that this is in the library already. So what is the best way to look for a typeclass like positive in Mathlib?

Also, I named positive and pos rather arbitrarily. What would be the standard convention for naming this?

Also, this import line was chosen fairly randomly. What is the best way to determine what imports one should put at the top of a file? Putting import Mathlib works, is that importing everything? But a subdirectory like import Mathlib.Data.Fin doesn't work?

[Vlad Tsyrklevich]

For the second question, you can use #min_imports at the bottom of the file, often it's convenient to import all of Mathlib and then minimize it at the end to ensure you don't miss any theorems/instances while you're working

[Vlad Tsyrklevich]

(deleted)

[Vlad Tsyrklevich]

lets try that again, @loogle Nonempty (Fin _)

[loogle]

:search: Fin.pos', Fin.size_pos', and 2 more

[Freek Wiedijk]

Am I correct that this loogle query does not find the "positive" typeclass that I was looking for?

[Vlad Tsyrklevich]

Yes, so it finds the instance you're looking for but not positive

[Freek Wiedijk]

Sorry, I don't understand: these four hits that loogle finds are not instances?

[Freek Wiedijk]

But knowing about loogle is great, thanks!

[Vlad Tsyrklevich]

So it depends on what you're looking for, if you're just looking for Nonempty (Fin n) with the hypothesis h : 0 < n then Fin.pos_iff_nonempty.mp h should yield it.

[Vlad Tsyrklevich]

re loogle, Jireh's talk https://www.youtube.com/watch?v=UJrYKR01QwU has a great introduction to search tools that taught me how to use loogle far more effectively

[Freek Wiedijk]

What I was trying is to just have a typeclass positive hanging around for my natural number, from which the nonemptiness then is derived automatically. Or, relatedly, being able to prove Nonempty (Fin 3) using type inference:

example : Nonempty (Fin 3) := by
  infer_instance

[Vlad Tsyrklevich]

So Lean has an docs#NeZero type class that is functionally identical here if you're working over the naturals. I don't know of a positive type class. Someone else would be more qualified to speak to design decisions made in Lean/Mathlib regarding when to use type classes vs hypotheses

[Vlad Tsyrklevich]

I'm also not sure how to tell you how to find that particular type class, I just happen to know it exists

[Freek Wiedijk]

NeZero is good enough, great! So, question to everyone (@Floris van Doorn?), how does one search for this?

Also, my question about naming conventions in Mathlib (should positive have been capitalized and should pos have been out like in NeZero?) is still open. Is there documentation about that?

Or more generally, how does one get acquainted with Mathlib? I'd like to have something like a "tourist guide" for that territory :smile:

[Floris van Doorn]

To find instances: use #synth:

variable {n : Nat} [NeZero n]
#synth Nonempty (Fin n)

You can click on the result, and recursively on the popups to see that it uses docs#Fin.instInhabited

[Floris van Doorn]

To search lemmas, I have some notes here: https://github.com/fpvandoorn/LeanCourse24/blob/f8f8aea8ea65f70314f4207db7dfe9ff9bdc7325/LeanCourse/Lectures/Lecture2.lean#L150-L185
(Mathematics in Lean probably has similar remarks)
(#synth is not mentioned there, since I haven't explained instances yet)

[Floris van Doorn]

When searching for a theorem/definition where you know the mathematical name, you can use the library overview: https://leanprover-community.github.io/mathlib-overview.html or try your luck with https://leansearch.net/

[Floris van Doorn]

Note: Inhabited is the data-carrying version of Nonempty

[Floris van Doorn]

Btw, if your question was "How would I learn the existence of NeZero", you could have learned it from looking at the output of #synth Nonempty (Fin 3).
If you're wondering how to learn about the existence of #synth: then you'd have to read a textbook like Mathematics in Lean, or if you want all the nitty-gritty details, the reference manual: https://lean-lang.org/doc/reference/latest//Type-Classes/Instance-Synthesis/#Lean___Parser___Command___synth (remark: the reference manual is still incomplete, but nowadays it has a lot of information)

[Floris van Doorn]

It's hard to write a tourist guide for Mathlib. To learn about what is in Mathlib, search for definitions and lemmas using the above methods. Then read the surrounding lemma statements, the documentation and the module doc (documentation at the top of the file). That is the best way to learn Mathlib design decisions. Writing a single document that explains all that would get unwieldy quickly.
If you want to learn a proof technique, try to find a proof in Mathlib that uses that technique and see how the lemmas are stated and proven there...

[Freek Wiedijk]

Another search question (hopefully, I will get the hang of finding stuff myself at some point): I'm looking for the obvious function of type (α → Option β) → Option (α → β) where I have [Fintype α]. I have been moogling and loogling and grepping, but I don't see it...

[Robin Arnez]

Do you mean this "obvious function":

def obviousFunction [Fintype α] (f : α → Option β) : Option (α → β) :=
  if h : ∀ x, (f x).isSome then
    some (fun a => (f a).get (h a))
  else
    none

(I have no idea whether that exists already, I don't think so..., correct me if I'm wrong)

[Freek Wiedijk]

Yes, that's what I meant (of course :smile:)! But I cannot imagine this not being there somewhere already...

[Robin Arnez]

@loogle (_ → Option _) → Option _

[loogle]

:search: List.findSome?, Option.orElse, and 18 more

[Robin Arnez]

Hmm there are only a few functions that look like what you want and none of them return a function -- so probably what you want doesn't exist already.