Pinned toot

Every boolean in the Agda codebase can actually be one of True, False, or An internal error has occurred. Please report this as a bug.

6:30 to go. my spaghetti has come back to bite me in the ass (already). i am stopping for lunch now

Show thread

Playing Factorio with the anxiety indicator (Oh no I'm behind schedule)

what i should be doing: opaque/unfolding

what my brain wants to be doing: factorio no spoon planning

need to file my taxes but my head hurts so much i'm pretty sure if i try to do it today i'm just gonna spontaneously combust

so instead of doing that i'm gonna sleep instead

it's far too hot for me to do anything other than complain about the weather, it seems

herculean, heroic, other h-adjectives that mean of daunting size and commanding respect for having been undertaken

Show thread

after yesterday's scare i'm back on the grind. today: getting the annotated printing PR mergeable and merging @totbwf's herculean rewrite of everything co/limit for the 1lab

We're going home now that she's been doing better for a couple hours

Show thread

doctor seems to think it's just dietary which is gonna be really "funny" when her bp is 21 over 16 again

Show thread

I'm doing some anxiety scrolling and wow. [gestures at everything], huh?

Show thread

Had to accompany my mum to the hospital so pretty-printing can take the L on this one

(She's stable)

Not gonna look at my github notifs on Sunday

CVE-2023-21036 / acropalypse is absolutely bonkers.

Apparently for 5+ years the cropping / editing tools for screenshots on Google Pixel phones was only overwriting the start of the screenshot PNG file, but not truncating.

All screenshots shared for the past 5+ years might have data recoverable from them. Demo available at

Google still hasn't communicated anything on this.

(h/t ItsSimonTime on Musk's site)

Agda developer me and Agda user me are sometimes at odds in funny ways

Agda developer me: Not using the provided built-in modules is unsupported

Agda user me: [doesn't use those, code breaks literally every other commit]

Why do I do this to myself?

i even did a thing yesterday! a minor refactor, but a thing nonetheless!

Show thread
Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.