Release 0.5.1

Commits

• 8d8d3ef: woops, missed the first let when resolving merge. thank goodness we are dealing with a static type system (Mathew Polzin)
• 6258662: fix arity for blodwen-set-thread-data (Edwin Brady)
• dad1804: Fix for thread data in racket/gambit too (Edwin Brady)
• 61e04e3: Use gsha256sum when sha256sum doesn't exist (Stiopa Koltsov)
• 106487c: [refactor] Move pathLookup from Compiler.Common to Utils.Path (Fabián Heredia Montiel)
• 9b8de95: Detect hashFn once (Fabián Heredia Montiel)
• dd7081e: Use --tag (non-reversed) variant of sha256sum for NetBSD compat (Fabián Heredia Montiel)
• b192be3: Merge branch 'name-quote-single-brace' of https://github.com/buzden/Idris2 into buzden-name-quote-single-brace (Edwin Brady)
• ae0e4f4: fix returned sexp for make-lemma command result (#570) (Arnaud Bailly)
• 948a5ba: noticed I was not quite retaining existing behavior around Alt error processing so fixed that. updated tests. (Mathew Polzin)
• 883097e: whitespace lint fix (Mathew Polzin)
• d9a56c5: Merge branch 'unification' of https://github.com/Russoul/Idris2 into Russoul-unification (Edwin Brady)
• a709f6d: Fix/reorganise tests (Edwin Brady)
• 4079ae0: Merge branch 'master' of https://github.com/AliasQli/Idris2 into AliasQli-master (Edwin Brady)
• f51aa22: Bring #1719 up to date with latest changes (Edwin Brady)
• c80a502: Return Bool from IOArray.writeArray (Stiopa Koltsov)
• 89125e9: merge w/ upstream (Mathew Polzin)
• ec3b868: rename experimental command line flag and group with the other experimental feature. (Mathew Polzin)
• 6c24b9e: fix bad merge conflict resolution. (Mathew Polzin)
• 07c62e9: Fixed wrong reflection of records and parameters (Giuseppe Lomurno)
• 37c7009: Removed leak of internal names from test reflection010 (Giuseppe Lomurno)
• 7e904ec: Update %hide help to show it takes a 'name'. (Thomas E. Hansen)
• 66217b6: Merge branch 'master' into refc-buffer (Edwin Brady)
• 3ee965e: FAQ/CONTRIBUTION updates (Edwin Brady)
• c4ed139: Replace per signal counter with per signal flag (Stiopa Koltsov)
• d2af6e5: Export throw and catch again in App (Edwin Brady)
• d1e6726: Update issue template for proposals (André Videla)
• c4b41ee: Remove all mentions of realpath from docs (Kamil Shakirov)
• 0fec867: [ fix ] Name in Language.Reflection.TT (Zoe Stafford)
• d4039d9: Add docs for chez-exe (Niklas Larsson)
• 41c20dd: Assertions in RefC runtime (Stiopa Koltsov)
• f195aed: [ Test ] allow 'N' as an acceptable response (Alex Humphreys)
• 877e830: A couple of documentation corrections (Edwin Brady)
• 5a351f4: Accept HasIO in onCollect functions (Stiopa Koltsov)
• ee063a5: Apply "qualified do" notation to bangs and comprehensions (#1700) (Ruslan Feizerakhmanov)
• ce44d3b: Change semantics of lines and unlines function to match Haskell and other languages (#1585) (Stepan Koltsov)
• 0ecf74e: System.Directory.nextDirEntry (Stiopa Koltsov)
• c7629e2: Skip dot and dot-dot in nextDirEntry (Stiopa Koltsov)
• 4eff6ac: System.Directory.listDir (Stiopa Koltsov)
• 7325002: Implement test discovery (Stiopa Koltsov)
• b663a06: Update javascript.rst (Kenneth J Hughes)
• ac595b1: Fix link to chez-exe (Niklas Larsson)
• d1b1ec0: Minor FAQ edits (Edwin Brady)
• 9aa7a43: Added documentation for new string literals (André Videla)
• 396ebe2: Add documentation for new string literals (André Videla)
• 2068eb2: Better ordering of delayed elaborators (Edwin Brady)
• 68db9fe: Add reg048 files (Edwin Brady)
• eabab4b: Split Windows CI build into multiple steps (Stiopa Koltsov)
• ab36ad7: Simplify a few Factor proofs (Nick Drozd)
• 440a3af: Update docs/source/reference/strings.rst (André Videla)
• 5f34801: Make drop and drop' public exported from the vect module. (Mathew Polzin)
• 74db771: [fix] Loading libidris2_support.dll with Racket (#1583) (Ben Hormann)
• 34167d5: [ ci ] controlling builds via commit messages (#1766) (G. Allais)
• 9f0a706: [ ci ] turn ubuntu-bootstrap-racket off for now (#1772) (G. Allais)
• 1276f47: Fix #1767 (André Videla)
• bab3897: move basic053->interpolation002, move basic061->basic053 (André Videla)
• edefd54: A bit of refactoring of argument elaboration order (Edwin Brady)
• e633a9f: Correct error018 test (Edwin Brady)
• 52c21c6: Update bootstrap code (Edwin Brady)
• 7c85971: Make sure main branch is covered in addition to master during the transition. Make the default branch for linting the main branch. (Mathew Polzin)
• 523c0a6: actually, with the change to the super linter, there's really no point in having CI work on both master and main at the same time, we just need to rename the branch right away for a smooth transition. (Mathew Polzin)
• 6811c33: Fix printing functions for string starter token (André Videla)
• f4e1346: Remove fromString calls from interpolated strings (André Videla)
• e5879dc: Document --init (Ellis Kesterton)
• 603c60e: Add some docs about building on Windows (Niklas Larsson)
• df43045: [ debug ] add a lot of logging throughout positivity checking (Guillaume ALLAIS)
• 230f42b: [ re #1771 ] Do not use Erased to go under binders (Guillaume ALLAIS)
• b24a9a5: [ re #1771 ] Fix another Erased-related issue (in nameIn) (Guillaume ALLAIS)
• d0c0698: [ re #1771 ] Check parameters for positive uses (Guillaume ALLAIS)
• 4b0edba: Update windows docs with gotchas (Niklas Larsson)
• a693138: [ fix ] bash TAB completion for files (stefan-hoeck)
• c28b257: Add ability to manipulate scheme objects (Edwin Brady)
• b76050d: Remove __collect_safe (Edwin Brady)
• 207a604: [ re #1782 ] A bit more debugging info (Guillaume ALLAIS)
• 13ef8ba: [ fix #1782 ] remove the case-specific code (Guillaume ALLAIS)
• 0d03064: Include GMP in the requirement list (Kamiλ Shakirov)
• 31ffb4e: [ cleanup ] various public export & cleanup (Guillaume ALLAIS)
• c48fe48: [ cleanup ] on is meant to be used with 2 arguments (Guillaume ALLAIS)
• 84b0643: [ ci ] add collie & frex (Guillaume ALLAIS)
• 4920601: Add tests for Nat ranges and fix bad range [1,2..1] behaviour. (#1794) (Sventimir)
• 8e1ca0e: Add break in each case alt in js backend (#1796) (Zoe Stafford)
• 94811ba: [ ci ] bring racket builds back (Guillaume ALLAIS)
• fe306f8: support explicitly setting a version tag during build. (Mathew Polzin)
• 52cc155: get a bit more specific about the GMP library requirement. (Mathew Polzin)
• 1669fc3: Refactor %builtin (#1803) (Zoe Stafford)
• 1b6cc3b: More Scheme readback machinery (Edwin Brady)
• ca95781: flake.nix: Use Racket's Chez for non-x86_64-linux platforms (Las Safin)
• f3855d7: Update contrib Text.Parser to match Library.Text.Parser (#1808) (Alex Humphreys)
• cd86340: Skip forced arguments in conversion check (Edwin Brady)
• 170af1e: Use Closures instead of NF in binders for normal forms (#1823) (Edwin Brady)
• 0d6049c: Fix error message for incorrect function patterns (#1816) (Ellis Kesterton)
• 15ccebb: [ contrib ] Implementation of Zippable was added for Validated (Denis Buzdalov)
• be37e5b: Added "lookupBetween" "leftMost" and "rightMost" to Data.SortedMap (Tim Engler)
• 590a9b1: Add a --list-packages command to the idris2 executable (#1824) (Mathew Polzin)
• 150bffc: [ doc ] Hopefully fix the linting problem in the docs (Denis Buzdalov)
• 21c6f4f: [ breaking ] remove parsing of dangling binders (#1711) (G. Allais)
• 9357d77: [ base ] Relax requirement of Alternative implementation for ReaderT (Denis Buzdalov)
• 99f1e11: [ cleanup ] Slightly improve readability (Denis Buzdalov)
• 8fb18e2: [ fix ] Make standard monad transformer's Alternative be lazy on 2nd arg (Denis Buzdalov)
• 377b21e: [ doc ] Remove trailing spaces from doc files (Denis Buzdalov)
• c339827: [ elab ] Add an ability to fail elab script with a custom FC (Denis Buzdalov)
• 940f588: [ ttimp ] Add a utility function returning an FC by TTImp (Denis Buzdalov)
• 23bb381: [ cleanup ] Small code cleanup, less mutual block and one \case use (Denis Buzdalov)
• 82796b3: print full names in linear checking (André Videla)
• c1ebc05: [ new ] semantic highlighting in REPL & holes (#1836) (G. Allais)
• c29dc73: [ base ] Add semigroup and monoid instances for Vect (Denis Buzdalov)
• dd7d77d: [ visibility ] Make Monad of Vect to the visible from outside (Denis Buzdalov)
• 1e8f9b3: [ fix ] export Show instance for Bounds (stefan-hoeck)
• 370a273: Inline Neg implementations (Daniel Kröni)
• 58907de: [ new ] specify data/record/interface (Guillaume ALLAIS)
• 089e2ec: [ refactor ] introduce defNameType (Guillaume ALLAIS)
• 2f53e56: [ new ] semantic highlighting for the html backend (Guillaume ALLAIS)
• 6f5e5da: [ pretty ] cleaning up binder names (Guillaume ALLAIS)
• e1bfaa7: [ cleanup ] remove commented out code (Guillaume ALLAIS)
• 1df84e8: [ fix #1635 ] Show module docstring in HTML backend (Guillaume ALLAIS)
• 8d8a135: [ fix #1496, fix #1345 ] propagate lex & lit fails too (#1850) (G. Allais)
• 4a9f000: [ close #1313 ] test case (Guillaume ALLAIS)
• ed9a21f: [ new ] support prim__putStr in browser (stefan-hoeck)
• 2465418: [ fix ] fix #1839 (#1857) (Stefan Höck)
• 99b0058: [ fix ] invalid Cast instances (Guillaume ALLAIS)
• 70ac0f4: Specify libc-name for tarm64osx (loovjo)
• e2addcf: [ new ] semantic highlighting via the IDE mode (#1868) (G. Allais)
• 2d7ddc6: [ fix #472 ] Port doc about comments from Idris1 (Peter Hajdu)
• 1e00277: [ fix #1859 ] Undo my mistakes (#1866) (G. Allais)
• 3e1f6ab: Add copyFile to System.File (#1797) (madman-bob)
• cdc157a: Add javascript support for getting system time as integer. (Mathew Polzin)
• 078db21: Return a Vect from Stream take (#1812) (Joel Berkeley)
• 7a3d557: Add copyDir function (#1805) (madman-bob)
• 126daf7: Remove DirInfo.error (Stiopa Koltsov)
• 79177a7: [ fix #1788 ] Only mention building using the previous version (Guillaume ALLAIS)
• 08d9e7d: [ install ] Install non-executable files with the executable flag off (Kamil Shakirov)
• ef91cc0: Add list difference to base Data.List module. (Mathew Polzin)
• bd94b91: mkdist.sh script cleanup (Kamil Shakirov)
• 0e4168e: [ ci ] ignore Release/ for idris2 builds (Guillaume Allais)
• 2428b35: [ install, docs ] Add a new makefile target to install libdocs (#1884) (Kamiλ Shakirov)
• d289ed6: [ fix #1887 ] Parse _ <- as DoBind instead of DoBinPat (Guillaume ALLAIS)
• 9498f44: [ fix ] Parse let _ = as Let rather than LetPat (Guillaume ALLAIS)
• a7d73d0: [ new ] ellipses for with patterns (Guillaume ALLAIS)
• 1d1c428: [ re #1828 ] test case (Guillaume ALLAIS)
• abd0552: [ docs ]: fix typo (#1893) (withoutK)
• 031508a: [ performance ] Common subexpression elimination (#1869) (Stefan Höck)
• d62e45d: [ contrib ] Make sorted map be able to store dependently typed values (Denis Buzdalov)
• b35e548: [ cleanup ] use whenJust (Guillaume ALLAIS)
• 2577832: [ new ] --total cli flag (Guillaume ALLAIS)
• 5d70c74: [ prelude ] Implement Semigroup for ordinary pairs (Denis Buzdalov)
• b918f1c: Simplify 01W Preorder (Nick Drozd)
• 7d6042a: Prove associativity and commutativity for 01W (Nick Drozd)
• 5126600: Cut some unused imports (Nick Drozd)
• c3a072c: Speculative normalisation (#1902) (Edwin Brady)
• 2a5739c: Check primitives (fromInteger etc) reduce on LHS (#1903) (Edwin Brady)
• 9865765: Normalise errors on display, not when they arise (#1906) (Edwin Brady)
• c861845: Abandon ambiguity resolution on undefined name (#1907) (Edwin Brady)
• b231ef0: [ fix #1831 ] Be more careful about checking primitive names (Guillaume ALLAIS)
• 6780874: nix flake: make it more idiomatic (Matthieu Coudron)
• af5657d: [ performance ] Memoise toplevel constants (#1899) (Stefan Höck)
• 30aa38f: [ cleanup ] Compiler.Common (Guillaume ALLAIS)
• 6fcb8b1: [ cleanup ] Compiler.Opts.CSE (Guillaume ALLAIS)
• 71511f4: code-blocks missing in the docs (#1911) (Guillaume ANDRIEU)
• 1559891: [ base ] Indexing Vectors. (#1892) (Jan de Muijnck-Hughes)
• 911a907: [ highlighting ] Builtin.assert_ functions using postulate face (#1914) (G. Allais)
• 1f85265: [ re #1632 ] (->) does not unify with any of TCon/Type/PrimVal (Guillaume ALLAIS)
• 6a6ad30: [ fix ] consolidating mismatchNF (Guillaume ALLAIS)
• 654d399: Add function that checks whether a file handle points to a TTY device. (#1908) (Mathew Polzin)
• 281ae86: [ fix ] string casts on js backends (stefan-hoeck)
• 9e4d97f: invFin: export ~> public export and invFinSpec (#1890) (Ruslan)
• 853547e: [ golden ] Allow test dir names to contain spaces (Denis Buzdalov)
• d4553a1: Add chez-scheme to chez search path (#1921) (shenlebantongying)
• 4b44859: Thread the option of silencing output to stdout (#1919) (Ruslan)
• 7baf698: Made unifying error msg nicer. (#1922) (Tim Engler)
• 32e26c5: [ refactor ] introduce UserName for (UN/RF) (#1926) (G. Allais)
• f6281af: [ elab ] Erase check and quote's main argument (#1847) (Denis Buzdalov)
• 426441e: [ new ] persistent css switch and alternative style files (#1923) (G. Allais)
• 8b9916f: [ html ] Various HTML docs fixes (#1924) (G. Allais)
• 44328d7: [ fix ] Wrap paths in quotes for one more call for system (Denis Buzdalov)
• 304c0e6: [ install ] Fix install-libdocs makefile target (Kamil Shakirov)
• 34c7209: Retain the --client mode behaviour (Ruslan Feizerakhmanov)
• 971afa9: Add a transform rule making (++) for List tail-recursive. (#1888) (James Cook)
• 22c1204: Small fix for incremental compilation (#1930) (Edwin Brady)
• ada3eb4: Version 0.5.0 (#1931) (Edwin Brady)
• 6802827: Remove __collect_safe from bootstrap chez (#1933) (Edwin Brady)
• 2e98dd6: Abandon auto search on undefined name (#1938) (Edwin Brady)
• 87c1cb6: [ repl ] better printing of holes (Guillaume ALLAIS)
• 1e90182: Version increment to 0.5.1 (#1939) (Edwin Brady)
• bf0a157: Disable -Xcheck-hashes, at least for the moment (#1940) (Edwin Brady)
• 2376439: Fix Package build (Edwin Brady)
• 6d1cb38: Compatibility fix (again) (Edwin Brady)
• 29aa9dd: Compile with JVM bootstrap backend (Marimuthu Madasamy)
• 93d21f5: Support for self hosting (Marimuthu Madasamy)
• fb34f2d: Build 0.2.2 (Marimuthu Madasamy)
• 023da03: Update README to indicate WIP for Idris 2 0.3.0 (Marimuthu Madasamy)
• c3dda40: Fix build, package libraries (Marimuthu Madasamy)
• b7de2ae: Enhance IdrisPaths.idr ro read IDRIS2_PREFIX at runtime, fix build (Marimuthu Madasamy)
• fd02509: Rename modules and packages to match repository (Marimuthu Madasamy)
• 2844af0: Add latest release workflow (Marimuthu Madasamy)
• a6da938: Fix branch name on latest release workflow (Marimuthu Madasamy)
• 8e2cf60: Fix libraries packaging, enable latest release for master (Marimuthu Madasamy)
• dc8c724: Fix code formatting (Marimuthu Madasamy)
• 70f5424: Fix command for compilation (Marimuthu Madasamy)
• 4341554: Optimize 0-arity functions, prepare for self hosting, implement future (Marimuthu Madasamy)
• b02d7d6: Optimize 0-arity foreign functions (Marimuthu Madasamy)
• b495921: Self host 0.3.0 (Marimuthu Madasamy)
• 5315209: Prepare for 0.3.0 release (Marimuthu Madasamy)
• d3cda1c: Update release link to point to latest release (Marimuthu Madasamy)
• 4e5f597: Build 0.4.0 (Marimuthu Madasamy)
• 339cec1: Fix constructor tag in optimizer (Marimuthu Madasamy)
• c3678b9: Prepare for 0.4.0-rc.2 (Marimuthu Madasamy)
• d70756e: Fix constant case expression scope, char conversion (Marimuthu Madasamy)
• a64f6f5: Enhance trampoline, fix function signature, optimize lambda (Marimuthu Madasamy)
• 6faeff1: Fix libraries packaging (Marimuthu Madasamy)
• 5919042: Self host 0.4.0, deploy to maven (Marimuthu Madasamy)
• 621e198: Prepare for release 0.4.0 (Marimuthu Madasamy)
• f4e7a90: Fix license link (Marimuthu Madasamy)
• cde992c: Fix jar packaging (Marimuthu Madasamy)
• 1b8fe03: Build 0.5.1 for JVM (Marimuthu Madasamy)
• 66223d0: Self host 0.5.1 for JVM (Marimuthu Madasamy) #139