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

Groups > sci.logic > #342663

SWI Agent Provocateur gets kicked out of Rocq? (Re: Coq/Rocq and how to completely break it)

Cross-posted to 3 groups.

Show all headers | View raw

Hi,

Woa! I could have told you so. Although hired
by EricGT to provoke me on SWI-Prolog discourse,
and then EricGT kick me out of SWI-Prolog discourse,

on grounds "not listening to staff". The same
Julio Di Egidio who invented nonsense stuff on
SWI-Prolog discouse, to annoy me.

Had his lesson teached about the usual code of
conduct in politically correct forums, where one
has to adopt a "performative" way of telling

technical thruths, either by not telling them,
because the community has already lost their
moral compas, and is only producing hot air,

or just quitting the community. The lesson was
already posted in 2023:

Théo Zimmermann
For anyone who might have followed this discussion or any of the recent 
discussions in which Julio Di Egidio was a participant and which turned 
sour, we (administrators of the Coq Zulip and members of the Code of 
Conduct enforcement team) want to let everyone know that we do not 
consider this behavior acceptable (regardless of its technical content). 
A prior warning had been addressed to Julio in August 2023. Following 
this warning and recent new reports, we have decided to send a new 
warning accompanied by a temporary ban, that could be lifted with a 
statement that the offender would follow our rules in the future.

Bye

Julio Di Egidio schrieb:
> 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 sci.logic | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-07-10 14:01 +0200
  Re: Coq/Rocq and how to completely break it Julio Di Egidio <julio@diegidio.name> - 2025-07-10 14:31 +0200
    Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it) Mild Shock <janburse@fastmail.fm> - 2025-07-15 18:31 +0200
      Having 2544 issues is probably a bad sign (Was: Maybe AGI should take over proving) Mild Shock <janburse@fastmail.fm> - 2025-07-15 18:34 +0200
        The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign) Mild Shock <janburse@fastmail.fm> - 2025-07-15 19:01 +0200
    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
      SWI Agent Provocateur gets kicked out of Rocq? (Re: Coq/Rocq and how to completely break it) Mild Shock <janburse@fastmail.fm> - 2025-11-30 10:28 +0100
        How to get GigaLIPS for Transitive Closure (Was: SWI Agent Provocateur gets kicked out of Rocq?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 11:20 +0100
          I am already using this method for 20 years [AI Effloreszenz] (Was: How to get GigaLIPS for Transitive Closure) Mild Shock <janburse@fastmail.fm> - 2025-11-30 11:32 +0100
            New branding Accelerated Linear Algebra [OpenXLA C++] (Was: I am already using this method for 20 years) Mild Shock <janburse@fastmail.fm> - 2025-11-30 11:43 +0100
        When put in virtual jail, ask for removal of your content (Was: SWI Agent Provocateur gets kicked out of Rocq?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 12:55 +0100

csiph-web