Skip to content

Release 0.4.0-rc.1
Compare
Choose a tag to compare
@github-actions github-actions released this 11 Oct 02:06
· 1518 commits to main since this release
v0.4.0-rc.1
2d81e68

Commits

  • c54c1a6: Add some inlines (Edwin Brady)
  • 251d77b: Swap 'False' and 'True' constructors (Edwin Brady)
  • e58bcfc: Semantic highlighting (#1335) (Ohad Kammar)
  • 8038f0a: [ refactoring ] Tiny changes following up the idris-lang/Idris2#830 (Denis Buzdalov)
  • 25ae664: [ fix #1378 ] Collect constructors after inlining (#1380) (Zoe Stafford)
  • 5048103: [ contrib ] add (alissa-tung)
  • 53094e3: Choose foreign string based on priority (Niklas Larsson)
  • 08d61d7: [ fix #1370 ] use the lambda's type for eta-expansion (Guillaume ALLAIS)
  • 8a7aeca: [ builtin ] O(1) natToInteger for any 'Nat'-like type (#1363) (Zoe Stafford)
  • f028981: [ fix #801 ] Use Number for up to 32 bit integers on JS backends (#1375) (Stefan Höck)
  • 4de7b21: [ new ] Add chez-sep codegen (#1359) (Matúš Tejiščák)
  • ab24121: [ breaking ] making toList part of Foldable (#1395) (G. Allais)
  • 1d70a83: Mention Compiler.Separate in the CHANGELOG. (Matus Tejiscak)
  • 004cc45: [ test ] cosmetic changes & retest capability (#1394) (G. Allais)
  • efaf290: Calculate whether an inlining is safe (Edwin Brady)
  • f21a495: Merge github.com:idris-lang/Idris2 into tweak-cg (Edwin Brady)
  • 75de88d: Add missing cases in hashing ConInfo (Edwin Brady)
  • 364eaff: [ towards #1124 ] Statically enforced logging (#1402) (Stefan Höck)
  • 1d762d4: Print constructor labels correctly (Edwin Brady)
  • 5b246ed: [ totality ] Make Language.Reflection modules have %default total (Denis Buzdalov)
  • 8d4c955: [ new ] tab auto-completion in bash-like shells (stefan-hoeck)
  • 2a57f1c: [ doc ] instructions for activating tab completion (stefan-hoeck)
  • dece431: [ refactor ] minor changes (Guillaume ALLAIS)
  • ecfa1f5: [ debug ] adding existing log levels to autocompletion (Guillaume ALLAIS)
  • c798f6d: [ fix ] auto-complete known log topics (stefan-hoeck)
  • 1a6c8ee: [ fix ] support all log level prefixes (stefan-hoeck)
  • 2100260: [ fix ] Handle ambiguous DPair/MkDPair (Guillaume ALLAIS)
  • 664a761: Remove path and version from Racket libc FFI definer (Johann Rudloff)
  • b9e95d5: Do not explicitly load libc on FreeBSD (Johann Rudloff)
  • 2477d06: Use sysctl instead of nproc to get number of processors on FreeBSD (Johann Rudloff)
  • 7fe8c42: [ builtin ] O(1) integerToNat for any 'Nat'-like type (#1403) (Zoe Stafford)
  • 7e52099: [ fix ] missing log option (#1411) (Zoe Stafford)
  • ba10b46: Add missing 'commit' on backtrack (Edwin Brady)
  • 0392b49: [ doc ] Update the test-lib's readme according to the current state (Denis Buzdalov)
  • 3610464: [ fix ] record projections (Guillaume ALLAIS)
  • 4917d12: [ fix ] highlighting of tuples (Guillaume ALLAIS)
  • c6f125b: Fix tail calls in node back end (Edwin Brady)
  • 3493083: [ fix #621 ] add warnings for shadowed global definition (#1407) (G. Allais)
  • 45fc100: Store postponed unification problems as values (Edwin Brady)
  • 70d8e4b: Merge github.com:idris-lang/Idris2 into unify-postponing (Edwin Brady)
  • 5ac441a: Some micro-optimisations (Edwin Brady)
  • e3fa071: Don't calculate blocked metavariable set (Edwin Brady)
  • d97f526: [ perf ] Move unnecessary toFullNames calls under a logC (#1423) (Ruslan Feizerakhmanov)
  • 7cc88d2: [ elab ] More descriptive "Bad elaborator script" error message (#1427) (Denis Buzdalov)
  • d0a6c9b: [ debug ] better information (Guillaume ALLAIS)
  • ac4b31b: [ fix #1421 ] Use resolved names for the impossible LHS (Guillaume ALLAIS)
  • f98bb39: Bugfix highlighting of let declarations (Ohad Kammar)
  • 2f66f3e: [ test ] case for the fix (Guillaume ALLAIS)
  • 669bcf3: Avoid reading whole ttcs unnecessarily (Edwin Brady)
  • 66f3787: [ cleanup ] Annotate JS backend sources (#1425) (Stefan Höck)
  • 7f210b5: Inline small metavariables (Edwin Brady)
  • d51fe89: Trim namespace when writing definitions to TTC (Edwin Brady)
  • eca2577: [ doc ] updated changelog (stefan-hoeck)
  • b94f7e9: Strip current namespace when writing out defs (Edwin Brady)
  • 72e0245: Remove trailing space (Edwin Brady)
  • 5ab91ca: Substantial reduction in TTC size (Edwin Brady)
  • f6919af: Increment TTC version (Edwin Brady)
  • 890810e: Remove unsecure commands (#1433) (Michael Messer)
  • 31a5175: [ re #1031 ] Disallow ? patterns on the LHS (Guillaume ALLAIS)
  • 823230b: Vect reasoning library (#1439) (Ohad Kammar)
  • 618c714: [ close #1384 ] built-in Snoc-lists [< 1, 2, 3 ] (#1383) (Ohad Kammar)
  • 06ca4be: Refactor C codegen (Robert Wright)
  • d961c04: Make RefC fail noisily (Robert Wright)
  • 51ddcad: Improve RefC foreign function support (Robert Wright)
  • 2a957a3: Add RefC FFI header file support (Robert Wright)
  • 978d86f: Fix RefC identity functions memory management (Robert Wright)
  • c34c6e0: Complete RefC standard String support (Robert Wright)
  • 204b96f: Add RefC math library linking (Robert Wright)
  • ecde887: Add RefC external type support (Robert Wright)
  • cf2b05c: Add RefC Buffer support (Robert Wright)
  • f3aae06: Add RefC Clock support (Robert Wright)
  • cd39066: Add RefC getArgs support (Robert Wright)
  • 58a321c: Add RefC foreign closure support (Robert Wright)
  • c57bb5a: Add RefC StringIterator support (Robert Wright)
  • 1e15ff3: Disable C file linting (Robert Wright)
  • 5aef7a2: fixup! 04dfba03 (Robert Wright)
  • 50d75cc: [ cleanup ] logging (#1442) (Zoe Stafford)
  • e9f5038: [ fix ] Version encoding should be stable (#1443) (G. Allais)
  • ee7956b: [ cleanup ] move DocString to Doc.String (Guillaume ALLAIS)
  • 6904cf5: [ :doc ] Adding projections to the record doc (Guillaume ALLAIS)
  • b457d15: [ fix #221 ] realpath alternative for macOS (Ben Hormann)
  • 7ca526e: fix typo (archlinuxxx)
  • 699de70: [contrib] More properties of vectors (#1449) (Ohad Kammar)
  • ad656a8: Remove realpath (#1457) (Kamiλ Shakirov)
  • e293d82: [ fix ] System.getArgs on node backend (stefan-hoeck)
  • 6f90e5d: [ test ] node test for System.getArgs (stefan-hoeck)
  • 961683a: [ FFI ] Support new IntX types in foreign function types (#1437) (Stefan Höck)
  • a0a4172: Simple signal handling (#1458) (Mathew Polzin)
  • d9318a2: [ Fixup #1437 ] Correct cases in cftySpec (Fabián Heredia Montiel)
  • 704a252: [ fix #55 ] Propagate linear context from Definition to Clauses (Fabián Heredia Montiel)
  • f1085b9: [ test #18 ] Add passing tests from issue to avoid regressions (Fabián Heredia Montiel)
  • 1fd5ccf: [ fix #1453 ] rename cast -> coerce (#1468) (G. Allais)
  • 4b0f171: [ help ] display logging topics and accompanying blurbs (if any) (#1467) (G. Allais)
  • 1aefab3: [ fix ] nproc missing for non-GNU systems (Ben Hormann)
  • 6920545: A rough dump of how to debug idris2's workings. (#1464) (Jan de Muijnck-Hughes)
  • 68f6f4d: Cache intermediate results in totality checking (Edwin Brady)
  • 9cce0e1: Remove whitespace in test file (Edwin Brady)
  • a9b754e: Remove whitespace again (Edwin Brady)
  • b5cbf92: [ test ] cosmetic improvements (Guillaume ALLAIS)
  • 30c178c: [ feature ] Implement -Werror (WarningsAsErrors) (#1466) (Fabián Heredia Montiel)
  • 2e61779: [ docs ] Build docs for the 'test' package (Kamil Shakirov)
  • d69e35c: [ re #1466 ] Actually error out with -Werror (#1474) (G. Allais)
  • eb044fc: Support prim__codegen on javascript (Zoe Stafford)
  • 6f83924: [ warn ] holes are not shadowed by implicits (Guillaume ALLAIS)
  • da4ee92: [ cleanup ] Remove unnecessary Libraries.Utils.Either (Fabián Heredia Montiel)
  • 6df80ff: [ cleanup ] tests/Main.idr import list (Guillaume ALLAIS)
  • 6b07113: [ feature ] Expose 'resolvedAs' and 'getSimilarNames' (Andor Penzes)
  • 24f7c9d: Add foldMap to Foldable (#1483) (Zoe Stafford)
  • 29cc1f4: [ refactor ] Use f <$> ... instead of pure f <*> ... in traverses (Denis Buzdalov)
  • eccce3b: [ fix ] Memoize intermediary results in JS backends (#1494) (Stefan Höck)
  • 98d6749: RefC Integer Support (#1480) (madman-bob)
  • c5b10f0: [ doc ] for the linear pair constructor (#1492) (G. Allais)
  • 4a193b3: Small pruning fix (Edwin Brady)
  • 2a4197e: [ doc ] Some documentation on := syntax of let bindings (#1487) (Denis Buzdalov)
  • 18e15e2: [ fix ] Cast CLOCKS_PER_SEC to float before division (Johann Rudloff)
  • 9e7625e: [ log ] more readable output for elab.ambiguous (#1500) (G. Allais)
  • 5fa272b: Read import hashes correctly (Edwin Brady)
  • baa6051: [ fix ] use twos complement truncation for signed ints (#1471) (Stefan Höck)
  • 7aee7c9: [ new ] --install-with-src; refactoring around FCs (#1450) (Ruslan Feizerakhmanov)
  • d12abbd: Add a 'shortcut' to conversion check (Edwin Brady)
  • aa94dd2: Add RefC Char pattern matching support (Robert Wright)
  • 9a523ed: Recover full file name when encoding FC to SExp in Name-At command (Ruslan Feizerakhmanov)
  • f0af11a: Always return absolute paths (Ruslan Feizerakhmanov)
  • abd5432: [ fix ] indentation of impossible clauses (#1520) (CodingCellist)
  • a281550: Remove unused 'useMetas' field (Edwin Brady)
  • 9512683: Recover the original way of sending file contexts to idemode clients (Ruslan Feizerakhmanov)
  • 7d23527: Remove redundant converstion checks in Pi types (Edwin Brady)
  • 18c7e2c: Merge github.com:idris-lang/Idris2 into normalise-tweaks (Edwin Brady)
  • a75887f: Update error018 test output (Edwin Brady)
  • 4a09707: vars can be erased in evalLocal (Edwin Brady)
  • 2061982: [cleanup] Remove half of Libraries.Data.List1 (Fabián Heredia Montiel)
  • 0df3316: [cleanup] Remove Libraries.Data.Bool.Extra (Fabián Heredia Montiel)
  • 663a838: Properly normalise constants on LHS (Edwin Brady)
  • 38bdbfb: Please the linter (Edwin Brady)
  • f923c36: Please the linter again (Edwin Brady)
  • 06f69ba: Fix test output (Edwin Brady)
  • 19cb268: Only fully normalise fromInteger on LHS (Edwin Brady)
  • 012d7f8: [ README ] Contributors wanted. (Andor Penzes)
  • ba92a82: Contributors -> Contributions (André Videla)
  • dad4dcd: Add totality annotations to src and libs/{prelude, base} (Fabián Heredia Montiel)
  • bf09856: [ totality ] More %default total stuff (Denis Buzdalov)
  • 97ee3d4: Check LHS arguments are polymorphic enough (Edwin Brady)
  • fda76b8: Merge github.com:idris-lang/Idris2 (Edwin Brady)
  • 4c99537: Add color to tests (Fabián Heredia Montiel)
  • 4a0a575: Return Maybe from strengthen (#1540) (Nick Drozd)
  • bdd8f41: Add drop for Vect. (Mathew Polzin)
  • 1133658: Add missing unlock in signal handling C code. (Mathew Polzin)
  • 0209cee: include the other definition of drop because both are quite useful. (Mathew Polzin)
  • 85e4df8: Add filenames to Golden Test missing file error reporting (Robert Wright)
  • c63f25d: Distinguish common C and RefC FFI calls (Robert Wright)
  • d202139: Distinguish common C and RefC Buffer functions (Robert Wright)
  • c6a5827: Add RefC readBufferData/writeBufferData support (Robert Wright)
  • 195e690: Fix RefC Buffer getInt function to work with large values (Robert Wright)
  • 1875f62: Remove freeBuffer function (Robert Wright)
  • e9b42cc: Guarantee Ref C Buffer 0 initialization (Robert Wright)
  • a91b45d: use socketaddr_storage in getsockname (Martin Molzer)
  • ac31e17: [ refactor ] Right-align padded numbers. (#1554) (CodingCellist)
  • b946ec0: [ fix ] Create library dir if necessary (#1300) (claymager)
  • 757f41f: [test] Add preformance test of Fin/Vect (Fabián Heredia Montiel)
  • 488b470: Use map for some maybes (#1548) (Nick Drozd)
  • 7692de6: Allow underscores in integer literals to aid readability (Kamil Shakirov)
  • 927c358: [ base ] Some lacking implementations for Uninhabited were added (Denis Buzdalov)
  • a28bc65: Fix deadlocks [Rebased, Squashed] (#1536) (Fabián Heredia Montiel)
  • a3a9b5c: Merge github.com:idris-lang/Idris2 (Edwin Brady)
  • ff9725b: Tidy up applyToStack/continueNF (Edwin Brady)
  • 9fbdf56: Add CBV mode to the evaluator (Edwin Brady)
  • ec43876: Simplify some lambdas (#1561) (Nick Drozd)
  • 0db136d: Hoist some pures (#1556) (Nick Drozd)
  • e0e8403: [ new ] detect changes using sha256 rather than timestamps (#1535) (Fabián Heredia Montiel)
  • 41c3fd2: [docs] ind-ind ind-rec rec-rec in style of fwddecl (#1558) (Alissa Tung)
  • c04835c: [ cleanup ] Reuse Tarjan's algorithm in JS backend and some other cleanups (#1504) (Stefan Höck)
  • 3e3a4e1: Use truncated case notation (#1562) (Nick Drozd)
  • 55f8bc3: Improve case-splitting formatting to not introduce new whitespace; add a bit of comments+docs. (#1553) (CodingCellist)
  • f3177e0: [ fix ] print postfix projections... postfix (#1557) (G. Allais)
  • fb14b57: Add clarifying note re: PREFIX in config.mk (I B 3)
  • 722bab8: Stop pointing at the Void (I B 3)
  • da21f04: Add note to INSTALL.md re: PREFIX being an absolute path (I B 3)
  • 68c6fe2: [ Fix #1577 ] Actually use natMinus hack (#1578) (Tim Engler)
  • 657699a: [doc] Add missing entries and refactor CHANGELOG.md (#1566) (Fabián Heredia Montiel)
  • a8264f8: Add ability to extend RefC backend to create further backends (Robert Wright)
  • 37f8c2c: Merge github.com:idris-lang/Idris2 into eval-updates (Edwin Brady)
  • 95710c3: Add chezscheme binary to search path (Matt Smith)
  • e35930a: Change reg042 to look at compiler output (Edwin Brady)
  • ab2012a: Small change in output of reg042 (Edwin Brady)
  • 49f8cef: [ cleanup ] Test.Golden (#1526) (G. Allais)
  • d2986e5: [ refactor ] to allow testpools to specify a backend (#1591) (G. Allais)
  • verbatim URLs are deprecated (zseri)
  • c760812: fix #1514 (Broken doc in the theorem proving part of Idris2) (zseri)
  • 92066c2: Add timeout for definition/expression search (Edwin Brady)
  • 4ef29da: Fix expression search on already solved holes (Edwin Brady)
  • 7802b72: Refine timeout mechanism (Edwin Brady)
  • 21cca08: [ fix ] missing Show Void in prelude (Guillaume ALLAIS)
  • af1cbbf: Update CHANGELOG (Edwin Brady)
  • a0cfa28: Update version numbers (Edwin Brady)
  • 4d12766: [ fix ] expected test output (Guillaume ALLAIS)
  • ae73c39: Merge github.com:idris-lang/Idris2 into prepare-040 (Edwin Brady)
  • afd5595: [ fix ] missing Show (Fin n) in base (Guillaume ALLAIS)
  • 56a9a58: Update version number in pkg010 test (Edwin Brady)
  • 7d3e3e0: Check sizes of buffers and strings in TTCs (Edwin Brady)
  • 991a4e8: Update bootstrap scheme (Edwin Brady)
  • a93def9: Merge github.com:idris-lang/Idris2 into prepare-040 (Edwin Brady)
  • 6511412: Change heading in CHANGELOG (Edwin Brady)
  • 80aeeca: Add note on --mkdocs (Edwin Brady)
  • 980b617: Added --mkdoc to CHANGELOG too (Edwin Brady)
  • 0010773: More version number updates (Edwin Brady)
  • 8bff4e6: Fix Package build (Edwin Brady)
  • afa6bbe: Compatibility fix (again) (Edwin Brady)
  • c861a8e: Compile with JVM bootstrap backend (Marimuthu Madasamy)
  • 14a5d80: Support for self hosting (Marimuthu Madasamy)
  • 874966e: Build 0.2.2 (Marimuthu Madasamy)
  • 74dda9e: Update README to indicate WIP for Idris 2 0.3.0 (Marimuthu Madasamy)
  • 1663f7f: Fix build, package libraries (Marimuthu Madasamy)
  • c1013bd: Enhance IdrisPaths.idr ro read IDRIS2_PREFIX at runtime, fix build (Marimuthu Madasamy)
  • 3598f76: Rename modules and packages to match repository (Marimuthu Madasamy)
  • c0b20e9: Add latest release workflow (Marimuthu Madasamy)
  • f569451: Fix branch name on latest release workflow (Marimuthu Madasamy)
  • 1aded90: Fix libraries packaging, enable latest release for master (Marimuthu Madasamy)
  • c32ca8f: Fix code formatting (Marimuthu Madasamy)
  • ab479e5: Fix command for compilation (Marimuthu Madasamy)
  • 1024e50: Optimize 0-arity functions, prepare for self hosting, implement future (Marimuthu Madasamy)
  • 1a45af7: Optimize 0-arity foreign functions (Marimuthu Madasamy)
  • c73b324: Self host 0.3.0 (Marimuthu Madasamy)
  • 76f8547: Prepare for 0.3.0 release (Marimuthu Madasamy)
  • 567a97a: Update release link to point to latest release (Marimuthu Madasamy)
  • 2d81e68: Build 0.4.0 (Marimuthu Madasamy) #130
Assets 3
Loading