Hello,

I would like to use the sel4.xml API description files to generate custom bindings for a prototype language to interact directly with seL4 without going through libsel4 C API.

I assume that the structure of these files could change, which I'm willing to accept, but wanted to know if these files are here to stay in the future? I understand also that I will still have to parse libsel4 C headers to recover the full API which I'm fine with too.

Do you see any trouble following this approach or would you recommend something else?

Hi, (sorry for the laggy response). There is a wish to represent the libsel4 API in a language agnostic format to make generating bindings for other languages easier but at the moment it isn't being actively worked on. Currently the parts of the API that are generated from language agnostic formats are the invocation and syscall bindings from the *.xml files and some data type definitions that are generated from *.bf (bitfield) files. The bitfield language is used to generate bitfield struct access methods in C as well as automatically generating some of the Isabelle theory scripts relating to the C methods.

In the future, the .xml files could get replaced with a more domain specific interface language format but it is likely that that transition would happen after more of the C definitions get converted to either .xml or .bf formats first.

I'm not sure whether you would want to manually translate all of the non-xml definitions or also try and generate them. The definitions that change the most across build configurations are already likely to be in a .xml representation as that was the motivation for adding the .xml representation in the first place.

As for staying up to date with any changes, this discussion page (https://sel4.discourse.group/t/procedural-generation-of-the-sel4-api/24) will likely get updated with any changes. Also feel free to weigh in on the discussion there too.