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.
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!
Ah, I am now trying out a new font for my book...
Thanks to @barik I'm going to have the Duck Tales theme song from my childhood running through my head all day
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.
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"?
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.
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?
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: https://groups.google.com/g/homotopytypetheory/c/Ir2joc7imyI
Join the Discord: https://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 😛
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
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.