March 29, 2021 1:51 PM, "Ben Fiedler"
I'm having troubles generating the CAmkES glue component specification and proofs from our source. I can and have successfully generated the ADL/CDL spec and implementations using the documented CMake parameters.
Grepping around the docs I've found references to a 'camkes.sh' script, but neither the project tree nor the files generated during build contain it.
Digging around reveals commit 21becfa909595f0ba204b7fafef9e3629e8627c7 [1] in camkes-tool to be a potential culprit. Even though the camkes.sh script was removed long before, it seems that this commit removed support for the --platform argument and shifted to a more CMake-focused build (and the documentation was not updated - it still mentions the --platform argument). In the course of this, the cimp-base.thy template was orphaned and is not referenced anymore (at least according to grep). I think I can hack some CAmkESGen expression together that instantiates the cimp-base.thy template, but I'm still not entirely clear where/how the user-provided UserStubs.thy theory comes into play, or what to specify in it. Any help is still greatly appreciated! [1]: https://github.com/seL4/camkes-tool/commit/21becfa909595f0ba204b7fafef9e3629...