import not from mathlib

Stream: general

[Filippo A. E. Nuccio]

I have been asked to give a talk about Lean and I am producing a talk.lean file to use during the presentation. I have simply put this new file outside of mathlib (in another git repository) and I work with VSCode, with which I open my local mathlib and then work on talk.lean, which happily imports every file which is in mathlib in the standard way, e.g. with

import topology.basic
import analysis.convex.cone

But now I would like to import another file, say burp.lean which is not in mathlib; how can I specify (and can I specify?) the full path of burp so that talk.lean accepts something like

import ???.burp

[Yury G. Kudryashov]

AFAIK, you have 2 options:

• add this file to the same repo where you have talk.lean;
• add the project that contains burp as a dependency in leanpkg.toml (probably you already have mathlib as a dependency).

[Kevin Buzzard]

When I give demos in talks I just work within mathlib and add new files (often in a scratch directory which I make) but I've never had to import a new file in a second new file before

[Filippo A. E. Nuccio]

@Yury G. Kudryashov @Kevin Buzzard : thanks, both seem very good ideas. But I guess that for both options, you need to work in a separate branch of mathlib, is that right (ot that I don't want to create it, I just try to get my git OK). Because otherwise it would try to push both the leanpkg,toml and the scartch directory to master, which won't work... Finally, very stupid question: the toml file, I modify it by simply opening with a text editor and adding the path of burp.lean?

[Kevin Buzzard]

The simplest approach for a one-off talk is not to modify any configuration files or to change any branches or anything, to work directly with a local clone of mathlib, and just to put burp.lean in src. Then you can just import it with import burp. There are plenty of other ways to make it work but they will all be more complicated.

[Kevin Buzzard]

You can just set this up by making some directory called my_talk, running leanproject get mathlib within that directory (giving you a new mathlib which you are free to corrupt or break without causing any trouble to your current set-up), and then just dumping anything new which you want to import later on into src. Then just open this copy of mathlib using VS Code.

[Kevin Buzzard]

Another approach is to make a new project of your own with leanproject new my_talk and then just put files into src there, and then you can import them -- this is how LTE is set up for example, where we can import other LTE files and also mathlib files at the same time. But for a one-off talk I would not go to so much trouble. Again you don't have to edit any configuration files, leanproject will do it all for you.

[Filippo A. E. Nuccio]

Yes, this seems by far the easiest path, thanks. I just have a small doubt about running leanproject get mathlib in a the directory my_talk; this will create a mathlib folder inside my_talk, but it will also initiate this subdirectory as a git repository whose remote is the usual mathlib, right? In particular, I won't be able to push, which I'd like to, for backup and future references. I imagine that the only ways to be able to push things remotely are either to manually de-initialise this folder or to create a branch different from master, no?

[Eric Wieser]

I would recommend the leanproject new approach

[Eric Wieser]

That way you can also point people to a working copy of the code from the talk, which they could even open in gitpod

[Filippo A. E. Nuccio]

OK; does the new command automatically creates a remote git repo, or simply a local one which I need to init?

[Eric Wieser]

It definitely doesn't create a remote one, but I don't think it creates a local one either

[Eric Wieser]

Create the git repo first, then run leanproject new in it

[Eric Wieser]

Or alternatively; try it and see

[Filippo A. E. Nuccio]

Thanks!