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. <ballo...@debian.org> Imagine a large red swirl here.