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: | 741 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 79:54:27 |
| Calls: | 12,451 |
| Calls today: | 1 |
| Files: | 15,194 |
| Messages: | 6,537,725 |