The end of the world is nigh:
<https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/status.20and.20future.20of.20the.20phase.20split/near/528029103>
From interactive proof assistant to completely upside-down and
completely broken, and not just on that at that point of course.
And the fucking shamelessness...
On 10/07/2025 14:01, Julio Di Egidio wrote:
The end of the world is nigh:
<https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/status.20and.20future.20of.20the.20phase.20split/near/528029103>
From interactive proof assistant to completely upside-down and
completely broken, and not just on that at that point of course.
And the fucking shamelessness...
But we must thank MS for the nail in that coffin, too: they can't
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 797 |
| Nodes: | 16 (3 / 13) |
| Uptime: | 174:17:54 |
| Calls: | 13,200 |
| Calls today: | 7 |
| Files: | 15,489 |
| Messages: | 6,579,338 |