Skip to content

v0.3.5

Latest
Latest

Choose a tag to compare

View all tags
@maximebuyse maximebuyse released this 02 Oct 12:35
· 300 commits to main since this release
hax-lib-v0.3.5
bf9a7e4
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Changes to the Rust Engine:

  • The module names now produces ExplicitDefIds instead of DefIds (#1648)
  • Add a resugaring FunctionsToConstants (#1559)
  • Drop the tuple nodes of the AST, add resugaring node for tuples (#1662)
  • Add support for enums and structs to the Lean backend (type definitions,
    expressions, pattern-matching) (#1623)
  • Update name rendering infrastructure in the Lean backend (#1623, #1624)
  • Printers now emit proper diagnostics (PR #1669)
  • Global identifiers are now interned (#1689)
  • Global identifiers are encapsulated properly, and provide easy destructuring as tuple identifiers (#1693)
  • Add support for trait and impl in the Lean backend (#1679): trait definitions, trait bounds
    on functions, impl definitions. The typeclass resolution in the generated code is left implicit
    (relies on Lean). Limited support for associated types. No support for default implementations.

Changes to the frontend:

  • Add an explicit Self: Trait clause to trait methods and consts (#1559)
  • Fix ImplExpr::Builtin that had some type errors (#1559)
  • Improve the translation of Drop information (#1559)
  • Add variance information to type parameters (#1559)
  • Cleanup the State infrastructure a little bit (#1559)
  • Add information about the metadata to use in unsize coercions (#1559)
  • Resolve dyn Trait predicates (#1559)
  • Many improvements to FullDef (#1559)
  • Add infrastructure to get a monomorphized FullDef; this is used in charon to monomorphize a crate graph (#1559)
  • Fix a regression affecting projection predicates (#1678)

Change to cargo-hax:

  • Improve the caching of rustc when using cargo hax commands (#1719)
  • Add hidden commands and flags to explicitly manipulate haxmeta files (#1722)

Changes to hax-lib:

  • New behavior for hax_lib::include: it now forces inclusion when in contradiction with -i flag.
  • hax-lib requires edition 2021 instead of 2024 (#1726)
  • Improved VecDeque model in F* proof lib (#1728)

Changes to the Lean backend:

  • Improve support for functionalized loops (#1695)

Miscellaneous:

  • A lean tutorial has been added to the hax website (#1626)
  • Add end-to-end tests for the website (#1690)
  • Diagnostics reporting were improved (#1692)
Assets 2
Loading