| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-11 | Ocaml semantics can now run aarch64 hello world example using octapod | Alasdair Armstrong | |
| New testcase for bitfield syntax Updated to work with latest lem and linksem | |||
| 2018-01-05 | Moved parser, lexer and pretty printer to correct locations. | Alasdair Armstrong | |
| 2017-12-13 | Merge remote-tracking branch 'origin/master' into interactive | Alasdair Armstrong | |
| 2017-12-13 | find zarith using ocamlfind instead of using the one in ocaml-lib which is ↵ | Shaked Flur | |
| no longer there | |||
| 2017-12-11 | Prototype interactive mode for sail. | Alasdair Armstrong | |
| Requires linenoise library (opam install linenoise) for readline support. Use 'make isail' to build sail with interactive support. Plain 'make sail' should work as before with no additional dependencies. Use 'sail -i <commands>' to run sail interactively, e.g. sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail then try some commands for typechecking and evaluation sail> :t main sail> main () Doesn't use the lem interpreter right now, instead has a small operational semantics in src/interpreter.ml, but this is not very complete and will be changed/removed. | |||
| 2017-12-05 | Update header files on master | Alasdair Armstrong | |
| 2017-12-05 | Update license headers for Sail source | Alasdair Armstrong | |
| 2017-08-11 | Menhir for new parser, ocamlyacc for old | Brian Campbell | |
| 2017-02-03 | fix headers | Peter Sewell | |
| 2016-01-20 | trim some obsolete/bitrotted make stuff. | Robert Norton | |
| 2015-11-10 | Update tag for register write in nested lexp | Kathy Gray | |
| Also starting to try to get elf compiling for sequential interpreter | |||
| 2015-04-08 | makefile changes to keep up with lem ocaml-lib changes | Kathy Gray | |
| 2014-08-24 | Use LEM_DIR environment variable if defined | Gabriel Kerneis | |
| LEM_DIR must contain the *absolute* path the Lem directory. If not defined, the previous behaviour is retained: a relative path is used, assuming Lem is in bitbucket/lem. | |||
| 2014-08-21 | Allow command line interface to exhaustively evaluate the next step, ↵ | Kathy Gray | |
| printing the events. Note: this commit switches back to a standard lem build located in ~/bitbucket/lem/lem | |||
| 2014-08-20 | Add ability to track register dependencies in interactive stepper; thus ↵ | Kathy Gray | |
| testing register tracking/tainting | |||
| 2014-08-13 | Silence some lem warnings in compilation. | Kathy Gray | |
| 2014-08-13 | Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵ | Peter Sewell | |
| temporarily use other version of Lem | |||
| 2014-05-12 | OCamlbuild magic to use PPrint | Gabriel Kerneis | |
| 2014-04-23 | Rename main to sail, build pretty_printer lib | Gabriel Kerneis | |
| 2014-04-02 | Skip constraint resolution to build Power model | Gabriel Kerneis | |
| 2013-11-07 | Port L2 to new Lem | Gabriel Kerneis | |
| Tests compile and run properly. There is a lot of hackery going on to workaround the rough edges of new Lem. Use at your own risk (you need the "library-format" branch of lem). | |||
| 2013-11-07 | Stub for external calls | Gabriel Kerneis | |
| 2013-10-10 | Use ocamlbuild, no findlib required | Gabriel Kerneis | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |