Lean on a thumb drive

Stream: general

[Jason Rute]

This PA.SX question might be interesting to folks. They are wondering how to install and run Lean from a thumb drive (no internet). I assume those who teach might have thought of this. (If you have a complete answer, it would be good to post it there.)

[Shreyas Srinivas]

There is no official lean docker container is there?

[Kim Morrison]

There is .docker/gitpod/Dockerfile in the Mathlib repository.

[Shreyas Srinivas]

Is it published on docker hub?

[Kim Morrison]

No. Back in mathlib3 days it was, but it appeared that it was insufficiently useful to warrant the logistical overhead of keeping it up to date.

[Eric Wieser]

I assume the trick here is installing elan on the flash drive, then the rest is easy (as long as you're not trying to work across multiple platforms)

[Jason Rute]

Eric Wieser said:

I assume the trick here is installing elan on the flash drive, then the rest is easy (as long as you're not trying to work across multiple platforms)

At least with the PA.SX question they aren’t using internet which is needed to use Elan.

[Eric Wieser]

Elan doesn't need the internet once it (and the toolchain) is installed

[Ruben Van de Velde]

"(and the toolchain)" is the important point, yeah :)

[Eric Wieser]

True, though once you succeed in installing elan on the flash drive, the rest of the instructions are just "do the rest of the normal process of installing a Lean project while you're online" and the result is a fully-configured flash drive that works offline.

[llllvvuu]

The main non-obvious instruction I can think of is what the user should put in their project's settings to point VSCode to the thumbdrive toolchain via relative path. Otherwise they may have to configure it every time they plug in the drive unless the mount point is deterministic.

[Shreyas Srinivas]

Has anyone tried packaging lean toolchain +mathlib + cache for a fixed version into an AppImage?

[Eric Wieser]

llllvvuu said:

The main non-obvious instruction I can think of is what the user should put in their project's settings to point VSCode to the thumbdrive toolchain via relative path. Otherwise they may have to configure it every time they plug in the drive unless the mount point is deterministic.

Sourcing the .elan/bin/env from the flash drive should hopefully be enough to achieve this, which could be done as part of a script that launches vscode on the right directory.

[Kim Morrison]

Shreyas Srinivas said:

Has anyone tried packaging lean toolchain +mathlib + cache for a fixed version into an AppImage?

Yes, this has been done at various points, but unfortunately the second step (setting up a regular build, with a CI process that tests it works) has not happened to my knowledge, so these efforts have not persisted.