Re: Bug#866334: About Bug#866334: RFP: lean -- theorem prover from Microsoft Research
On Fri, May 20, 2022 at 07:07:42PM +0100, Julian Gilbey wrote:
> On Fri, May 20, 2022 at 10:59:35PM +0530, Nilesh Patra wrote:
> > On 5/20/22 8:31 PM, Bill Allombert wrote:
> > > 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.
>
> Debian now has the package "elan" which handles installation of Lean;
> this might be sufficient.
Thanks for the tip, I did not know about elan. However installing
software this way really put me off, and it does not seem to install
matlib. Then I found
<https://leanprover-community.github.io/install/debian.html>
(which is 'wget | bash + pip install' variant).
So I feel the RFP to be appropriate, even though probably overwhelming.
Cheers,
--
Bill. <ballombe@debian.org>
Imagine a large red swirl here.
Reply to: