Re: Bug#866334: About Bug#866334: RFP: lean -- theorem prover from Microsoft Research
On Mon, Sep 16, 2019 at 08:39:56PM +0100, Julian Gilbey wrote:
> 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!
Lean is now the theorem prover with the largest community, so it would
be nice to have it in Debian. However I do not know how usable it is
outside the visual studio IDE.
Cheers,
--
Bill. <ballombe@debian.org>
Imagine a large red swirl here.
Reply to: