Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.programming > #16870

Re: Coq/Rocq and how to completely break it

From Julio Di Egidio <julio@diegidio.name>
Newsgroups sci.logic, comp.lang.prolog, comp.theory, comp.programming, comp.software-eng, sci.math
Subject Re: Coq/Rocq and how to completely break it
Date 2025-11-30 09:52 +0100
Organization A noiseless patient Spider
Message-ID <10gh0jt$5v4n$1@dont-email.me> (permalink)
References <104oa2l$r4na$2@dont-email.me> <104obqh$r4na$3@dont-email.me>

Cross-posted to 6 groups.

Show all headers | View raw


On 10/07/2025 14:31, Julio Di Egidio wrote:
> 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...

Follow up on Rocq and the appointed pieces of ungodly shit:

Now if I try to login:

<< Account suspended: No constructive purpose to their actions other 
than creating dissent within the community. >>

You pieces of FRAUDULENT UNGODLY SHIT, the defamation added to the
abuse, abuse of power as well as personal.

And the last blow, just to mention the icing on the cake, if the
great people they have been onboarding:

<< FYI: I have no animosity towards you. >>
(Dear Thomas I-am-a-retarded-Nazi Lamiaux, FYI I don't give a shit
whether you smile or not while shitting all over the place, you
fucking nazi-retarded pieces of shit, you and the whole gang...)

YOU UNGODLY FRAUDULENT AND RETARDED PIECES OF SHIT, now it's all
Microsoft and Lean and Lean 2 and sub-Lean and proto-Lean... with
Microsoft's world-famous best practices, top guidance and impeccable
products tailored to their customers' real needs...

Indeed you managers and maintainers and marketers and the fucking
corporate ladder and the whole fucking pyramid indeed: on behalf
of real humanity, I wish you all a rapid ass cancer!!

Bottom line:

Fuck you. And fuck you especially for 20 years of Coq that you have
managed to destroy in less than 5 years, you pieces of pyramidic shit.

*Plonk*

Julio

Back to comp.programming | Previous | NextNext in thread | Find similar


Thread

Re: Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-11-30 09:52 +0100
  Re: Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-11-30 10:00 +0100

csiph-web