Good afternoon!
I’d like to tell you about a major case of violation by the person with the nickname @5HT.
He hired me for type theory research and I worked successfully from 2018 to 2022 until February 28 he decided to break any relationship with me and kicked me out of the Groupoid organization where my projects were located.
A few days later, all my commits in that organization were no longer connected to my account.
@5HT said that this caused by ban in organization, but, very strangely, @forked-from-1kasper disappeared in contributors statistics (commits are still available, so it’s easily to check existence of my commits) in:
- https://github.com/groupoid/anders/graphs/contributors
- https://github.com/groupoid/homotopy.dev/graphs/contributors
- https://github.com/groupoid/ivy.mike/graphs/contributors,
but not in
- https://github.com/groupoid/principia/graphs/contributors
- https://github.com/groupoid/ground.zero/graphs/contributors
- https://github.com/groupoid/castle.bravo/graphs/contributors
- https://github.com/groupoid/hurricane/graphs/contributors
- https://github.com/groupoid/smiling.buddha/graphs/contributors
- https://github.com/groupoid/canopus/graphs/contributors.
After that, he twitted in his account @infinitystack:
https://twitter.com/infinitystack/status/1499341999039782913
(translation below, archived version)
that I’m not now considered as one of Anders author, but rather as his russian slave, because
- this work was paid
- @5HT has more commits in this repository
(And this is an easily verifiable manipulation, because his commits are mainly about library, *.anders files, of language, but not about language itself, i.e. *.ml files).
And recently, he removed me from LICENSE file without asking, which is an obvious violation of the license.
April 6 Update. Commit history from https://github.com/groupoid/anders/commits/main was removed. You may compare this repository with https://github.com/forked-from-1kasper/anders.
April 7 Update. He removed me from OPAM configuration file too: https://github.com/groupoid/anders/commit/024099a150aaff11b9f4c50748f9239d9141fb71.
Moreover, he deleted all authors of groupoid/CCHM (known earlier as groupoid/cubical).
April 8 Update. Commit history from https://github.com/groupoid/groupoid.space, https://github.com/groupoid/cubical.systems and (important) https://github.com/groupoid/CCHM was deleted.
June 17 Update. License in all projects from https://github.com/o89 was changed to his very strange non-free DHARMA license. It is very funny, because nothing in this repository works with new versions of Lean 4 (since transition to bundled LLVM/clang or maybe earlier).
Also look here, here, and here for more interesting comments from @5HT.
July 16 Update. Something strange happened: stars in groupoid/anders disappeared (last time I saw 82 stars there, but in archive there is only page with 84 stars from the 6th of June; two stars disappeared later). The same thing happened with forks, so it’s not very hard to find that they are now here. Such things usually happens when main repository was deleted: all forks become fork of some other fork of the deleted repository; but this could not happen now, because 1) redirect from forked-from-1kasper/tt (this is where groupoid/anders was created) is still alive, 2) there is still badge in my profile confirming that I created groupoid/anders, 3) there is nothing about that in Gitter (although I’m not sure that something should be in Gitter), 4) https://github.com/groupoid says that groupoid/anders was modified 21 days ago (if repository was recreated, there should be some other date). Maybe this could happen if repository was hidden and then opened from public, but I’m not sure about this too. It’s funny that @5HT in his profile unpinned groupoid/anders after this (it’s not very hard to verify that groupoid/anders was here earlier). This says a lot about what he is actually worried about.
In addition, https://anders.groupoid.space/ doesn’t work now. I don’t know how long it’s broken and whether it’s related to stars.
July 23 Update. https://anders.groupoid.space/ works again.
I did a little investigating, and found that this is not the first time that other people’s authorship has been erased by @5HT.
If you look at the code of the smiling.buddha project, you will quickly notice that a considerable part of this library is just a rearrangement (with some name changes and added comments) of the cubicaltt typechecker library examples, for example:
s1.ctt in cubicaltt library and circle.ctt in smiling.buddha
helix.ctt in cubicaltt library and helix.ctt in smiling.buddha
univ.ctt in cubicaltt library and univalence.ctt in smiling.buddha
This library contained some original code and I was curious to find out where it came from. (And it was pretty difficult.)
Originally there was a project called EXE, which @5HT hired several people to develop.
If we go to the repository of this project now, we find the only author is @5HT. Fortunately for us, there are many forks of this project left by which other authors can be identified.
https://github.com/silky/exe/graphs/contributors
The real, working code was written by zraffer, who was later erased from the authors, while @5HT mostly did a lot of trivia commits, giving comments and correcting typos.
Looking through the EXE forks, you will notice repositories named infinity share a common history. The list of infinity contributors includes a person with nickname nponnecop who, I know for a fact (full logs), wrote this code for money and whose major contribution has also been erased from history.
April 11 Update https://gist.github.com/forked-from-1kasper/06d241303cc314b35c291c38e61a5e0c?permalink_comment_id=4128741#gistcomment-4128741
There is a long list of repositories, with the loss of commit history and, the most important, authorship.
For example: in groupoid/pure, you can see from the commits how the authors of the project disappeared: Andy Melnikov, Paul Lyutko.
April 5 Update. https://github.com/groupoid/pure (or OM, or PTS) was renamed to Henk and recreacted as https://github.com/groupoid/henk/ without saving history; original repository moved to https://github.com/5HT/henk. After around a day history from https://github.com/5HT/henk was erased too (probably through delete + new), and history from https://github.com/groupoid/henk/ was erased again (i.e. a second time a day).
https://github.com/groupoid/homotopy was deleted, but you still can check and compare latest saved version with earlier forks listed below.
Other project, called homotopy (or HTS, or EXE), have 8 contributors, but there is only one, in credits section of README.md, and in commit history.
His favorite strategy is to change the names of the projects several times, merge and split the code again to make it harder to suspect him of stealing, so it is quite difficult to recognize the connection between his repositories.
I’m still investigating, and apparently this person’s entire career is based on hiring people and then appropriating their work, and in some cases directly stealing code from other projects without attribution.
In my opinion, the Github community shouldn’t tolerate people like @5HT.
Best wishes and hope for proceedings with this person.
Translation:
P.S. I also attach a (probably incomplete) list of forks of these repositories:
https://github.com/forked-from-1kasper/henk
https://github.com/forked-from-1kasper/homotopy
https://github.com/forked-from-1kasper/homotopy.dev
https://github.com/5HT/5HT
https://github.com/AlexZolcman/CCHM
https://github.com/5HT/tonpa.guru
https://github.com/adept/infinity
https://github.com/diasbruno/pts
https://github.com/DmytroMitin/infinity
https://github.com/e42s/exe
https://github.com/e42s/infinity
https://github.com/e42s/om
https://github.com/erlang-cn/hts
https://github.com/erlang-cn/pts
https://github.com/hardentoo/infinity
https://github.com/ilya-klyuchnikov/pure
https://github.com/jfrancese/cubical
https://github.com/k-haze-nil/om
https://github.com/knurdDongle/infinity
https://github.com/m-2k/exe
https://github.com/m-2k/om
https://github.com/mafm/pure
https://github.com/nau/om
https://github.com/nponeccop/hts
https://github.com/nponeccop/infinity
https://github.com/nponeccop/n2o.hs
https://github.com/nponeccop/om
https://github.com/py361/agda
https://github.com/pyzh/cubical
https://github.com/pyzh/infinity
https://github.com/pyzh/om
https://github.com/Randl/om
https://github.com/sam-mix/pts
https://github.com/silky/exe
https://github.com/spivakov/om
https://github.com/ulidtko/exe
https://github.com/xafizoff/agda
https://github.com/xafizoff/cubical
https://github.com/xafizoff/hcomp
https://github.com/xafizoff/om
https://github.com/yurrriq/exe
https://github.com/yurrriq/om
https://github.com/Zabrane/pure
https://github.com/zeitraffer/om
https://github.com/zaoqi-unsafe/exe
April 5 Update. List of renames and transfers:
https://github.com/groupoid/pure → https://github.com/5HT/henk + https://github.com/groupoid/henk
https://github.com/groupoid/homotopy deleted completely
https://github.com/groupoid/smiling.buddha → https://github.com/groupoid/CCHM
https://github.com/groupoid/principia → https://github.com/groupoid/bertrand
https://github.com/groupoid/castle.bravo → https://github.com/5HT/nicolas
https://github.com/groupoid/hurricane → https://github.com/groupoid/valery
https://github.com/groupoid/ivy.mike → https://github.com/5HT/ivy.mike
https://github.com/groupoid/canopus → https://github.com/5HT/canopus
April 6.
https://github.com/groupoid/ground.zero → https://github.com/5HT/ground.zero
https://github.com/groupoid/minitt → https://github.com/5HT/minitt
April 8.
https://github.com/5HT/hts-archive deleted
https://github.com/5HT/nicolas deleted (see https://github.com/forked-from-1kasper/bravo)
https://github.com/5HT/ivy.mike deleted (see https://github.com/forked-from-1kasper/ivy.mike)
https://github.com/5HT/canopus deleted (see https://github.com/forked-from-1kasper/canopus)
https://github.com/5HT/ground.zero deleted (see https://github.com/forked-from-1kasper/ground_zero)
https://github.com/groupoid/homotopy.dev deleted
https://github.com/groupoid/ant → https://github.com/5HT/ant
https://github.com/5HT/henk → https://github.com/groupoid/henk
April 14.
https://github.com/groupoid/bertrand → https://github.com/5HT/bertrand
https://github.com/groupoid/valery → https://github.com/5HT/valery
June 17.
https://github.com/5HT/bertrand deleted (see https://github.com/forked-from-1kasper/principia)
https://github.com/5HT/valery deleted (see https://github.com/forked-from-1kasper/hurricane)
https://github.com/5HT/minitt deleted
Just to clarify,
nponeccopand Andy Melnikov are the same person.I didn't work for money, instead I voluntarily sponsored a few months of Paul's work. I'm a humble and a relatively wealthy person, and all those details (who hired whom) were just unimportant for me back then. I saw this monetary contribution as voluntary token amount to motivate Paul, the late fact that both @5HT and Paul considered it salary came as a surprise to me.
As for "contributions being erased", both my and Paul's work were independent subprojects. Neither of us finished the respective subproject, so our contribution was in some sense "useless" and later @5HT deleted the code he didn't see as relevant anymore. Subsequently, he removed my name from the website, and I just didn't care.
During my work I extensively refactored the "standard library", and it's not clear whether my code is still there in the "upstream" repo of @5HT. Again, I just don't care. My code remains in my github fork and I can continue the work any time if I feel like it. My subproject was essentially a formalization of proofs in one paper, so at this point it's a completely different project from what @5HT does.