Anne C. A. Baanen @Vierkantor@mastodon.vierkantor.com

An introductions post, since I've got a bunch of new followers in the last couple of weeks (hello everybody!)

By day, I do computer verification of #math in the Lean prover, by night I do #osdev. When there isn't a plague going around, I like #cycling in nature and befriending #crows. I also know a bit of #linguistics.

I really like explaining concepts — feel free to ask any question (esp. mathematics / theoretical comp sci). Replies to toots are always welcome.

ME, ONE YEAR AGO: this mexican party is good, but it has... how can one say ... too many people? there are in fact, only so many people one can dance with in the course of a party. I think I'm right in saying that, aren't I?

MY WIFE: this is absurd!

ME: my dear, don't take it too hard. it's quality celebrating. there are simply too many people. just remove a few, and it will be perfect.

MY WIFE: which few did you have in mind?

"smartphone" but with "smart" meaning "hurt" or "sting"

A couple of visiting jackdaws!

A crow today on the way to the supermarket. Five when I came back with a fresh bag of peanuts. They learn quickly 😊

Indeed, I happen to be the IUPAC nucleid acid notation for the codon of aspartic acid.

Here is it running (badly, with half of the features not working!) on real hardware:

Some more twiddling of bits in system registers later, and it seems everything works, finally! 🎉

(I suspect some system registers were not consistently being set when the machine powers up? e.g. some reserved-as-0 bits being set as 1. In any case, QEMU is much more forgiving of weirdness in the MMU, which is nice for setting expectations, not so nice for debugging wtf is going on when you're still bringing the system up.)

still some weirdness left though: only a few lines in the framebuffer are getting updated after switching to virtual memory.

disabling the MMU while updating the mapping seems to fix this issue 🎉

Or prog1 rock, or prog2 rock, or progv rock, or prog* rock, or multiple-value-prog1 rock?

If prog rock is so good, why isn't there progn rock?

hmm, `at s1e1r' indicates that some physical addresses are not being translated correctly. even though it is being translated correctly in QEMU. argh. time for bed.

after a couple of nights of trying, still can't figure out wtf i'm doing wrong when trying to enable virtual memory. I have read through the whole aarch64 and cortex-a72 docs on this subject, tried all combinations of TLBI + DMB + IC + ISB instructions that i can think of. it just seems like all read operations using virtual memory are returning 0 and all write operations are getting lost.

Did you know that a 1712 law against sorcery is still in force in England, making it illegal to fly? This is why British Airways force you to wear a seatbelt, as the restraint gives you the legal defence that you were being abducted rather than flying yourself.

the list destructor function, of type `list a -> (a × list a)', should obviously be called "ns"

"colimit cocones" should have been called "ne colimits".

She made HoTT coCoA.

It must be amazing to have such an optimistic view of people, like the guy who appeared on tv to propose "Why don't restaurants have 'safe days' on monday, wednesday and friday, and 'unsafe days' on tuesday, thursday and saturday? Let people choose for themselves how much risk they can handle."