sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-03-14	WIP Latex formatting	Alasdair Armstrong
	Added option -latex that outputs input to a latex document. Added doc comments that can be attached to certain AST nodes - right now just valspecs and function clauses, e.g. /! Documentation for main / val main : unit -> unit These comments are kept by the sail pretty printer, and used when generating latex
2018-02-17	Merge master branch into sail2 for OCaml 4.06 compatibility	Thomas Bauereiss

2018-02-07	Have exceptions working in C backend	Alasdair Armstrong

2017-12-16	compatibility with OCaml 4.06.0;	Shaked Flur
	imported new version of PPrint (20171003)
2017-12-13	Cleanup code by fixing compiler warnings, and fix ocaml compilation	Alasdair Armstrong
	Add the ast.sed script we need to build sail. Currently we just need this to fix up the locations in the AST but it will be removed once we can share locations between ocaml and lem.
2017-12-05	Update header files on master	Alasdair Armstrong

2017-12-05	Update license headers for Sail source	Alasdair Armstrong

2017-10-06	Various improvements to menhir parser, and performance improvments for Z3 calls	Alasdair Armstrong
	New option -memo_z3 memoizes calls to the Z3 solver, and saves these results between calls to sail. This greatly increases the performance of sail when re-checking large specifications by about an order of magnitude. For example: time sail -no_effects prelude.sail aarch64_no_vector.sail real 0m4.391s user 0m0.856s sys 0m0.464s After running with -memo_z3 once, running again gives: time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail real 0m0.457s user 0m0.448s sys 0m0.008s Both the old and the new parser should now have better error messages where the location of the parse error is displayed visually in the error message and highlighted.
2017-09-13	Fixed code display in error messages that span multiple lines	Alasdair Armstrong

2017-09-13	Work on improving Sail error messages	Alasdair Armstrong
	- Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases
2017-08-04	Various improvements for ASL generation	Alasdair Armstrong
	Fixed a bug where existential constraint's weren't used to solve function quantifiers correctly
2017-02-03	fix headers	Peter Sewell

2016-06-20	Fix error in type checker that put some constraints wrongly into conditional ↵	Kathy Gray
	constraints, breaking power. Also improve reporting of contract constraints, but then turn them off :( to allow power to compile.
2016-01-26	move closer to power.sail -> power.ml output	Kathy Gray

2014-04-02	Solve more constraints; fix up test suite bugs uncovered by solving more ↵	Kathy Gray
	constraints. Clean up Lem output a little for readability while debugging.
2013-08-08	More forms converting from parse_ast to ast; also removed some annot aux ↵	Kathy Gray
	homs for terms that only need locations and not full annotations
2013-08-01	Lex and discard comments	Gabriel Kerneis

2013-07-31	Revert "Remove the wrong reporting basic"	Gabriel Kerneis
	This reverts commit b0efdb7172e65707cceab0eff469584217b8b589.
2013-07-31	Remove the wrong reporting basic	Kathy Gray

2013-07-31	Adding the real reporting basic	Kathy Gray