Post #2049507

Speaking personally, I understand that this announcement may be disappointing to anyone whose use-case falls outside the language variant we plan to support. However, I simply do not think it is feasible to give each feature the care it deserves while keeping to the scope of the upstream codebase. As an example, in the process of cleaning up the forked codebase, I found yet another proof of false involving irrelevant record fields, an outcropping of a feature we plan to cut entirely. We could keep playing whac-a-mole with these features, as upstream surely will, but I personally believe that our limited time is better spent improving Mikan instead of fighting fires in language features none of us are especially invested in. Mikan is libre software, so our patches can be adopted by any compatibly-licensed fork that shares our values; I'm also personally happy to lend my expertise in the codebase to anyone who plans to maintain a fork like this for their own subset of the Agda language.