summaryrefslogtreecommitdiff
path: root/src/process_file.ml
AgeCommit message (Expand)Author
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-07Add a symbol for new implicit arguments for backwards compatabilityAlasdair Armstrong
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
2019-02-06Improve emacs modeAlasdair Armstrong
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2018-12-26More cleanupAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-20Make sure sail -v prints useful version infoAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Jenkins: Fix deprecation warningsAlasdair Armstrong
2018-09-06Allow options to be set in the interactive modeAlasdair Armstrong
2018-09-04Improve error messages for include and ifdef statementsAlasdair Armstrong
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-07Revert "Warnings: deal with all the deprecation warnings"Alasdair Armstrong
2018-07-26Warnings: deal with all the deprecation warningsAlastair Reid
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-06-29Constant folding improvementsAlasdair
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-18more riscv mappings; riscv now builds successfully to lem which builds to isa...Jon French
2018-05-17Remove sequential code againBrian Campbell
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-03Work in progress on the coq backendBrian Campbell
2018-05-01tidyJon French
2018-05-01Use a naming scheme rather than random fresh ids for union anonymous recordsJon French
2018-05-01Add anonymous record arms to unionsJon French
2018-04-26Add a new SHARE_DIR argument to use when doing opam build. For non-opam build...Robert Norton
2018-04-26Opam packaging: add install and uninstall targets and code to find various fi...Robert Norton
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-04-04Use solver properly to simplify nexps in mono analysis, Lem printingBrian Campbell
2018-04-04Initial rewrite to move complex nexps in fn sigs into constraintsBrian Campbell
2018-02-27Get MIPS translated to LemThomas Bauereiss
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss