Re: Bug#866334: About Bug#866334: RFP: lean -- theorem prover from Microsoft Research
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.
Best wishes,
Julian
Reply to: