Pinned toot

✨ 𝓲𝓽 𝓲𝓼 𝓪𝓵𝔀𝓪𝔂𝓼 𝓪𝓵𝓵 𝓽𝓱𝓮 𝓽𝔂𝓹𝓮𝓼 ✨

Pinned toot

"Computers are rocks we tricked into thinking" is entirely incorrect. Computers are rocks we tricked ourselves into believing they could think

jonoodle boosted

typles search is still busted so i'm just gonna remake toot's

why mushrooms so expensive...

I'm sitting in the back of the classroom and I can literally see everyone's open laptop screen and now I'm realizing when I used to sit in row 3 everyone else behind me could see when I was checking twitter

Cha Cha Cha is last in semifinal 1 which is fantastic omg. Everyone's gonna remember it and it's gonna qualify I know it is

Eurovision semifinals running orders are out

taking the backseat on a project is so nice. I don't need to think about design decisions or understand the entire type system as a whole, just enough to go chug chug chug on the coq proofs until it's all green

HELP I think it timed out

eauto make laptop fans go brrrrr

I'm slowly but surely learning the ways of Coq

ok nope. I just checked with a hex editor and it's as compact as possible. 17156 px is the limit

a 17157 px square GIF is 200017 bytes, so if 17 bytes could be shoven from the image...

in case anyone was wondering, the largest possible GIF you can create using GNU IMP under 200 KB is 17156 px by 17156 px. I'm sure you can shave off a few bytes though because there's a lot of blocks in the GIF spec you can just delete without consequence, and sometimes the animation looping block gets included even if it's not an animation. the total size is 199 988 bytes

I believe the limit is 4096 px but I have no idea where to check this

Mastodon::DimensionsValidationError (17150x17150 images are not supported):app/models/concerns/attachmentable.rb:58:in check_image_dimension'app/models/concerns/attachmentable.rb:29:in block in has_attached_file'app/controllers/admin/custom_emojis_controller.rb:21:in create'app/controllers/concerns/localized.rb:11:in set_locale'lib/mastodon/rack_middleware.rb:9:in call'`

yeah that's valid

if I could remember where the logs are

500 Internal Server Error

I wonder what the server logs say

GNU IMP warning me about creating an image of size 2.1 GB. dw about it, this is fine

looks like it's actually 200 KB... that's exactly 200 000 bytes I guess
I could do some calculations taking into account how LZP encoding works but I think I'll just binary search by saving a bunch of squares through GNU IMP lol

Show older

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