sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2020-01-28	Use external PPrint	Thomas Bauereiss

2019-01-03	Comment out bisect coverage in ocamlbuild files	Alasdair Armstrong

2018-12-26	Add makefile target for building with Bisect coverage	Alasdair Armstrong

2018-04-26	Make ocamlbuild assume lem is in path instead of relative to current directory.	Robert Norton

2018-03-02	Use sail_lib.lem values in C backend	Alasdair Armstrong
	Rather than just using strings to represent literals, now use value types from sail_lib.lem to represent them. This allows for expressions to be evaluated at compile time, which will be useful for future optimisations involving constant folding and propagation, and allows the intermediate bytecode to be interpreted using the same lem builtins that the shallow embedding uses. To get this to work I had to tweak the build process slightly to allow ml files to import lem files from gen_lib/. Hopefully this doesn't break anything!
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