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

@andrejbauer catamorphism ⇒ recursion scheme ⇒ computability ⇒ mathematics ⇒ philosophy of mathematics ⇒ philosophy ⇒ higher algebra, etc.

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

@niss looks like it yeah

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

Show older

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