Skip to content

CHANGELOG_NEXT.md

Latest commit

 

History

History
109 lines (91 loc) · 4.69 KB

CHANGELOG_NEXT.md

File metadata and controls

109 lines (91 loc) · 4.69 KB

Changelog Next

This CHANGELOG describes the merged but unreleased changes. Please see CHANGELOG for changes to all previously released versions of Idris2, as well as the sub-headings typically used for changes. All new PRs should target this file (CHANGELOG_NEXT).

[Next version]

Documentation

  • Various changes to user documentation both the frontend and backend, as generated by ReadTheDocs and located in doc.

    • Migrated sphinx python project to uv for better project management.

    • Adopted sphinx extension myst-parser to enable documentation to be provided using Markdown, specifically the MyST dialect.

    • Adopted, but not activated, inclusion of sphinx-contrib.bibtex to provide better support for citing in documentation.

    • Adopted a new sphinx theme called sphinx_book_theme, which provides a HTML theme with a more 'modern' look & feel. For example, more indepth navigation, revised responsive mode (when compared to ReadTheDocs), and light & dark modes.

Compiler changes

  • Fixed missing handling of dotted patterns See #3669, comment.
  • Removed modules and functions moved to base:
    • Libraries.Data.Fin → Data.Fin
    • Libraries.Data.IOArray → Data.IOArray
    • Libraries.Data.List.Extra.minimum → Data.List.minimum
    • Libraries.Data.List.Lazy → Data.List.Lazy
    • Libraries.Data.List.Quantifiers.Extra.(++) → Data.List.Quantifiers.(++)
    • Libraries.Data.List.Quantifiers.Extra.head → Data.List.Quantifiers.head
    • Libraries.Data.List.Quantifiers.Extra.tail → Data.List.Quantifiers.tail
    • Libraries.Data.List1 → Data.List1
    • Libraries.Data.SnocList.revOnto → Data.SnocList.revOnto
    • Libraries.Data.SortedMap → Data.SortedMap
    • Libraries.Data.SortedSet → Data.SortedSet
    • Libraries.Utils.Binary.bufferData' → Data.Buffer.bufferData'
  • Removed unused functions:
    • Libraries.Data.List.Extra: breakAfter, splitAfter and zipMaybe
    • Libraries.Data.List.Quantifiers.Extra.tabulate.
    • Libraries.Utils.Binary.nonEmptyRev
    • Libraries.Utils.String.dotSep
  • Fixes an issue when unifying lambda terms with implicits (#3670)
  • The "With clause does not match parent" error now points to the correct location
  • The compiler now warns the user when impossible clauses are ignored. This typically happens when a numeric literal or an ambiguous name appears in an impossible clause.
  • Do not inline Core.sequence, because it is recursively defined.
  • Fixed coverage checker issues (#1800, #1998, #2318, #2822, #3679).
  • Fixed totality checking in namespace and mutual blocks (#2868, #3692).
  • Fixed incorrect argument multiplicity when using an as-pattern (#3687).
  • Type inspection now resugars primitive functions to more likely names/operators (#3712)
  • Better messages for errors inside string interpolation.
  • Added execution time logging for elaboration scripts.
  • Optimised the passing of local variables during compile-time normalisation.
  • Added getFC to elaborator reflection, exposing the macro call-site source location.

Building/Packaging changes

  • Fix parsing of capitalised package names containing hyphens.
  • Change flake.nix to point at idris-community/idris2-mode as the URL for inputs.idris-emacs-src (from the user fork redfish64/idris2-mode).

Backend changes

RefC Backend

  • Fixed an issue to do with alligned_alloc not existing on older MacOS versions, causing builds targeting PowerPC to fail (#3662). For these systems, the compiler will now use posix_memalign.
  • Fixed integer comparison operators returning incorrect results on WASM32. The idris2_extractInt function incorrectly used idris2_vp_to_Int32 for unboxed values, which dereferences unboxed pointers as Idris2_Int32* (previously Value_Int32*) on 32-bit platforms when UINTPTR_WIDTH is not defined (common in Emscripten).
  • Fix missing support for sized, signed integers in FFI.
  • Fix headers for numeric negation.
  • Prefix RefC Idris values with Idris2_ to prevent name collisions with third partly libraries.

Library changes

Base

  • Added rtrim to Data.String.
  • Added decToMaybe, maybeCong and maybeCong2 to Data.Maybe.
  • Added maybeEq to Decidable.Equality.
  • Removed writeIORef1, which unsafely allowed a linear value to become unrestricted.