Martin Berger

> We would like to implement a versioning string Hello Allen, where do you want the version strings to be, in each .sail file, or once, somewhere in the top-level...

How about we have a top-level file `VERSION.md` in `master` that contains as first line the git tag for the release?

> something embedded in the binary itself. Which binaries have you got in mind?

How do you suggest that version be extracted from binaries, by grepping or something like a `--version` command line switch?

That's fine. Does Sail offer a reliable facility to drop this kind of information into all it's backends (OCaml, C, HOL ...) or would this have to be done on...

@jrtc27 Sounds all very reasonable, I'm happy to have such an addition. Now we 'only' need to agree on the exact naming scheme. I have no particular preferences. It sounds...

Sail currently compiles to the following provers: - HOL4 https://github.com/HOL-Theorem-Prover/HOL - Isabelle/HOL https://isabelle.in.tum.de/ - Coq https://coq.inria.fr/ They are interactive provers. I imagine you want to prove equivalence between individual functions...

@PeterSewell Does Isla handle unrestricted recursion?

Bill wants to prove equivalence of two full models ... One of the interns I had last summer had some Sail code that was naturally expressed using recursion and wanted...

I think there is a lot of recursion 'under the hood' in the infinite precision arithmetic and other helpers, that handled by C, Coq etc, depending on backend.