> On Wed, Jun 28, 2017 at 05:37:53PM -0400, Benjamin Barenblat wrote: > > Description : theorem prover from Microsoft Research
On Thu, Jun 29, 2017 at 1:41:57 AM, Julian Andres Klode <j...@debian.org> wrote: > I don't think we need the company advertisement here, though. 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”. > > 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? 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.” > > 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 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. > […] the quote might have licensing issues. 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.
