Release 2.0.0

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.

Release 1.2.2

1.2.2

• [API] Add callbacks to the Source_Manager to notify clients of the parse progress.

Release 1.2.1

1.2.1

• New minor version release due to minor API changes and major command-line changes.

• When using --verify you can now also specify a CVC5 executable using --use-cvc5-binary. This allows you to use the --verify option on platforms where there is no CVC5 PyPI package (i.e. Windows or more recent versions of OSX).

• The PyVCG package is now required on all platforms. The optional dependency is now CVC5 instead.

• Remove the --lint option. Lint messages are now enabled by default, and .trlc files are processed as well. Instead there is a --no-lint option which turns off the extra warnings.

• Add the --skip-trlc-files option which disables processing of .trlc files. Enabling this option is equivalent to the old --lint mode.

• Add the --error-on-warnings option which generates a status code of 1 if any warning is raised.

• We now always print a short summary, indicating how many files were processed and how many messages were generated. The
  --show-file-list option still exists and still prints the complete list of files. This summary may be suppressed with the --brief option.

• The Source_Manager has new and different constructor flags, although it can still be constructed with no parameters.

• The Message_Handler now uses an enumeration instead of a string to signal message severity/kind. For normal use this is transparent, but if you subclass the message handler then you need to deal with this. The category (for lint messages) is now also a separate parameter instead of being baked into the message.

• Please note that if you parse messages in CI, the regex has changed slightly.

• Fix an issue where --skip-trlc-files would incorrectly register and parse the preamble of .trlc files.

• Fix a spurious space in the summary output.

• Fix support for Python 3.11. The package can now be installed without issues.

• Fix issue in VCG where the matches function could be generated more than once. This was only an issue in the debug output and was not visible to users.

Release 1.1.10

1.1.10

• [TRLC] Fix missing typechecks for numeric subtypes on value
  assignments. It was possible to assign an integer to a decimal
  component, or the other way around. This now correctly generates an
  error.

• [TRLC, LRM] You can now also write """foo""" string literals. Just
  like the ''' strings, these can contain newlines.

• [TRLC, LRM] User defined checks are now not allowed to contain a
  newline. However you can now provide additional information that
  can contain a newline. For example:

  checks Requirement {
    top_level == true or derived_from != null,
      error "linkage incorrect",
      """You must either link this requirement to other requirements
         using the derived_from attribute, or you need to set
         top_level to true."""
  }
  

  Would now produce something like this:

  Requirement Potato {
              ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect
                   | You must either link this requirement to other requirements
                   | using the derived_from attribute, or you need to set
                   | top_level to true.
  

  For more details please
  refer to the LRM.

Release 1.1.9

1.1.9

• [TRLC] Add support for Python 3.11. We now support Python 3.8 up to
  and including 3.11.

• [TRLC] Add new option --no-detailed-info which supresses the
  additional information the linter may add to a message, such as
  counter-examples or reasoning.

• [TRLC] The tool is now much less likely to abort on parse errors,
  instead we continue where it's possible to generate more errors in
  other unrelated packages and declarations. This may occasionally
  generate follow-on errors that look weird, however once you fix the
  earlier errors things should work out.

• [TRLC] Add new option --no-error-recovery which restores the old
  behaviour w.r.t. error handling. With this option, every error you
  see is absolutely a real error which you need to fix; but of course
  there could be more errors once you fix them.

• [LRM] Mark .check files as a deprecated feature. You should move
  your checks into the corresponding .rsl file. The linter also
  complains about these now.

Release 1.1.8

1.1.8

• [TRLC] Hotfix for the CVC5 API issue: pinning PyVCG to 1.0.3, which
  in turn pins CVC5 to 1.0.5 (the last known good version).

Release 1.1.7

1.1.7

• [TRLC, LRM] Fixed a missing restriction on tuple types that
  permitted interesting nesting of tuples with separators and optional
  components. The restriction forbids any tuple with declared
  separators from having components that are themselves tuples with
  separators. We may relax this restriction in the future to permit
  some combinations where this doesn't lead to parsing problems for
  values.

  The problem can be seen in this example:

  tuple T {
     a String
     separator @
     b optional Integer
  }
  
  tuple Q {
     a T
     separator @
     b optional Integer
  }
  

  If we now write "foo" @ 12 then there is no possible way to
  specify if you meant:

  • Instance of Q where a is "foo" @ 12 and b is unspecified
  • Instance of Q where a is just "foo" and b is 12

• [TRLC, LRM] Fixed LRM and tools allowing empty enumerations. This is
  now explicitly forbidden. It was always unreasonable to do this as
  it would have been impossible to use the enumeration type, and there
  is no legitimate use-case anyway since you cannot add more literals
  later through e.g. a type extension.

• [TRLC] Add alternative entry-point for users who cannot modify their
  PATH. You can now do python3 -m trlc [args...] and it works just
  like trlc [args...].

• [TRLC] Fix tool crash when encountering a file not in UTF-8
  encoding. We now print an error message indicating the issue.

• [TRLC] Fix bug when parsing arrays: arrays without comma separators
  were accapted when they should have been rejected.

• [TRLC] Fix tool crash when parsing a file with an unterminated /*
  comment.

• [LRM] Fix typo in in several places: .rls should be .rsl.

Release 1.1.6

1.1.6

• [TRLC] Add new option --lint --verify. This option requires
  PyVCG to be installed (which is
  only available on GNU/Linux or OSX). This option attempts to
  statically verify all checks for freedom of run-time errors (no null
  dereferences, no division by zero, and no array out of bounds
  access). For example with this .rsl:

  type T1 {
    x optional Integer
    y optional Integer
    z          Integer
  }
  
  checks T1 {
    x != null implies y == x, fatal "potato"
    y != null implies x > 1, warning "potato"
  }
  

  The --lint --verify option might say:

  y != null implies x > 1, warning "potato"
                    ^ test1.rsl:11: warning: expression could be null [vcg-evaluation-of-null]
                    | example record_type triggering error:
                    |   T1 bad_potato {
                    |     /* x is null */
                    |     y = 0
                    |     z = 0
                    |   }
  

• [Package] Provide Linux and OSX packages, along with the default
  package, which should automatically install PyVCG where it is
  available. On Windows, pip should fall back to the platform
  agnostic package.

• [TRLC] Add new option --no-user-warnings to suppress any warning
  generated from a user-defined check.

• [TRLC] Fix missing static check on exponents (they must not be
  negative).

• [TRLC] Fix missing static check for Boolean types on check
  expressions (tools would crash without error message).

• [TRLC, LRM] Fix several tool crashes when the null literal
  appeared in expressions outside equality. Re-worded the section on
  null values in the LRM to be much stricter. We consider this to be a
  bug-fix and not a change of semantics.

• [LRM] Clarify equality semantics for arrays, tuples, and record
  references. Moved the definition of null equality into the same
  place.

Release 1.1.5

1.1.5

• [LRM, TRLC] Remove limitation on late packages. You may now declare
  any number of packages in trlc files; and you may even import
  them. It is still recommended to have a rsl file for a package
  spanning multiple files, even if it's basically blank; however the
  technical limitation and language rules surrounding late packages
  have been removed.

• [LRM, TRLC] Add base 2 and base 16 integer literals. You can now
  write things like 0xdeadbeef and 0b10010010. Octal literals are
  not supported.

• [LRM, TRLC] Add support for readability separators in integer and
  decimal literals. You can now write things like 1_000_000.00 or
  0b1001_0010.

• [TRLC] Improve --lint output by appending a rule name in the output
  (in a style similar to clang-tidy). In the future it will be
  possible to turn rules off you don't like.

• [TRLC] Relax errors surrounding array sizes, they are now lint
  messages like the language manual suggests.

• [TRLC] A warning is now issued by the tools when encountering a
  duplicate import statement.

• [TRLC] A warning is now issued by the tools when encountering
  duplicate late package declarations.

• [TRLC] New --lint check for detecting tuples with separators that
  could be confused with base 2 or base 16 integer literals.

Release 1.1.4

1.1.4

• [TRLC] Improve error messages by using a more human readable form of
  expected tokens, so now you see "opening brace '{'" instead of
  "C_BRA".