Asta Halkjær From @ahfrom@types.pl

this is a real sentence uttered by a real cryptographer

time to post again the best user interface i've ever seen

ANN: #Agda 2.6.3 is out today! 🐔🎉
Get yours here: https://hackage.haskell.org/package/Agda

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 2.6.2.2 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 --without-K.

⚠️ Note that --cubical-compatible and --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 declareData and 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 🙂

As Gregor Samsa awoke one morning from uneasy dreams, he found himself rewritten in Rust for performance reasons.

#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!

is anyone aware of an account/bot on here that posts pictures of crabs? I used to follow a couple on birdsite but they don't appear to have migrated, and I miss my daily dose of sideways scuttling.

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*

The Onion never misses

never change, the onion, never change

#Accessibility is cool.
I had wondered about the change, but never checked.
Excellent work by @FinancialTimes

#DigitalComms #Communications #Screenreader #Screenreaders #TextToVoice