m4lvin · HackerTrans

16 giorni fadiscuss

How about these? - rate limit overall messages, maybe even percentage wise: if some ip sent more than 70% of all messages in the last minute, mute it. - let other users mark/report spam and if three others agree something is spam, block all slightly similar messages for 24 hours? - forbid sending the exact same message more than N times per M seconds. - rate limit color change and jump much more.

m4lvin

mese scorsodiscuss

Expected Lean 4, the programming language and proof assistant, but got the management philosophy ;-)

m4lvin

2 mesi fadiscuss

As Wikipedia says, "some official plugins proprietary". So "can be" is doing a lot of work in that sentence. I would at most compare it to saying that VS Code is open-source.

m4lvin

3 mesi fadiscuss

Okay, but how do I use this as a replacement when the mic is not working on Linux?

m4lvin

2 anni fadiscuss

I think one reason for the web interface is that the device stays usable. If it would export a block device then it would need to unmount the file system on itself or at least block changes. If I remember correctly in the old days before MTP, all Android did this, making storage on the device itself unavailable while making it available via USB.

m4lvin

2 anni fadiscuss

The trick is that the human only needs to read and understand the Lean statement of a theorem and agree that it (with all involved definitions) indeed represents the original mathematical statement, but not the proof. Because that the proof is indeed proving the statement is what Lean checks. We do not need to trust the LLM in any way.

So would I accept a proof made by GPT or whatever? Yes. But not a (re)definition.

The analogy for programming is that if someone manages to write a function with a certain input and output types, and the compiler accepts it, then we do know that indeed someone managed to write a function of that type. Of course we have no idea about the behaviour, but statements/theorems are types, not values :-)

m4lvin

2 anni fadiscuss

pass is the best.

If your phone is android, I'd recommend https://passwordstore.app/ plus syncthing :-)

m4lvin

2 anni fadiscuss

Thanks for making me look up rerere which I first thought would be a typo but actually seems like a really useful thing :-)

https://git-scm.com/book/en/v2/Git-Tools-Rerere

m4lvin

2 anni fadiscuss

For anyone looking for a free alternative that works without google play services: https://f-droid.org/packages/de.nulide.findmydevice/

m4lvin

4 anni fadiscuss

Funny coincidence. Yesterday I watched the talk by SPJ about Lenses and it finally clicked for me :-)

https://skillsmatter.com/skillscasts/4251-lenses-composition...

Maybe someone has an actual public link to this with no login needed?

edit: thanks for the subcomment! https://www.youtube.com/watch?v=k-QwBL9Dia0

m4lvin

5 anni fadiscuss

I have my own XMPP server ;-) and I understand the underlying problem here. I mostly wanted to point out that for a new person to quickly try out Movim this might be a stumbling block. As another comment suggested using something like OAuth to smooth this out might help.

m4lvin

5 anni fadiscuss

I wanted to try it out, but this is annoying:

- registration happens on https://api.movim.eu/register and firefox provides me a way to generate a password and save it linked to that domain.

- now I want to log in at https://mov.im/?login but firefox has no idea that it should use my api.movim.eu account for that.

comments