Gerwin Klein

Yes, that sounds eminently reasonable.

Hm, it's a bit more complicated than that. The current auto-deployments are: - seL4 auto-deploys to `devel.xml`. cpp-compatible updates are not recorded in `default.xml` - l4v auto-deploys to `default.xml` (based...

> Is it a deliberate choice to avoid cpp-compatible updates to default.xml? What's the rationale? (Not that it matters for this issue.) IIRC the original design was that any push...

> The libsel4 invocation stubs do not check the message info register at all, they just assume everything worked, so I'm not surprised it hasn't been noticed before. I do...

If we want to avoid boilerplate, we could even add a small command in ML that sets up the type definition and automatically derives the type classes.

I mostly meant the weekly should also keep testing the normal default. Not sure if we want to leave it at `16`, but `16` is as good as any I...

> Then you propose adding 1 and 2 to the weekly test? That makes sense. yes, that would have been much clearer :-) > - we need a branch with...

The fault handler is a regular user-level thread that can listen on the fault handler endpoint (which also is a regular endpoint, which can be set as a fault handler...

> Does this mean that no exceptions can occur in the kernel? Yes, no exceptions can occur in the kernel. > After switching to the user thread,what if an exception...

Given that gcc-11 is the current version, gcc-7 seems fairly far behind. There have been a lot of gcc releases in the last 3 years, so maybe it's not that...