Skip to content

0.8.1

Compare
Choose a tag to compare
@Gbury Gbury released this 10 Feb 16:10
· 89 commits to master since this release

CHANGES:

UI

  • Fix handling of size/time limits on windows (PR#117)
  • Fix spurious printing of backtraces (PR#118)
  • Add release binaries for windows

LSP

  • Add option for the lsp to read preludes before checking
    each file (PR#116)
  • The LSP now sends an empty list of diagnostics upon closing
    a file (PR#116)

Parsing

  • Fix a bug related to alt-ergos function definition, which
    were previously alwyas non-recursive. Now, alt-ergo's function
    definitions are always recursive (PR#123)
  • Add parse_raw_lazy to parse a string into a lazy list of
    statements (PR#125)
  • Add support for mutually recursive functions and predicates
    in Alt-ergo's native language (PR#129)

Typing

  • Properly add binding locations for implicit type variables
    (PR#123)
  • Ensure that type of recursively defined symbols are freshened
    to avoid type variables sharing between declaration and
    definition (PR#123)

Loop

  • Use GC.finalise instead of Gc.finalise_last in loop/parser.ml
    in order to avoid a bug in the ocaml 5.0 runtime, see ocaml/ocaml#12001
    (PR#128)
  • New module to implement Alarms (size/time limits) (PR#117)
  • Add optional argument to Pipeline.run to specify
    an alarm implementation (PR#117)
  • Add a bt key to the state to record whether we should print
    backtraces (PR#118)
  • Use parse_raw_lazy to parse raw contents in full mode if/when
    necessary (PR#125)