Zulip Chat Archive

Stream: general

Topic: import not from mathlib

Filippo A. E. Nuccio (Sep 16 2021 at 22:24):

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 (Sep 17 2021 at 01:30):

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 (Sep 17 2021 at 05:25):

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 (Sep 17 2021 at 08:24):

@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 (Sep 17 2021 at 08:27):

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 (Sep 17 2021 at 08:28):

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 (Sep 17 2021 at 08:31):

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 (Sep 17 2021 at 08:47):

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 (Sep 17 2021 at 08:48):

I would recommend the leanproject new approach

Eric Wieser (Sep 17 2021 at 08:48):

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 (Sep 17 2021 at 08:53):

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

Eric Wieser (Sep 17 2021 at 08:55):

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

Eric Wieser (Sep 17 2021 at 08:55):

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

Eric Wieser (Sep 17 2021 at 08:55):

Or alternatively; try it and see

Filippo A. E. Nuccio (Sep 17 2021 at 08:55):


Last updated: Dec 20 2023 at 11:08 UTC