<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<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]-->
</head>
<body lang="EN-CA" link="#0563C1" vlink="#954F72">
<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>
</body>
</html>