On Wed, Jun 28, 2017 at 05:37:53PM -0400, Benjamin Barenblat wrote:
> Package: wnpp
> Severity: wishlist
> Owner: Benjamin Barenblat <bba...@mit.edu>
>
> * Package name : lean
> Version : 3.2.0
> Upstream Author : Leonardo de Moura <leona...@microsoft.com> et al.
> * URL : https://leanprover.github.io/
> * License : Apache-2.0
> Programming Lang: C++
> Description : theorem prover from Microsoft Research
I don't think we need the company advertisement here, though.
>
> 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.
This looks good so far for the package description, not sure about
the rest though:
>
> From the About page: “Lean is a new open source theorem prover being
> developed at Microsoft Research, and its standard library at Carnegie
Sounds weird, how can a standard libary develop something?
> 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.
Seems like this is not a good fit for the package description, and
the quote might have licensing issues.
--
Debian Developer - deb.li/jak | jak-linux.org - free software dev
| Ubuntu Core Developer |
When replying, only quote what is necessary, and write each reply
directly below the part(s) it pertains to ('inline'). Thank you.
