sail-riscv
sail-riscv copied to clipboard
riscv
Questions on `riscv-ast-raw.txt`
What is the purpose of generated_definitions/ast/riscv-ast-raw.txt and how is it generated?
It's a dump of the Sail internal AST. Not sure why it's there - could be for some RMEM deep embedding experiment. It's from 5 years ago when we were first building the model, and weren't being particularly careful with what we checked in.
As to how it was generated - not sure we still have the code set up to do it, but the Sail internal AST is specified as an Ott grammar, and Ott can (or could) dump the contents of that in a format that is basically a big OCaml literal.
We should probably remove it.
Should we remove the entire prover_snapshots directory? Or move it to another repo at least?
Yes, those snapshots are seriously out-of-date. Ideally we'd have the CI generate some and when it fails only spam the people who might fix it, but currently they probably won't build without updates to the handwritten bits anyway. (Which I might try and sort out quite soon.)
I'll close this since Alasdair removed the riscv-ast-raw.txt. Maybe I'll remove the whole directory at some point... (or if someone else wants to feel free!)