Gerwin Klein

I would say yes, that would be great. Whatever is needed or would help someone get started who has not much background in any of these.

@pingerino it looks like there are docs for this now on https://docs.sel4.systems/Tutorials/camkes-vm-linux.html Can the PR be closed?

> @lsf37 this was specifically for creating the guest linux image. I can't see that in the tutorial? Right, I confused the guest image with the VMM. Sorry about the...

Interesting, we should look into that. I don't recall the details on how the pages are generated, but I thought it was the same source as the manual. IIRC, the...

Just to clarify, merging everything into one page is not what I was after. The point was more to have a single page with the most important information when you...

> Looks good to me (assuming that the `Word_Lib` failure is trivial)! It should be, I moved the lemma manually without checking dependencies, and that's what I get for my...

The Word_Lib failure has drawn in a whole slate of word lemma movement from CRefine, so it's probably worth looking at this again before I merge.

> I'm confused by the remaining failures but assuming that it's mostly unrelated then it still looks good to me. They were because the seL4 PR was not rebased yet...

Excellent write-up, thank you! One variation I thought of when reading through it -- probably not worth it, but I wanted to record it anyway just so we can decide...

> With the V/E 2, you still need to resolve the issue of storing an extra expression along with a variable to use for bounds checking in lieu of its...