| Age | Commit message (Collapse) | Author |
|---|
|
platform build.
|
|
build until we add suitable platform definitions/stubs.
The platform bits are not yet hooked into the model, but only into the build, so are untested.
|
|
|
|
|
|
resolving the difference in type parameters between the prompt and state
monads, and allowing a single output file to be used with either.
Normally, the type alias is to the prompt monad, but for HOL4 we use the
state monad.
|
|
In order to use up-to-date sequential CHERI model for test suite
|
|
|
|
|
|
sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount.
|
|
step function for execution.
|
|
|
|
|
|
Deactivate plugins of the datatype package except for the size plugin in order
to keep processing time reasonable. This is currently only needed for the big
AST datatypes, so we just patch this using a sed command.
|
|
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
|
|
|
|
Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings.
|
|
|
|
|
