- Output global and local types in a protobuf format so that they can be used programmatically elsewhere.
- sedlex is now used for lexing, for future Unicode support.
- Improved pretty printing of global and local types.
- Improved error message for merge errors by including the role name.
- BREAKING: Scribble-style "module" and "type" declarations were parsed into an AST but remain unused, now they are rejected and become parse errors.
- New ways to convert global/local types into LaTeX macros, using mpstmacros
- Improve documentation for some modules
scr_module
is now an abstract type, whose definition is not exposed- File name will not be reported in error messages if there is none
- JavaScript files in the web version are now minified
- Improve the list of examples in the web version
- Fix a panic when duplicate recursion variable exists
- Stacktraces is printed correctly when
NUSCRDEBUG
orDEBUG
env variable is set - Error is raised gracefully when an unbound role is found in the expansion of
an
do
block
- A new module
LiteratureSyntax
where global and local type constructors that similar to those used in literature (without extensions) are provided for the convenience of developers. - New command line options to output global and local types in the format of mpstk.
- Following a change in cmdliner, user errors will result in an error code of 124 instead of 1
- Improved documentation
- Fixed an issue that breaks parser generation with menhir
- Unguarded recursions should be correctly reported as errors
- A new pragma system for extensions:
(*# PRAGMA #*)
at the beginning of the input file can enable theory extensions. - Nested Protocol extension, via
NestedProtocols
pragma (by Benito Echarren Serrano) - Refinement Type extension, via
RefinementTypes
pragma (by Fangyi Zhou)
- New, improved command line interface with cmdliner
- Reorganise code layout
- Recursions immediately after a choice is permitted under some circumstances
- Non-distinct choice prefixes now raise an error
- Degenerate recursions in protocols will be removed
- Catch an uncaught exception when user enters a non-existent protocol from CLI
- Merging [end] and [\mu t.t] after projection is now possible
- Export code generation APIs in Lib
- Modernised Web Interface
- Change signature of
generate_fsm
in Lib - Annotate signature of
project_role
,generate_fsm
with names - Update ppxlib dependency version
- Remove js_of_ocaml dependencies
- Fix usage in executable
- Fix non-monadic code generation
Initial Release