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

Groups > sci.math > #641469 > unrolled thread

Re: Coq/Rocq and how to completely break it

Back to article view | Back to sci.math

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  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

#641469 — Re: Coq/Rocq and how to completely break it

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

[toc] | [next] | [standalone]

#641470

On 30/11/2025 09:52, Julio Di Egidio wrote:
> 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. >>

Forgot the link, should anybody be interested:

<https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms>
<https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/12>

My complains and the flags to the mods have been hidden/deleted as
abuse, pieces of ungodly fraudulent, not just retarded, shit......

And now go fuck yourself.

*Plonk*

-Julio

> (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.

[toc] | [prev] | [next] | [standalone]

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

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
> 

[toc] | [prev] | [next] | [standalone]

#641480 — How to get GigaLIPS for Transitive Closure (Was: SWI Agent Provocateur gets kicked out of Rocq?)

Hi,

Maybe a probem with the Logic Programming community
is the fact, that they are totally clueless about
linear algebra. Something tells me, we I could

compute the transitive closure via matrix inversion:

(I-M)^(-1) = I + M + M^2 + M^3 + ...

I am pretty sure there are a few Lean or even Rocq
theorems already formalized, showing some of these
identities and their numerical perks.

Still I find here long discussions (**), mareveling
how to compute the transitive closure, in a
sequential setting. But already when M is sparse

things are pretty speedy with linear algebra. Matrices
are perfect for AI Accelerators that are specialized
for linear algebra, since it is one of the most

parallelizable computations in numerical linear algebra.
GPU and distributed HPC performance is excellent,
but one has possibly to consider AI Accelerators nowadays

on laptop and micro servers, for so called Local AI.

Bye

P.S.: (**)
Wanna see a bunch of clueless people associated to Stony Brook or not:
https://discourse.prolog-lang.org/t/subgraph-isomorphism-prolog-vs-conventional/173/7

P.P.S.: I am currently looking into combinatorial search,
but transitive closure is of course also a candidate to
delegate to an AI accelerator when doing Local AI.

Mild Shock schrieb:
> 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
>>
> 

[toc] | [prev] | [next] | [standalone]

#641481 — I am already using this method for 20 years [AI Effloreszenz] (Was: How to get GigaLIPS for Transitive Closure)

Hi,

I am already using this method for 20 years,
just copied the Google Page Rank idea a couple
of decades ago. Its described here:

We solve this equation exactly in that we
calculate R = (E-L)-1*H. The matrix inversion
(E-L)-1 is only computed once for the web site
and is stored across the pages of the web site.
May 14th, 2006 - Web Site Ranking
https://www.herbrand.ai/izytab/doclet/home/03_support/01_browse/05_rank.html

While the matrix inversion was very primitive
in the beginning. I use a couple of ideas to further
develop it. From using sparsity to using tiles,

and doing it with multiple works, and worker
queues. You find everything behind the scenes
now, I did some explorations. Just image what

experience Google has and its TPUs to compute
with matrices, their page rank was what made
them the first attractive search engine, that

could provide information retrieval that made sense.

Bye

P.S.: Disclaimer, I don't say its possible so
easily to replicate the new Gemini AI, by simply
tapping into Local AI via AI Accelerators.

Its more to get a glimpse how the AI Effloreszenz
could happen, did happen. I guess mostly it hapoened
by not by getting obsessed with sequential algorithms

and all the Stony Brook nonsense, but by adopting a
linear algebra view point, with very controlled
doses of parallelism and of course the lock step

innovation in better hardware.

Mild Shock schrieb:
> Hi,
> 
> Maybe a probem with the Logic Programming community
> is the fact, that they are totally clueless about
> linear algebra. Something tells me, we I could
> 
> compute the transitive closure via matrix inversion:
> 
> (I-M)^(-1) = I + M + M^2 + M^3 + ...
> 
> I am pretty sure there are a few Lean or even Rocq
> theorems already formalized, showing some of these
> identities and their numerical perks.
> 
> Still I find here long discussions (**), mareveling
> how to compute the transitive closure, in a
> sequential setting. But already when M is sparse
> 
> things are pretty speedy with linear algebra. Matrices
> are perfect for AI Accelerators that are specialized
> for linear algebra, since it is one of the most
> 
> parallelizable computations in numerical linear algebra.
> GPU and distributed HPC performance is excellent,
> but one has possibly to consider AI Accelerators nowadays
> 
> on laptop and micro servers, for so called Local AI.
> 
> Bye
> 
> P.S.: (**)
> Wanna see a bunch of clueless people associated to Stony Brook or not:
> https://discourse.prolog-lang.org/t/subgraph-isomorphism-prolog-vs-conventional/173/7 
> 
> 
> P.P.S.: I am currently looking into combinatorial search,
> but transitive closure is of course also a candidate to
> delegate to an AI accelerator when doing Local AI.
> 
> Mild Shock schrieb:
>> 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
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#641482 — New branding Accelerated Linear Algebra [OpenXLA C++] (Was: I am already using this method for 20 years)

Hi,

Its amazing what can be done with linear
algebra. Want graph isomorphism formulated
in linear algebra? Try this:

      AX = XB

Didn't try yet. But there is currently a rebranding
going on. The fancy term "tensor" seems to be
not extremly accessible for the many engineers

that anyway know linear algebra already. So we
find for eample now TensorFlow mutated into:

XLA (Accelerated Linear Algebra)
is an open source compiler for machine learning. The
XLA compiler takes models from popular frameworks
such as PyTorch, TensorFlow, and JAX, and optimizes
the models for high-performance execution across
different hardware platforms including GPUs, CPUs,
and ML accelerators.
https://openxla.org/?hl=de

So Local AI will again change the landscape, and
it might be no joke that Python disappears. It
could be really the case that C++ becomes

more dominant. Not sure whats going on exactly.

Bye

Mild Shock schrieb:
> Hi,
> 
> I am already using this method for 20 years,
> just copied the Google Page Rank idea a couple
> of decades ago. Its described here:
> 
> We solve this equation exactly in that we
> calculate R = (E-L)-1*H. The matrix inversion
> (E-L)-1 is only computed once for the web site
> and is stored across the pages of the web site.
> May 14th, 2006 - Web Site Ranking
> https://www.herbrand.ai/izytab/doclet/home/03_support/01_browse/05_rank.html 
> 
> 
> While the matrix inversion was very primitive
> in the beginning. I use a couple of ideas to further
> develop it. From using sparsity to using tiles,
> 
> and doing it with multiple works, and worker
> queues. You find everything behind the scenes
> now, I did some explorations. Just image what
> 
> experience Google has and its TPUs to compute
> with matrices, their page rank was what made
> them the first attractive search engine, that
> 
> could provide information retrieval that made sense.
> 
> Bye
> 
> P.S.: Disclaimer, I don't say its possible so
> easily to replicate the new Gemini AI, by simply
> tapping into Local AI via AI Accelerators.
> 
> Its more to get a glimpse how the AI Effloreszenz
> could happen, did happen. I guess mostly it hapoened
> by not by getting obsessed with sequential algorithms
> 
> and all the Stony Brook nonsense, but by adopting a
> linear algebra view point, with very controlled
> doses of parallelism and of course the lock step
> 
> innovation in better hardware.
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Maybe a probem with the Logic Programming community
>> is the fact, that they are totally clueless about
>> linear algebra. Something tells me, we I could
>>
>> compute the transitive closure via matrix inversion:
>>
>> (I-M)^(-1) = I + M + M^2 + M^3 + ...
>>
>> I am pretty sure there are a few Lean or even Rocq
>> theorems already formalized, showing some of these
>> identities and their numerical perks.
>>
>> Still I find here long discussions (**), mareveling
>> how to compute the transitive closure, in a
>> sequential setting. But already when M is sparse
>>
>> things are pretty speedy with linear algebra. Matrices
>> are perfect for AI Accelerators that are specialized
>> for linear algebra, since it is one of the most
>>
>> parallelizable computations in numerical linear algebra.
>> GPU and distributed HPC performance is excellent,
>> but one has possibly to consider AI Accelerators nowadays
>>
>> on laptop and micro servers, for so called Local AI.
>>
>> Bye
>>
>> P.S.: (**)
>> Wanna see a bunch of clueless people associated to Stony Brook or not:
>> https://discourse.prolog-lang.org/t/subgraph-isomorphism-prolog-vs-conventional/173/7 
>>
>>
>> P.P.S.: I am currently looking into combinatorial search,
>> but transitive closure is of course also a candidate to
>> delegate to an AI accelerator when doing Local AI.
>>
>> Mild Shock schrieb:
>>> 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
>>>>
>>>
>>
> 

[toc] | [prev] | [next] | [standalone]

#641483 — When put in virtual jail, ask for removal of your content (Was: SWI Agent Provocateur gets kicked out of Rocq?)

Hi,

Most of the admins in these discourse forums, are
not aware that you have full control of your
content. At least EricGT didn't know that

deleting content is 100% valid. And that most
discourse forums, Rocq being no exception, have
a terms of service TOS, that reads as follows:

"Content you submit to the forum belongs to you,
and you decide what permission to give others for it.
But at a minimum, you license the company to provide
content that you submit to the forum to other users
of the forum.

That special license allows the company to copy,
publish, and analyze content you submit to the forum.
When content you submit is removed from the forum,
whether by you or by the company, the company’s special
license ends when the last copy disappears from the
company’s backups, caches, and other systems.

The company last updated these terms on July 12, 2018"
https://discourse.rocq-prover.org/tos

So as a retailation to a virtual jail attack, you
can ask complete removal of all content. My experience
most virtual jail actions are illegal, politically

motivated, because the product has flaws, and the
"community" has something to hide, it should
not be allowed to have virtual jails in forums.

But since its nevertheless exercised by Nazi Retard
administrators, in retailation you can ask
for complete removal of all of your posts,

as longs as the ToS have not been changed. So watch
the date of the ToS. Some meta discourse forums
have different ToS, but the usual "happy engagament"

forums have blindly copied the ToS, that allows more control.

Bye

Mild Shock schrieb:
> 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
>>
> 

[toc] | [prev] | [standalone]

Back to top | Article view | sci.math

csiph-web