Lmao, why is that not a link:
Here on types, I can make a longer post, rather than a tiny thread, about the headline changes:
⏩ A ton of performance improvements, which total to a ~30% improvement over 188.8.131.52 in time spent for the standard library;
🧊 Erased Cubical Agda, which marks all marks all Cubical Agda definitions (primitives and imports from other --cubical modules) as @0, quantity-0. The upshot is that you can reason about your programs using cubical machinery (funext!
HITs! univalence!), but nothing cubical "survives to runtime" — because unlike plain Cubical Agda, Erased Cubical can be compiled, using any of our backends (Haskell, JS) or agda2hs.
🇰 For a while during 2.6.3's development,
--without-K also meant "generate support code for Cubical Agda". This was widely regarded as a bad move and made a lot of people very unhappy, so we rolled it back: Your
--without-K code will no
longer suffer from cubical breakouts, and especially no longer enjoy surprise hcomps in error messages. The trade-off is that, if you want your modules to be usable from Cubical Agda (
--cubical), you need to use the new
--cubical-compatible flag. Since
--cubical-compatible does a ton extra (required!) internal work, modules using it will generally take longer to check, and generate larger interfaces files than, the same modules
⚠️ Note that
--without-K should accept the exact same programs; This means you could develop against
--without-K, then change to
--cubical-compatible for release, for example. If you find something that one
accepts and the other rejects, please do file a bug report! On GitHub. Not on my DMs.
🪞 Reflection can now generate data types, as long as you pre-declare the names of the type and all the constructors, using the
defineData primitives, together with the
unquoteDecl data syntactic form. These even work for
inductive-recursive and inductive-inductive definitions!
🙏 A massive thanks to everyone who contributed to this release. Git tells me that, since the last tag, these lovely folks authored commits on the master branch:
Moisés Ackerman, Andrej Bauer, Jacques Carette, Evan Cavallo, Felix Cherubini, Jonathan Coates, Lucas Escot, Robert Estelle, Alexandre Esteves, Naïm Favier, Sean Gloumeau, Oleg Grenrus, Marcin Grzybowski, Matthias Hutzler, Tom Jack, Andre Knispel, Thomas Lamiaux, Shea Levy, Viktor Lin, Vladimir Lopatin, Sandy Maguire, James Martin, Orestis Melkonian, Fredrik Nordvall Forsberg, Andreas Nuyts, Kyle Raftogianis, Prabhakar Ragde, Christian Sattler, Peter Selinger, Artem Shinkarov, Mike Shulman, Alissa Tung, Andrea Vezzosi, Szumi Xie, Tesla Zhang, Fangyi Zhou; Favonia, lawcho, Maštarija, oskeri, person-with-a-username, Riccardo, tensorknower69, and thorimur.
Some of them are here on Fedi, but I don't want to bother them all with pings, so I won't.
🧑💻 Our tireless main developers (🤓❤️) also deserve a great big round of applause, not only for finishing the release, but for all they do for the language,
especially since most have real jobs, too!
Andreas Abel, Guillaume Allais, Nils Anders Danielsson, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Ulf Norell, and Andrés Sicard-Ramírez.
If you want to get involved, please reach out! We always welcome pull requests and issue reports, be them to Agda itself, the Emacs mode, both their documentations, the standard, cubical, and categories libraries. We promise nobody will get
bitten for submitting a pull request 🙂
#Agda 2.6.3 has (finally) been released! Get yours now at https://hackage.haskell.org/package/Agda-2.6.3/changelog and get a complimentary performance boost to your Agda code FOR FREE!
Android is a nice operating system, but the apps are a shit show. No wait, I wish they were a complete shit show, because then I would adjust my expectations accordingly. It's death by a thousand paper cuts.
I've more or less internalised by now, what the Android "Back" action does in most apps, but my god is it jarring when I get it wrong.
For most of the apps I use that have tabs —Tusky, Facebook, Instagram, Gmail, Messenger, Spotify— the back action takes you back to the first tab of the app when you're on a different one.
The Fitbit app just closes the app. Bye bye. This made me look around and apparently it's not even consistent among Google apps. In Photos, Back closes the app. In the Play Store, you go Back to the first tab.
This has got to be the least well defined abstraction of all time.
Citizens! *Puts on steel toed boots* I urge you to remain calm at this moment! *loads rubber bullets into launcher* violence is not the answer! *Hangs night stick from belt* We grieve with your community! *Pulls reflective visor down on helmet* Peace is what this moment calls for *climbs into tank* The great MLK Jr said and I quote: I love police, and they are our friends! *diesel engine roars* So obey, comply, and remember we are in this together! *Tear gas launcher slowly points towards crowd*
Here's a subtle way Google broke their keyboard recently. I swiped the word "Hello", putting the keyboard in a state where the next press or swipe automatically adds a space.
However, they did not reset the shift button, which falsely appears to be active. If I press "S", it inputs a space and a lowercase "s". If I press the shift button first, it deactivates and I still get a space and a lowercase "s". I need to press shift twice to actually get an uppercase "S".
This used to work. (As a workaround, swiping a proper noun usually autocapitalises it, but still)
PhD student. Leftist. Trans.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.