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
Attachment:
OpenPGP_signature
Description: OpenPGP digital signature