#introductions
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?
#osdev
Here is it running (badly, with half of the features not working!) on real hardware:
#osdev
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.)
#osdev
still some weirdness left though: only a few lines in the framebuffer are getting updated after switching to virtual memory.
Or prog1 rock, or prog2 rock, or progv rock, or prog* rock, or multiple-value-prog1 rock?
#osdev
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.
#osdev
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.
re: bad category theory puns
the list destructor function, of type `list a -> (a × list a)', should obviously be called "ns"
covid, nlpol
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."
/'ɑ.nə/ & legally certified as they who must become Master & (intuitionistic) maths / programming & pronouns: they/them (or best offer) & trains, crows and sheep & as seen in children's magazine