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

[Bill Allombert]

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 

(which is  'wget | bash + pip install' variant).

So I feel the RFP to be appropriate, even though probably overwhelming.

Cheers,
-- 
Bill. 

Imagine a large red swirl here. 

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

[Julian Gilbey]

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

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

[Nilesh Patra]

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.


If you want to direct the conversation onto a mailing list, please use 
debian-math@ instead (CC'ed)
as lean is a math based packages

--
Best,
Nilesh





OpenPGP_signature
Description: OpenPGP digital signature

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

[Bill Allombert]

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. 

Imagine a large red swirl here. 

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

[Julian Gilbey]

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