Okay, so the function keys for adjusting keyboard backlight and screen brightness don't work out of the box, but I'm sure I can fix that tomorrow.

Show thread

I did it! I figured out how to get Linux to work reliably on a laptop:
1. Buy a big name laptop
2. Wait 7 years
3. Install the Linux of the future on your old laptop

Seriously i just installed Linux Mint Debian Edition on a 2015 MacBook air and everything just works, including suspend/resume the Broadcom wireless!

One of my favorite surprises when purchasing a used book is getting a paperback that a library had laminated before removing it from their collection. Best of paperback and hardcover: sturdy and durable but still flexible and relatively light

Ah, I am now trying out a new font for my book...

Show thread

Well I submitted a draft to arXiv at 8am, and even though literally all I did was upload and click submit (the draft itself was done last week) apparently my brain has decided that's the only productive thing I need to do today. It will probably change its mind at 10pm.

uspol, surveillance advertising 

wtf did I click on to make some ML model serve me *this* bullshit ad? On the Washington Post of all places.

Thanks to @barik I'm going to have the Duck Tales theme song from my childhood running through my head all day

I love to see an academic publisher show how much they "value [my] privacy" by working with their partners to "use precise geolocation data and identification through device scanning."

academia, public speaking 

love to give a talk in the first main session of ICSE after the keynote and spend half my talk resolving screen sharing issues that didn't exist in testing the same setup 20 minutes before the talk 😛

re: academic beancounting bs 

To be clear, I don't actually care about the data itself, I'm not going to use or publicize this profile to "Showcase Your Expertise and Increase Readership of [My] Research." I'm just miffed by (a) another showing of the (central) ACM organization failing to pay even minimal attention to even simple things that are obviously broken, and (b) the fact that they apparently signed on with this company that is basically selling a way to spy on who reads your papers, clearly without ever consulting actual ACM members.

Show thread

re: academic beancounting bs 

Oh, actually, they only emailed me about the SIGPLAN Notices version, but actually *both* versions are listed. The OOPSLA version is listed with no publication data at all, just published by the ACM in 2016 in a Journal/Book with no name. The ACM has the name, and is working with Kudos, but apparently nobody tested that conference names carry over, because why would the main professional org for a field that publishes primarily in conferences... check that conference titles transfer when they partner with a company trying to boost "scholarly impact"?

Show thread

academic beancounting bs 

So ACM has auto-registered my "recent" (2016) paper with Kudos, listing it as published in SIGPLAN Notices rather than in its actual publication venue, OOPSLA (compounding the fact that every SIGPLAN pub pre-PACMPL has two DOIs, one for where it was actually published and one for the SIGPLAN Notices hack to get Elsevier to count SIGPLAN pubs in journal metrics). There is no way for me to correct the publication's listing.

parenting 

My son has figured out how to have Spotify kids repeat the same individual song infinitely. Send help

I used Rust to implement the reference interpreter for my compilers class last term, and now I have to keep suppressing the urge to rewrite random pieces of software in Rust.

Is there a name for the general construction where given some algebra A, you lift it's structure pointwise to functions into A, e.g. if A is a Heyting algebra then functions B -> A are also a Heyting algebra? Performing this transformation has apparently become my primary job function (doing this with 3 different algebras in 3 different projects) so surely it has an actual *name* that is more concise than "the general construction where..." Right?

Colin boosted

announcement (boosts appreciated) 

We're delighted to announce the HoTTEST Summer School, which will take place online everywhere in the world during the months of July and August 2022.

The school will run both synchronously and asynchronously. The lectures will be delivered live (between 2:30-4pm UTC) and paired with various tutorial sessions run by teaching assistants. The course will also feature a discord-based all-hours Q&A and an online archive of all course materials so that participants can follow along on their own schedule.

This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory. Our goal is to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.

Read more: groups.google.com/g/homotopyty
Join the Discord: discord.gg/tkhJ9zCGs9

re: linux hardware support 

For a second I thought it actually auto-configured my network printer! But no, it can see the printer, but it can't actually send a print job with any of the recommended printer drivers 😛

Show thread

linux hardware support 

Another Linux install, another half-day of searching for the magic command invocation that will fix my monitor resolution for my particular combination of distro + graphics card + monitor + cable...

My monitor supports 2560x1440 but apparently my DisplayPort-to-HDMI adapter doesn't support that resolution at 60Hz, so Linux doesn't find the resolution at all. But apparently you can force it to try lower refresh rates, and *that* works with my cable *facepalm*. I have to say, after 20-something years of this, I'm kind of over it.

This toot brought to you by ```cvt -r 2560 1440``` generating the magic modeline for xrandr

Show older
types.pl

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