All Versions
Latest Version
Avg Release Cycle
211 days
Latest Release
382 days ago

Changelog History
Page 1

  • v8.4.3-final

    March 19, 2019

    Final version built with GHC 8.4.3

  • v8.2.1-final

    March 19, 2019


  • v0.8.4.0

    • 👌 Support for GHC 8.4.3
    • Significant restructuring of Bare front-end to shrink dependency on GHC-API
  • v0.8.2.2

    December 28, 2017
    • 👌 Support for GHC 8.2.2

    • 👌 Support for GADTs and TypeFamilies, see

      • tests/{pos,neg}/ExactGADT*.hs
    • ➕ Add support for Bags/Multisets, see

      • tests/pos/bag.hs
      • tests/neg/bag.hs
      • tests/pos/ListISort-bag.hs
    • Add support for inductive predicates see

      • tests/pos/IndEven.hs
      • tests/pos/IndPerm.hs
      • tests/pos/IndStar.hs
  • v0.8.0.1

    July 20, 2017
    • 👌 Support for GHC 8.0.2
  • v0.7.0.1

    • DELETED the gsDcons and generally carrying DataConP beyond Bare; this may cause problems with target as I removed the dconEnv field in TargetState. Is it live? To restore: have to apply the substitution syms/su in Bare.hs ALSO to gsDconsP (after restoring the gsDconsP field to [(DataCon, DataConP)])

    • 💥 breaking change Remove the Bool vs. Prop distinction. This means that:

      • signatures that use(d) Prop as a type, e.g. foo :: Int -> Prop should just be foo :: Int -> Bool.
      • refinements that use(d) Prop v e.g. isNull :: xs:[a] -> {v:Bool | Prop v <=> len xs > 0} should just be isNull :: xs:[a] -> {v:Bool | v <=> len xs > 0}.
    • ➕ Add --eliminate={none, some, all}. Here

      • none means don't use eliminate at all, use qualifiers everywhere (old-style)
      • some which is the DEFAULT -- means eliminate all the non-cut variables
      • all means eliminate where you can, and solve cut variables to True.
    • Change --higherorder so that it uses only the qualifiers obtained from type aliases (e.g. type Nat = {v:Int | ... }) and nothing else. This requires eliminate=some.

    • ➕ Add a --json flag that runs in quiet mode where all output is suppressed and only the list of errors is returned as a JSON object to be consumed by an editor.

    • ➕ Add --checks flag (formerly --binders), which checks a given binder's definition, assuming specified types for all callees (but inferring types for callees without signatures.)

    • ➕ Add --time-binds which is like the above, but checks all binders in a module and prints out time taken for each.

  • v0.6.0.1

    July 20, 2017
  • v0.6.0.0

    April 05, 2016
  • v0.5.0.1

    • 🛠 Fixed a bug in the specification for Data.Traversable.sequence
    • 0️⃣ Make interpreted mul and div the default, when solver = z3
    • 👉 Use --higherorder to allow higher order binders into the fixpoint environment
  • v0.5.0.0

    • ➕ Added support for building with stack

    • ➕ Added support for GHC 7.10 (in addition to 7.8)

    • ➕ Added '--cabaldir' option that will automatically find a .cabal file in the ancestor path from which the target file belongs, and then add the relevant source and dependencies to the paths searched for by LiquidHaskell.

    This means we don't have to manually do -i src etc. when checking large projects, which can be tedious e.g. within emacs.