is this a correct summary of how to create libraries ?

Stream: new members

[rzeta0]

It is surprisingly difficult to find guidance on the internet about creating libraries of lemmas to be used in lean proofs.

Question: So I wanted to ask if my summary below is (1) correct, and (2) missing something major?

Specifically, I am unsure of:

1. is it only VSC that recognises the change in makefile.lean and triggers a recompilation?
2. does it even trigger a recompilation or does something else happen, eg updating "header" files?
3. is it true / necessary / good practice to import custom libraries after the official ones?

---

There are two key steps.

Library

In a project’s lakefile.lean file, add a reference to the Lean file which contains your lemmas, as follows:

lean_lib MyLeanLemmas

Replace MyLeanLemmas with the name your chose for your own library.

If you’re using a Lean enabled editor, the change will be recognised and contents of the library compiled, ready for use.

Using A Library

To use the lemmas in the MyLeanLemmas library, we simply use import at the top of our lean program.

import Mathlib.Tactic import MyLeanLemmas

Additional libraries should be imported after any official Mathlib libraries.

[rzeta0]

If any of the above is incorrect - do let me know.

[Julian Berman]

I don't understand your first two questions.

[Julian Berman]

(I assume makefile is lakefile). Lean / lake / VSCode / any editor all could be said to be usable for compiling or recompiling a Lean project.

[Julian Berman]

I don't know whether the style guide says anything about import order, I think it doesn't say anything, but let's see, I think it's #style.

[Julian Berman]

Yeah, seems not from a scan. I'd do it personally probably just because it's common in many languages, and maybe some Lean code already does, but it would seem there's no explicit community guidance from the Mathlib style guide at least.

[Julian Berman]

I don't 100% follow the connection between your questions and the stuff below the divider -- I guess you're asking whether the thing you're writing below is good guidance? I'd probably mostly focus on lakefile.toml (rather than lakefile.lean) if you're writing a short beginner something, as that's simpler and it's what someone would get by default from lake new / lake init.

[rzeta0]

Thanks for the link to the style guide - I wasn't aware of it.

The first two questions are based on my observation that when I create a lean_lib in lakefile.lean the VSC status dialog tells me something is happening which takes a few seconds. It then prompts me to restart Lean.

Screenshot attached.

My guess is it is compiling the referenced lean file, and updating some kind of local header file so that references to lemmas can be resolved.

And part of my question was - is it only VSC that notices this change because it is continuously running lean unlike say editing the lakefile.lean in vi or notepad?

Screenshot 2024-11-20 at 21.41.02.png

[rzeta0]

also my environment doesn' have lakefile.toml .. is that a new thing?

my environment appears to be Lean "v4.12.0"

[Julian Berman]

rzeta0 said:

also my environment doesn' have lakefile.toml .. is that a new thing?

my environment appears to be Lean "v4.12.0"

It was initially written in February so probably it's present in 4.12, but 4.13 is the first version that emits lakefile.toml by default.

And part of my question was - is it only VSC that notices this change because it is continuously running lean unlike say editing the lakefile.lean in vi or notepad?

I would have assumed that that behavior was signalled via the language server in the same way that e.g. the message saying imports are out of date and prompting you to restart does -- but it appears it doesn't (by which I mean that lean.nvim doesn't appear to notice if I edit a lakefile.toml). I'm sure however it works would be trivial to replicate though, yes, it'll be something having to do with watching the file presumably.