* Package name    : lean
  Version         : 3.2.0
  Upstream Author : Leonardo de Moura <leonardo@microsoft.com> et al.
* URL             : https://leanprover.github.io/
* License         : Apache-2.0
  Programming Lang: C++
  Description     : theorem prover from Microsoft Research

Lean is a theorem prover or interactive proof assistant. That is, it’s
a system in which you can write formal mathematical proofs that are
checked for correctness by the computer. Lean is thus broadly similar
to Coq, but the Lean developers hope to build a faster, more extensible
system than Coq is today.

From the About page: “Lean is a new open source theorem prover being
developed at Microsoft Research, and its standard library at Carnegie
Mellon University. Lean aims to bridge the gap between interactive and
automated theorem proving by situating automated tools and methods in a
framework that supports user interaction and the construction of fully
specified axiomatic proofs. The goal is to support both mathematical
reasoning and reasoning about complex systems, and to verify claims in
both domains.”

Lean has been under development for several years; regular releases
first appeared in January. I use Lean, and I know other Debian users
would like to have it easily accessible.

I don't think we need the company advertisement here, though.

This looks good so far for the package description, not sure about
the rest though:

Sounds weird, how can a standard libary develop something?

Seems like this is not a good fit for the package description, and
the quote might have licensing issues.

Maybe. MSR is a well-known name in the programming languages and formal
verification communities, and the fact that they’re behind Lean is
something that many potential users would want to know. That said, I’m
not terribly attached to this description, and I’d feel comfortable just
saying “interactive theorem prover”.

Ha. I agree that it’s not the best-written description. I’d probably
rephrase it as “Lean is a theorem prover developed at Microsoft Research
and Carnegie Mellon University.”

I assume you’re specifically referring to this paragraph, in which case,
you’re completely right. I was responding to the reportbug prompt to
explain why I think Lean ought to be packaged. I don’t intend to include
this praagraph in the description.

We should be in the clear here, since the Lean web site is licensed
under Expat. The quote in question appears in Git at
https://github.com/leanprover/leanprover.github.io/blob/master/about/index.md,
if you’re interested.

Hi Benjamin,

please consider the option of maintaining
this package under the roof of the Debian
Science Team.

Best regards

Anton

Am Mittwoch, 28. Juni 2017 schrieb Benjamin Barenblat :

Hi Benjamin,

Thanks for this ITP.
I'd suggest to package this in Debian Science team.

Kind regards

     Andreas.

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

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,

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

Debian now has the package "elan" which handles installation of Lean;
this might be sufficient.

Best wishes,

   Julian

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,