Skip to content

Release 2.0.0

Latest
Compare
Choose a tag to compare
@phiwuu phiwuu released this 09 Sep 14:11
· 19 commits to main since this release

This new major release includes a number of incompatible
changes. These have been tagged in the changelog.

  • [Incompatible, TRLC, LRM, API] New major version as all deprecated
    features have been removed:

    • The deprecated builtin function syntax trlc:foo has been
      removed. You should now use foo instead.

    • Support for check files has been removed. You can simply move any
      checks into the rsl file.

    • API support surrounding check files in the Source_Manager has been
      removed.

  • [Incompatible, TRLC, LRM, API] The LRM had rules that names need to
    be sufficiently distinct, for example having Foo, foo or Fo_o
    in the same namespace would not be allowed. This was previously not
    implemented at all.

    The rules have been strengthened to apply to all names (packages,
    types, literals, objects) and are now enforced. This is also a
    backwards incompatible change as it may invalidate some previously
    valid .trlc or .rsl files.

  • [TRLC] The --verify command is now supported on Windows without
    the use of an external cvc5 install, now that the Python package
    for CVC5 is also available on Windows.

  • [TRLC, LRM] New builtin function oneof. This can be used to test
    if precisely one of a number of parameters is true. For example:

  • [TRLC] The warning about late package declarations is no longer
    issued.

  • [TRLC] New command-line flag -I which can be used to register
    include directories. You can use this to automatically parse a
    minimal set of file. Normally when invoking eg trlc foo.trlc this
    will fail, because you did not provide e.g. foo.rsl.

    With the -I flag you can now automatically let the tool discover
    any dependencies. When using e.g. trlc -I . foo.trlc the tool will
    discover it also needs foo.rsl and maybe potato.rsl which you
    imported in foo.trlc.

    Especially in large projects this will be much faster than
    explicitly parsing everything.

  • [API] The source manager has a new function
    register_include
    which should be used before any register_file or register_dir
    calls.

  • [API] When using includes, the symbol table will contains packages
    for every discovered package. These are indistinguisable from normal
    (but empty) packages, so if you're relying on iterating over all
    known packages you will find a lot of unused and empty ones now. If
    the include mechanism is not used, then there is no change in
    behaviour.

  • [TRLC] Various performance improvements when parsing large files.

  • [TRLC] Add --version flag that can be used to figure out the
    installed TRLC version.

  • [TRLC] Fix bug when creating a lexer with an empty file with
    delivered file content. The lexer attempted to open the file instead
    of using the empty string passed to the constructor.

  • [TRLC] Fix a bug in the verifier mistranslating existential
    quantifiers. This could both lead to false alarms and missed bugs.

  • [TRLC] Fix a bug parsing record references of incorrect types,
    instead of an ICE we now create an error message.