[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-20 19:38, Carette, Jacques wrote:
> [..]

> My take homes, if the plan is to continuing growing the "Agda
> ecosystem":
> - the community ought to pick a single communication system (Slack,
> Discord, Zulip, gitter, whatever, but just one!)
> - 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)
> - actively push people who have useful private libraries to submit
> them (perhaps in pieces) to stdlib
> [..]


The Standard library size needs to have some reasonable bound for it, 
and all the remaining
room is for applied libraries. For a widely used system, the total 
volume of applied
libraries is expected to be may be 1000 times larger than the stdlib 
volume.

--
SM