About Bug#866334: RFP: lean -- theorem prover from Microsoft Research

[Julian Gilbey <jdg@debian.org>]

I've just started looking at lean.  One of the issues around packaging
it is that different lean "scripts" (not sure the correct word here)
require different versions of lean.  There is a script available which
downloads the required version of lean for any particular script, and
so keeps a local set of lean versions.

If we were to package lean for Debian, what exactly would we package?
The current stable version, or a script such as this?  See
https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian_details.md
for a little more on this.

Thoughts would be appreciated!

Best wishes,

   Julian