What is Hackers' Pub?

Hackers' Pub is a place for software engineers to share their knowledge and experience with each other. It's also an ActivityPub-enabled social network, so you can follow your favorite hackers in the fediverse and get their latest posts in your feed.

wakest ⁂ @liaizon@social.wake.st
Public
Shared by wakest ⁂

RE: autonomous.zone/@twilight/1162

Hey lovely fediverse friends, as many of you might know, I help run some fediverse instances and I am currently paying way way too much money out of my own pocket because mastodon and mastohost have an awful habit of caching way too much and not giving good user accessible tools to prune away unneeded cruft. I could really use some community help supporting the instances I am currently paying for. Already in the process of figuring out how to move to a new server this month...

0
1
0
0
0
0
0
0
0
0
0
0
0
0
0
1
0
0
0
0
0
0
0
0
0
3
0
0
0
0
0
0
0
Yudderick & Co. @yudderick@toot.cat
Public
Shared by Cat 🐈🥗 (D.Burch) :paw:⁠:paw:

Petunia is my neediest cat. During the day she likes to sit off somewhere nearby and just cry over and over until she gets whatever inexpressible thing that she wants. Does she want to play? Does she want to be tucked in? Does she want to be cuddled? Is she just generally discontent?

Lately she's been spending the nights with me, and while it's sweet when she wants to cuddle, she frequently decides that she needs something. Instead of just sitting on my desk and crying at me, during the night she scratches the blankets and pillow around me, and sometimes just scratches at my face. Too bad she's too adorable to get mad at :blobcatcry:

A photo of a brown tabby cat on her side on a grey blanket, with a black ribbon snared in her claws and her mouth wide open as she prepares to bite it.A photo of a brown tabby cat on her side on a grey blanket with her mouth open and a black ribbon caught on her lower teeth as she stares into the camera.
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
1
0
0
0
9
0
0
0
0
0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. arxiv.org/abs/2603.10936v1

arXiv logo

A Formalization of Abstract Rewriting in Agda

We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus.

arxiv.org · arXiv.org

0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. afm.episciences.org/17678

Duality theory in linear optimization and its extensions -- formally verified

Vladimir Kolmogorov · Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".

afm.episciences.org · Episciences

0
0
0
Glyph @glyph@mastodon.social
Public

More generally I am deeply suspicious of any thinking which is rooted in, "I, with my high intellect, sophisticated approach to problems, and vaguely exceptional vibe, am inherently superior to others and thus more capable of avoiding a risk while engaging in the same activity". The people most vulnerable to propaganda are those who believe they are too smart to fall for it, and it stands to reason that those who *believe* that they can use AI well are also at risk for pathological outcomes.

0
0
0
Bumble @bumble@ibe.social
Public

Hi

I'm trying to help a friend out with his Mastodon instance. An upgrade went badly wrong and mastodon would not restart.

We've rebuilt the server using backups and the server is up and running. It is federating. However no one can login.

If I enable debugging log i get the following for a log attempt in the system logs

Errno::ECONNREFUSED (Connection refused - connect(2) for 127.0.0.1:389):
Mar 14 18:47:50 debian-s2-2 bundle[13675]: [0e4f20e2-6069-47ee-8678-e4db5247e075]
Mar 14 18:47:50 debian-s2-2 bundle[13675]: [0e4f20e2-6069-47ee-8678-e4db5247e075] app/models/concerns/user/ldap_authenticable.rb:11:in 'User::LdapAuthenticable::ClassMethods#authenticate_with_ldap'
Mar 14 18:47:50 debian-s2-2 bundle[13675]: [0e4f20e2-6069-47ee-8678-e4db5247e075] app/controllers/auth/sessions_controller.rb:69:in 'Auth::SessionsController#find_user_from_params'
Mar 14 18:47:50 debian-s2-2 bundle[13675]: [0e4f20e2-6069-47ee-8678-e4db5247e075] app/controllers/auth/sessions_controller.rb:62:in 'Auth::SessionsController#find_user'
Mar 14 18:47:50 debian-s2-2 bundle[13675]: [0e4f20e2-6069-47ee-8678-e4db5247e075] app/controllers/concerns/auth/two_factor_authentication_concern.rb:12:in 'Auth::TwoFactorAuthenticationConcern#two_factor_enabled?'
Mar 14 18:47:50 debian-s2-2 bundle[13675]: [0e4f20e2-6069-47ee-8678-e4db5247e075] lib/mastodon/middleware/socket_cleanup.rb:11:in 'Mastodon::Middleware::SocketCleanup#call'

API calls are working. Just the Web logins that are failing.

Any help much appreciated

0
1
0
Alex R :heart_progress: @alex@tech.lgbt
Public

'Oh, he's not normally like that', you say, as your red-eyed miniature hellhound attempts to take a chunk out of my ankles in a manner that suggests he is, in fact, deeply accustomed to the taste of human flesh

0
0
0
José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

A formalization of Borel determinacy in Lean. ~ Sven Manthe. afm.episciences.org/17712

A formalization of Borel determinacy in Lean

Sven Manthe · We present a formalization of Borel determinacy in the Lean 4 theorem prover. The formalization includes a definition of Gale-Stewart games and a proof of Martin's theorem stating that Borel games are determined. The proof closely follows Martin's "A purely inductive proof of Borel determinacy".

afm.episciences.org · Episciences

0
0
0
0
0
0
0
0
0
0
0
0
Misty @misty@digipres.club
Public

You might remember from my IGF list I was talking about the wildly experimental language game Kevin's Playing in Berlin. Well, it's out now! You owe yourself to look at this. store.steampowered.com/app/398

kevin's PLAYING in berlin on Steam

Release the author, who is nothing but the player. Release the player, and restore the freedom once taken away. A three-game experiment in what it means to play.

store.steampowered.com

0
0
0
0
0
0
0
0
0
0
7
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
Evan Hahn @EvanHahn@bigshoulders.city
Public

"human.json is a protocol for humans to assert authorship of their site content and vouch for the humanity of others. It uses URL ownership as identity, and trust propagates through a crawlable web of vouches between sites." I've added it to my website! codeberg.org/robida/human.json

Summary card of repository robida/human.json, described as: A lightweight protocol for humans to assert authorship of their website content and vouch for the humanity of others.

human.json

A lightweight protocol for humans to assert authorship of their website content and vouch for the humanity of others.

codeberg.org · Codeberg.org

0
2
1
0
0
0
Electronic Frontier Foundation @eff@mastodon.social
Public

When lawmakers and advocacy groups frame queer existence itself as a threat to young people, age-verification laws become ideological enforcement instead of regulatory policy. eff.org/deeplinks/2026/03/rep-

Rep. Finke Was Right: Age-Gating Isn’t About Kids, It’s About Control

What’s at stake is whether “protecting children” becomes a legal pretext for embedding government control over the internet to enforce specific moral and religious judgments—judgments that deny marginalized people access to speech, community, history, and truth—into law.

www.eff.org · Electronic Frontier Foundation

0
1
0
0
0
0