Comment by JuniperMesos
5 hours ago
In particular a number of other projects assume that you have a GitHub account. https://github.com/rust-lang/crates.io/issues/326 has been open for literally a decade without any meaningful work. If you want to publish a Lean software packages on Reservoir, the official Lean package registry, their requirements (https://reservoir.lean-lang.org/inclusion-criteria) not only specify a GitHub project specifically, but having at least two stars on GitHub as a "basic quality filter". Microsoft is a big funder of Lean and I can't help but think this is a deliberate restriction to increase lock-in on a Microsoft-owned platform.
No comments yet
Contribute on Hacker News ↗