importing from mathlib archive

Stream: general

[Kevin Buzzard]

The "main" part of mathlib(3) is in /src but there are a few files in /archive, e.g. archive/100-theorems-list/16_abel_ruffini.lean . Is it possible to import one of these files (e.g. that one), just as a one-off, in some test file in a Lean 3 repo which has mathlib as a dependency? I just wanted to show off Thomas Browning's Abel-Ruffini in the same file as some other Galois-related stuff (in a file which won't be imported by anything else). It would be slightly nicer than just switching over to the file itself (which I will do if nobody tells me how to do this in the next 8 hours or so...). I am slightly worried about the numerals at the beginning of the directory/file names as well as the fact that it's not in src...

[Kyle Miller]

Maybe you could copy 16_abel_ruffini.lean into your project with an importable name? That seems better than working inside that file, and it's not so bad since you (hopefully) only need to copy a single file.

[Eric Wieser]

You can edit your leanpkg.path file to include a reference to where the archive folder is

[Eric Wieser]

It might be possible to do that more permanently from the leanpkg.toml

[Eric Wieser]

But whatever you do it's going to be a hack

[Eric Wieser]

leanpkg' dependency handling isn't set up to deal with git repos containing multiple lean projects

[Kevin Buzzard]

Thanks for the ideas!