v0.6.0

v0.6.0

v0.5.1

v0.5.1

v0.5.0

v0.5.0

v0.4.1

v0.4.1

v0.4.0

v0.4.0

v0.3.3

v0.3.3

Version 0.3.0

General enhancements

• The verification plan files generated by vehicle compile -t MarabouQueries command have been
  changed from verificationPlan.vcle to the more readable .vcl-plan.

• The proof cache files generated by vehicle verify command have been
  changed from X.vclp to the more readable .vcl-cache.

Command-line interface changes

• The command vehicle verify now requires you to point at the folder generated by the previous
  vehicle compile command, rather than the verification plan file within it, and therefore the
  parameter --verificationPlan has been changed to --queryFolder.

  i.e. an old command vehicle verify --verificationPlan=my/project/queries/verificationPlan.vcle now
  becomes vehicle verify --queryFolder=my/project/queries.

Language changes

• Added additional overload for division operator /. Dividing two Nats together now results in
  a Rat.

Bug fixes

• Fixed erroneous error message generated when giving inferable parameters an unsupported type.

• Fixed erroneous evaluation of when dividing two rationals together.

• Fixed bug where the compiler would sometimes hang when reading .vclo files created with an
  older version of Vehicle.

What's Changed

• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #469
• Fix erroneous inferable parameter error message by @MatthewDaggitt in #476
• Rename verification plan and proof cache files by @MatthewDaggitt in #477
• Add dogsHierarchy test by @MatthewDaggitt in #478
• Loss experiments by @ndslusarz in #463
• Bump black from 23.1.0 to 23.3.0 in /vehicle-python by @dependabot in #481
• Build wheels for Vehicle by @wenkokke in #482
• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #483
• Fix #486 and #485 by @wenkokke in #487
• Adds the BNFC-generated Pygments lexer to py-vehicle-lang by @wenkokke in #489
• Cache the results of Gaussian elimination to avoid re-solving the same equations repeatedly by @MatthewDaggitt in #490
• Bump tox from 4.4.8 to 4.4.11 in /py-vehicle-lang-tensorflow by @dependabot in #492
• Bump mypy from 1.1.1 to 1.2.0 in /py-vehicle-lang-tensorflow by @dependabot in #491
• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #493
• Overload division so that dividing two Nats make a Rat by @MatthewDaggitt in #494
• Add image of specification to README.md by @MatthewDaggitt in #496
• Build Marabou on CI by @MatthewDaggitt in #475
• Add support for './scripts/cabal-freeze all' by @wenkokke in #498
• Fix py-vehicle-lang's Setup.hs: Remove _external if it exists by @wenkokke in #499
• Fix broken link in README by @wenkokke in #500
• Add list of verifier backends to the docs by @wenkokke in #504
• Add Dockerfiles by @wenkokke in #501
• Bump tox from 4.4.11 to 4.4.12 in /py-vehicle-lang-tensorflow by @dependabot in #505
• Added three ACASXu networks to example folder by @MatthewDaggitt in #508
• Bump numpy from 1.24.2 to 1.24.3 in /py-vehicle-lang-tensorflow by @dependabot in #510
• Build all wheels using cibuildwheel by @wenkokke in #506
• Bump pypa/cibuildwheel from 2.12.1 to 2.12.3 by @dependabot in #509
• Decouple CI for py-vehicle-lang-tensorflow by @wenkokke in #516
• Use file-embed to embed standard library by @wenkokke in #518
• Implemented object file versioning and general versioning improvements by @MatthewDaggitt in #519
• Refactor Decl into DefAbstract and DefFunction by @MatthewDaggitt in #520
• Preparations for implementing @noinline in NBE by @MatthewDaggitt in #521
• Rename primitives in Python binding by @wenkokke in #524
• Remove dependency on recursion-schemes by @wenkokke in #525
• Update sphinx requirement from <7,>=6.1.3 to >=6.1.3,<8 in /docs-source by @dependabot in #522
• Replace normApp with smart App synonym by @wenkokke in #526
• Add beginning of integration test suite for Marabou by @MatthewDaggitt in #497
• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #529
• Fix bug in pygments distribution & include LaTeX minted sample by @wenkokke in #530

Full Changelog: v0.2.0...v0.3.0

Version 0.2.0

General enhancements

• Added support for building Vehicle with GHC 8.10, 9.2 and 9.4.

• Vehicle now generates interface files with the .vclo extension that cache
  the results of type-checking. If the interface file exists and the hash matches
  then it won't re-type check the original file.

• Drastically improved the performance of type-checking (e.g. AcasXu down from 20 seconds to 0.5 seconds).

• Drastically improved the performance of compilation to Marabou (e.g. mnist-robustness now takes 1.5 seconds per image as opposed to ~50 years!).

• Logs now print out in real-time instead of at the end of compilation.

• Improved error messages which involve type declarations. The messages now display
  both the original and the expanded form of the type.

• After verification, witnesses returned by the verifier are now translated and printed out.

Command-line interface changes

• Decoupled the compilation and verification of verifier queries in the command-line
  interface.
  The compile command will now generate a verificationPlan file that stores
  all the state needed to reconstruct the truth value of the original property from the query results.
  The verify command now has been altered to now take in the verificationPlan file and
  run it.
  The old behaviour of the verify command which performed both compilation
  and verification has been retained in the new compileAndVerify command.

• The existing check command has been renamed validate.

• The new check command now type-checks the specification.

• The verify command now prints out progress to the command line.

• Removed the --redirect-output and --redirect-error command line options from all modes.
  This functionality can be replicated via pipes.

Language changes

• Added Type to the frontend language for the type of types.

Bug fixes

• Fixed parsing error where unbound type arguments were being generalised over in the
  opposite order that they occur.

• Fixed parsing error when partially applying map or fold.

• Fixed typing error for map.

• Fixed typing error for higher-order function arguments without explicit annotations.

• Fixed typing error for let-bound expressions at the top-level scope of a declaration.

• Fixed problem with properties with no infinite quantifiers getting incorrectly
  negated when compiling to Marabou queries.

• Fixed problem where properties with forall .. in and ``exists .. in` were
  causing compilation to Marabou to get stuck.

What's Changed

• Some odds and ends to do with profiling and performance by @MatthewDaggitt in #241
• Fix #240 by switching let-expressions to use argument inference by @MatthewDaggitt in #242
• Reorganise meta-variable code in type-checker to make it more modular by @MatthewDaggitt in #243
• Speedup type-checking slightly by removing unneccessary meta substitution through meta-types by @MatthewDaggitt in #244
• Fix #246 by improving the error message for invalid property types by @MatthewDaggitt in #248
• Stop substituting metas through all constraints every pass by @MatthewDaggitt in #250
• Improve type-checking performance by removing substitutions through meta solutions by @MatthewDaggitt in #251
• Improve performance of type-checking by better guards for logging by @MatthewDaggitt in #252
• Python commandline3 by @Tgl70 in #254
• Fix dependabot for readthedocs by @wenkokke in #256
• Removed another unused normalisation option by @MatthewDaggitt in #258
• Fixes #253 #230 by improving setup documentation by @MatthewDaggitt in #259
• Fix #220 by documenting what happens when no proof cache is provided when exporting to Agda by @MatthewDaggitt in #261
• Check #102 is fixed by enabling disabled tests by @MatthewDaggitt in #263
• Fix bug where incorrectly negating quantifier-less expressions for Marabou by @MatthewDaggitt in #262
• Remove duplicate default extensions by @wenkokke in #267
• Steps towards packaging vehicle-python by @wenkokke in #255
• Support for GHC 9.2 by @wenkokke in #266
• Improve documentation - fixing bugs and adding detail by @MatthewDaggitt in #264
• Support Python 3.9 by @wenkokke in #271
• Set fail-fast: true by @wenkokke in #279
• Use full GHC versions by @wenkokke in #277
• Fix name for build-vehicle-python by @wenkokke in #280
• Fix DEFAULT_GHC_VERSION to use full version number by @wenkokke in #282
• Support GHC 9.4 by @wenkokke in #273
• Support Python 3.8 by @wenkokke in #275
• Multiple differentiable logics by @ndslusarz in #247
• Support Python 3.7 by @wenkokke in #276
• Fix #278 by moving BNFC specific code to vehicle-syntax package by @MatthewDaggitt in #284
• Removing Python 3.7 support: numpy dropped support by @wenkokke in #287
• Run cabal-fmt & stylish-haskell by @wenkokke in #286
• Update pyproject.toml by @wenkokke in #288
• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #283
• Remove old cabal.project files by @wenkokke in #289
• Network variable names refactor by @MatthewDaggitt in #290
• Added (very basic) module information to identifiers by @MatthewDaggitt in #292
• Remove ability to redirect stdout and stderr by @MatthewDaggitt in #296
• Fix #294 by introducing the concept of different logging backends by @MatthewDaggitt in #298
• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #297
• Add interface files to Vehicle by @MatthewDaggitt in #299
• Simplify provenance implementation and remove dependency on range package by @MatthewDaggitt in #304
• Remove the concept of property context by @MatthewDaggitt in #306
• Run stylish-haskell by @wenkokke in #309
• Change logging to reset terminal colors to defaults instead of to white by @wenkokke in #313
• Add ghc-debug instrumentation by @wenkokke in #310
• Add nothunks instrumentation by @wenkokke in #314
• Load empty standard library by @MatthewDaggitt in #308
• Fix #156 where higher-order functions wouldn't type-check by @MatthewDaggitt in #317
• Add library versioning and include imports at normalisation time by @MatthewDaggitt in #319
• Fix generalisation bug in scope checker and use stdlib function in normalisation by @MatthewDaggitt in #320
• Fix various problems with folds in type-checking and normalisation by @MatthewDaggitt in #323
• Fix CI: remove Tox, run Python 3.8.0 on Ubuntu 20.04 by @wenkokke in #327
• Refactor binders in grammar and delaboration in preparation for type-classes in user-code by @MatthewDaggitt in #325
• [pre-commit.ci] pre-commit autoupdate by @pre-commit-ci in #326
• Turn DB indices into a newtype by @MatthewDaggitt in #328
• Better handling of negation lowering, including error messages by @MatthewDaggitt in #329
• Convert AST to be strict and derive instances of NoThunks by @wenkokke in #315
• Switch to ormolu by @wenkokke in #330
• Add HasMap type class by @MatthewDaggitt in #332
• Fix tests by @wenkokke in #334
• Migrate strictness annotations to use of StrictData and add benchmarks by @wenkokke in #335
• Refactoring printing to use Contextualised to eliminate duplicate strategies by @MatthewDaggitt in #337
• Fix performance regression by @wenkokke in https://github.com/vehicle-la...

Version 0.1.0

First initial release so that we can target tutorials at.