Which imports for textbook examples?

Stream: new members

[Luke Mantle]

I'm following this page of the Mathematics in Lean textbook, and I'd like to play around with the examples myself. How can I tell which imports I need at the start of my file?

[Pedro Sánchez Terraf]

AFAIK, you can find them in the sources of for the textbook. For example, this line and the next two.

[Pedro Sánchez Terraf]

I guess you'll be missing some library there, but you can download that file and put it nearby. Let me check.... EDIT: It seems that the library bit is needed for the Tutorial, not for this one

[Pedro Sánchez Terraf]

One thing I did was to put some of the sources on a repo, and then fill some gaps in. You can check some of my solutions (most probably not the best ones) from this commit on.
... perhaps is simply better to go to the relevant directory and check the history of each file there.

[Luke Mantle]

Hey, thanks for the help!

I tried copying the whole raw source from this tutorial page into an empty scratch file, and I'm getting loads of errors. I'm assuming this is just more stuff from me being a beginner, but what might be the problem?

[Luke Mantle]

What I'm really interested in is learning how to work with one-dimensional derivatives and integrals in Lean; is there a better place to start?

[Jireh Loreaux]

Copying the source into an empty scratch file is not the way to go. If you want to play around in Mathematics in Lean, then you want to hop into a shell and type leanproject get mathematics_in_lean. This will download the repository as well as the relevant mathlib cache for that book (note: that book is working from an older version of mathlib than is currently available, and if you tried to mix-and-match the book with the current mathlib, some things would break).

[Luke Mantle]

Ah, is there anothe book that uses the current up-to-date version of mathlib?

[Patrick Massot]

The difference with the current mathlib is completely irrelevant to the content of this book. In the worst case scenario there will be a couple of things having moved a bit.

[Kevin Buzzard]

If you install the project using leanproject get mathematics_in_lean then it will get the correct version of mathlib, you don't have to worry about compatibilities.

[Jireh Loreaux]

I'm sure also the book will get updated to a newer mathlib after the port to Lean 4, but likely not before then.

[Patrick Massot]

We could start updating, but this doesn't sound urgent.

[Jireh Loreaux]

no, certainly not. I only wanted to explain that this is why you can't open a current copy of mathlib, copy and paste the exercises into a new file and expect it to work. Hence the suggestion to do it the right (and easy) way with leanproject get mathematics_in_lean

[Pedro Sánchez Terraf]

Jireh Loreaux said:

Copying the source into an empty scratch file is not the way to go. If you want to play around in Mathematics in Lean, then you want to hop into a shell and type leanproject get mathematics_in_lean.

Thanks a lot for the clarification! I'm sorry if my advice was misleading.

The way I found to preserve and keep track of my solutions was to start a new leanproject and get (part of) the sources there. I don't know I the get command allows you to push (somewhere) afterwards---needless to say, I did not intend to push to the mathematics_in_lean repo.