Gerwin Klein

> Is this waiting for verification before this can be merged? Yes, that's correct.

I assume the glossary us based off the one we have in the [abstract spec](https://github.com/seL4/l4v/blob/master/spec/abstract/Glossary_Doc.thy)? I haven't looked through everything yet, but I'd like to before we merge it. It'd...

> What are the criteria for adding an entry and where are the descriptions coming from? > > E.g. do we want to limit it to seL4 specific things, or...

There still seem to be some capitalisation changes in the same commit that adds the glossary and an accidentally committed file `q` in there. @bbrcknl are you happy for me...

> > the glossary doesn't have a chapter number, but the bibliography coming after the glossary does, which looks weird in the TOC. If someone knows how to give it...

Yes, that's fine, these connectivity issues seem to be popping up a lot lately.

You're right, this does not make much sense for `max`. If it is really a `max`, it should be the end of a page, not the beginning of a page....

Nice find, and I'm glad that the assert catches it, because that would have been super hard to find at runtime. The value in `config.py` is just wrong, it needs...

The preprocess failure is fine from the verification side. Just to double-check, though, since this is in non-verified code: is the rest of the kernel code fine with a half-precision...

It seems to me that the only bit missing here is updating the commit message. @chrisguikema are you happy to do that?