<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body>
Thanks for the interesting observations! <br>
<br>
My impression is that Agda is used a lot for computer science /
programming language research, while Lean is <br>
used for formalising mathematics (obviously with many many
excpetions). These are different although certainly overlapping
communities. As a result, Lean has huge libraries of formalised (in
Kevin Buzzard's words) generic mathematics, and Agda has many
developments which study the meta-theory of type systems, and so on.
In principle, both communities could use the same system, I guess it
has happened for "soft" reasons (social reasons, "marketing", random
chance etc) that they don't. I don't know whether Lean is
fundamentally better than Agda for formalising maths, or whether
Agda is fundamentally better than Lean for PL research. Probably
not, but I also don't think there is any problem.<br>
<br>
The above is just what I have observed, I don't want to suggest
anything since I think it's very good already :-)<br>
(I agree with the single communication system though, that would
probably simplify things.)<br>
<br>
Nicolai<br>
<br>
<br>
<br>
<div class="moz-cite-prefix">On 20/08/2020 17:38, Carette, Jacques
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:YTBPR01MB3662471D56DED9E9383DC031B45A0@YTBPR01MB3662.CANPRD01.PROD.OUTLOOK.COM">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<meta name="Generator" content="Microsoft Word 15 (filtered
medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
<div class="WordSection1">
<p class="MsoNormal">No, I’m not leaving Agda. I have invested
too much time already, and I really do like it very much. I
am/was incredibly curious as to what seems to make Lean more
of a ‘rising star’.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">My personal conclusions:<br>
- it’s not really the system per se, although Lean being
‘classical’ helps attract a different crowd,<br>
- it’s the *<b>ecosystem</b>*, and in particular,<br>
- the large, extremely active and welcoming crowd of *<b>math-lib</b>*
developers that make Lean so attractive.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The visible face of Lean is not Leonardo,
but a large number of the library developers. They’ve taken to
github and Zulip with a vengeance. There can be 200-300
messages/day (!) on the Lean Zulip. [That’s kind of
exhausting… but I guess that’s the price of success.] Where
there are 18 open PRs on agda-stdlib (with the latest as
#1279), there are currently 77 on mathlib (latest #3879).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The good news for the Agda devs is that the
“system devs” of Lean are basically not visible here. They
exist, are very busy doing cool stuff, but the community is
not run by them at all. Frees the system devs to focus on
their core strengths.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">My take homes, if the plan is to continuing
growing the “Agda ecosystem”:<br>
- the community ought to pick a single communication system
(Slack, Discord, Zulip, gitter, whatever, but just one!)<br>
- the merge-into-stdlib process needs more bandwidth
(Matthew’s done an amazing job, I’m mostly suggesting that he
make proposals as to how to scale up)<br>
- actively push people who have useful private libraries to
submit them (perhaps in pieces) to stdlib<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">For example, there is quite a lot of PL
meta-theory ‘out there’, in Agda. It could make a lot of sense
to augment stdlib with the standard material for that. Lean’s
math-lib is driven by formalizing “regular math” (their
terminology, not mine). To me, it would make sense if Agda’s
stdlib was driven by “the math+CS that its users regularly
use”. [Thus PL meta-theory as an obvious example.]<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Jacques<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">PS: there is not an iota of complaint in
the above. It is 100% meant as conveying my observations, and
personal conclusions on how to build momentum.<o:p></o:p></p>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>