rework kernel/generated/arch/object/structures_gen.h to allow including it about sel4_libs HOT 2 OPEN

Are you talking about just the enum cap_tag part? It's hard because user level isn't supposed to be able to query type information about a cap. Maybe we could look at how seL4_DebugCapIdentify is defined and change it to return the same information, but not directly tied to the internal seL4 enum values.

from sel4_libs.

Seems to me that is the usual trade off between debug features and release code. In Debug mode you want to be able to have some insights and thus need some headers or definitions that are not meant to be really public. Wouldn't it be possible that things like the enum cap_tag" are simply put into a separate header file that has no includes? Then this header file can be included in debug builds by libsel4debug and thus become available to others indirectly when they include libsel4debug? No other module would then have a direct dependency here, all such "debug hacks" are well constained in libsel4debug.
After all, what is the real point on hiding some technical details that one desperately want for debugging and low level development purposes? If information is duplicated in hard coded magic numbers, I consider it even worse. That tends to end in a pitfall if something changes - because you never really notice this until things start behaving very strangely.

from sel4_libs.