Update dependency idris-lang/Idris-dev to v1 #20

renovate · 2022-07-14T19:08:52Z

This PR contains the following updates:

Package	Update	Change
idris-lang/Idris-dev	major	`0.4.2` -> `1.3.4`

Release Notes

idris-lang/Idris-dev

`v1.3.4`

Compare Source

Renamed 'forall' function for compability with future GHC releases
Updated version bounds
Bugfixes

`v1.3.3`

Compare Source

Updated to work with GHC 8.8 and cabal 3.0
Bugfixes and documentation updates

`v1.3.2`

Compare Source

Documentation added to proof section

Library updates

openFile opens the file in binary mode on Windows.
Added library functions clockTime and fRemove

Tool updates

Modules no longer require building if imports have changed but all
interfaces (i.e. types for names declared export and definitions of names
declared public export) are unchanged.
The result of calling :doc now details the accessbility of items as well as their totality.

Miscellaneous updates

Compiler flag --optimise-nat-like-types enables compilation
of Nat-like type families to big integers. A type family
is Nat-like if, after erasure, it has two constructors,
one nullary, the other one with exactly one recursive field.

`v1.3.1`

Compare Source

Tool updates

Fixes for building with GHC 8.6
Fix for megaparsec update
Some fixes for memory allocation issues in the C back end

`v1.3.0`

Compare Source

Language updates

Old 'induction' tactics and eliminator generation functionality ('%elim', '%case', 'elim_for') is no longer supported.
Please, rely on the ones provided by Pruviloj and elaborator reflection instead.

Library updates

Changed rndInt in Effect.Random so that it does not alternate between odd
and even.
Additions to contrib:
- Data.SortedBag: Bag (or Multiset) implemention based on Data.SortedMap.
- Data.PosNat: A Nat paired with a proof that it is positive.
- Data.Chain: A function with an arbitrary number of arguments, plus
  combinators for working with them.

Tool updates

Added a switch --allow-capitalized-pattern-variables to optionally allow capitalized pattern variables after they were prohibited in 1.2.0.
REPL now prints an error message if program compiled by :exec terminates
abnormally.
Idris now builds with GHC 8.4.
In the C backend, the representation of Idris values at runtime has been reworked.

`v1.2.0`

Compare Source

Language updates

In @-patterns such as x@p, x is now in scope on the right-hand side
of any definitions in where clauses, provided the left-hand side of the
definition does not shadow it.
The LinearTypes language extension has been revised. It implements the
rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative
Type Theory" and now works with holes and case expressions.
Backticked operators can appear in sections, e.g. (`LTE` 42) or
(1 `plus`).
Backticked operators can have their precendence and associativity set like
other operators, e.g. infixr 8 `cons` . Backticked operators with
undeclared fixity are treated as non-associative with precedence lower
than all declared operators.
Allow non-injective implementations if explicitly named, e.g.,
```
LTB : Nat -> Type
LTB b = DPair Nat (\ n  => LT n b)

implementation [uninhabltb] Uninhabited (LTB Z) where
  uninhabited (MkDPair n prf) = absurd prf
```
It is possible to use using implementation uninhabltb to add the
implementation to the automated resolution, but if it fails to find the
instance due to non-injectivity, one must pass it explicitly to target
function, i.e. absurd @{uninhabltb}.
Verbatim strings now support trailing quote characters. All quote characters
until the final three are considered part of the string. Now a string such as
""""hello"""" will parse, and is equivalent to "\"hello\"".
C FFI now supports pasting in any expression by prefixing it with '#', e.g.
```
intMax : IO Int
intMax = foreign FFI_C "#INT_MAX" (IO Int)
```
The deprecated keywords %assert_total, abstract, and [static] have
been removed as well as the use of "public" instead of "public export" to
expose a symbol.
The syntax for pattern-match alternatives now works for let statements in
do blocks in addition to let expressions and <- statements, e.g.
```
  do …
     let Just x = expr | Nothing => empty
     …
```
This means that a with-application (using |) cannot be used in that
position anymore.

Library Updates

Removed oldeffects library from libs folder, use effects or Control.ST instead.
Added Text.Literate, a module for working with literate source files.
Added Data.IORef, for working with mutable references in IO and JS_IO.
Added discriminate and construct tactics to Pruviloj.
Added IsSucc type to Prelude, which proves that a Nat is a successor.
Added Data.IOArray, containing primitives for mutable arrays.
Added Language.JSON, for total serialization/deserialization of JSON data.
Reworked operator fixity for many operators.
- Changed && and || to be right-associative. Increased precedence of &&
  to be higher than that of ||.
- Removed associativity from Boolean comparison operators ==, /=, <, <=,
  >, and >=. Increased precedence of /= and == to match the others.
- Made <|>, <$>, and . right-associative.
- Swapped precedence of <|> and <*> (and its related operators, <* and
  *>). Now <|> has a lower precedence.
- Lowered the precedence of >>= to be below that of <|>.
Added some useful string manipulation functions to Data.String.Extra.
Added Control.Delayed, a module for conditionally making a type Inf or Lazy.
Added Data.Fuel, which implements the Fuel data type and the partial forever function.
Added Data.Bool.Extra, a module with properties of boolean operations.
Moved core of Text.Lexer to Text.Lexer.Core. Added several new combinators
and lexers to Text.Lexer.
Moved core of Text.Parser to Text.Parser.Core. Added several new combinators
to Text.Parser. Made the following changes.
- Flipped argument order of parse.
- Renamed optional to option and flip argument order.
- Renamed maybe to optional.
- Generalised many combinators to use an unknown commit flag where possible.
Prelude.Doubles.atan2 is now implemented as a primitive instead of
being coded in Idris.
Added Test.Unit to contrib for simple unit testing.
Removed several deprecated items from the libraries shipped with Idris.
Moved abs from the Neg interface into its own Abs interface. Nat
implements Abs with abs = id.
Added Control.ST.File, an ST based implementation of the same behaviour
implemented by Effect.File in the effects package.

Tool Updates

Private functions are no longer visible in the REPL except for modules
that are explicitly loaded.
The --interface option now creates CommonJS modules on the node backend.
The C backend now pass arguments to the C compiler in the same order
as they were given in the source files.
Backslash, braces and percent symbols are now correctly pretty printed
in LaTeX.
Errors and warnings now consistently have the following format:
```
reg068.idr:1:6-8:
  |
1 | data nat : Type where --error
  |      ~~~
Main.nat has a name which may be implicitly bound.
This is likely to lead to problems!
```
The code is highlighted when highlighting information is available. How
much highlighting information is available depends on where the error
occurred.
The parser provider has been switched from Trifecta to Megaparsec. This
could possibly cause some subtle deviations in parsing from previous
versions of Idris.
Many more errors now report beginning and ending position (which may be
on different lines), instead of just a single point. The format is
Foo.idr:9:7-15: if ending column is on the same line or
Foo.idr:9:7-10:15: if the ending column is on a different line.
Error messages were changed so that the last column is inclusive, e.g.
Foo.idr:9:7-15: includes column 15. Previously the error would have read
Foo.idr:9:7-16:.

Packaging Updates

Package names now only accept a restrictive charset of letters, numbers and the -_ characters.
Package names are also case insensitive.
When building makefiles for the FFI, the environment variables
IDRIS_INCLUDES and IDRIS_LDFLAGS are now set with the correct C
flags.

`v1.1.1`

Compare Source

Erasure analysis is now faster thanks to a bit smarter constraint solving.
Fixed installation issue
Fixed a potential segfault when concatenating strings

`v1.1.0`

Compare Source

Library Updates

Added Text.PrettyPrint.WL an implementation of the Wadler-Leijen
Pretty-Print algorithm. Useful for those wishing to pretty print
things.
Added Text.Lexer and Text.Parser to contrib. These are small libraries
for implementing total lexical analysers and parsers.
New instances:
- Added Catchable for ReaderT, WriterT, and RWST.
- Added MonadTrans for RWST.
Added utility functions to Data.SortedMap and Data.SortedSet (contrib),
most notably merge, merging two maps by their Semigroup op (<+>)
Prelude.WellFounded now contains an interface Sized a that defines a size
mapping from a to Nat. For example, there is an implementation for lists,
where size = length.

The function sizeAccessible then proves well-foundedness of the relation
Smaller x y = LT (size x) (size y), which allows us to use strong
induction conveniently with any type that implements Sized.

In practice, this allows us to write functions that recurse not only on
direct subterms of their arguments but on any value
with a (strictly) smaller size.

A good example of this idiom at work is Data.List.Views.splitRec from base.
Added utility lemma decEqSelfIsYes : decEq x x = Yes Refl to
Decidable.Equality. This is primarily useful for proving properties of
functions defined with the help of decEq.

Tool Updates

New JavaScript code generator that uses an higher level intermediate
representation.
Various optimizations of the new JavaScript code generator.
Names are now annotated with their representations over the IDE
protocol, which allows IDEs to provide commands that work on special
names that don't have syntax, such as case block names.

`v1.0.1`

Compare Source

`v0.99.2`

Compare Source

Library Updates

Added Data.Buffer to base. This allows basic manipulation of mutable
buffers of Bits8, including reading from and writing to files.

Tool Updates

Idris now checks the list of packages specified at the command line
against those installed. If there is a mismatch Idris will complain.

Miscellaneous Updates

Documentation updates for the new Control.ST library
Various stability/efficiency fixes

`v0.99.1`

Compare Source

Language updates

Language pragmas now required for the less stable existing features, in
addition to the existing TypeProviders and ErrorReflection:
- ElabReflection, which must be enabled to use %runElab
- UniquenessTypes, which must be enabled to use UniqueType
- DSLNotation, which must be enabled to define a dsl block
- FirstClassReflection, which must be enabled to define a %reflection
  function
New language extension LinearTypes:
- This allows adding a /multiplicity/ to a binder which says how often it
  is allowed to be used; either 0 or 1 (if unstated, multiplicity is "many")
- The typing rules follow Conor McBride's paper "I Got Plenty o' Nuttin'"
- This is highly experimental, unfinished, not at all polished. and there
  are still lots of details to sort out. Some features don't quite work
  properly yet. But it is there to play with for the brave!

Tool Updates

Idris' output has been updated to more accurately reflect its
progress through the compiler i.e. Type Checking; Totality Checking;
IBC Generation; Compiling; and Code Generation. To control the
loudness of the reporting three verbosity levels are introduced:
--V0, --V1, and --V2. The old aliases of -V and --verbose
persist.
New REPL command :! that runs an external shell command.
The REPL now colourises output on MinTTY consoles (e.g., Cygwin and MSYS)
on Windows, which previously did not occur due to a bug.
Idris now runs in a UTF-8-compatible codepage on Windows. This fixes many
Unicode-rendering issues on Windows (e.g., error messages stating
commitBuffer: invalid argument (invalid character)).
Idris now has a --warnipkg flag to enable auditing of Idris
packages during build time. Currently auditing check's the list of
modules specified in the iPKG file with those presented in the
package directory.

Library Updates

Terminating programs has been improved with more appropriate
functions (exitWith, exitFailure, and exitSuccess) and a data
structure (ExitCode) to capture a program's return code.
Casting a String to an Int, Integer or a Double now ignores leading
and trailing whitespace. Previously only leading whitespace was ignored.
RTS functions openFile, do_popen, and ARGV are now properly encoded using UTF-8 on Windows.

Language updates

Improved unification by implementing a pattern unification rule
The syntax `{{n}} quotes n without resolving it, allowing short syntax for
defining new names. `{n} still quotes n to an existing name in scope.
A new primitive operator prim__strSubstr for more efficient extraction of
substrings. External code generators should implement this.
The previous syntax for tactic proofs and the previous interactive prover are
now deprecated in favour of reflected elaboration. They will be removed at
some point in the future.
Changed scoping rules for unbound implicits: any name which would be a valid
unbound implicit is now always an unbound implicit. This is much more
resilient to changes in inputs, but does require that function names be
explicitly qualified when in argument position.
Name binding in patterns follows the same rule as name binding for implicits
in types: names which begin with lower case letters, not applied to any
arguments, are treated as bound pattern variables.
Added %deprecate directive, which gives a warning and a message when a
deprecated name is referenced.

Library updates

The Neg class now represents numeric types which can be negative. As such,
the (-) operator and abs have been moved there from Num.
A special version of (-) on Nat requires that the second argument is
smaller than or equal to the first. minus retains the old behaviour,
returning Z if there is an underflow.
The (+), (-), and (*) operations on Fin have been removed.
New Logging Effects have been added to facilitate logging of effectful
programmes.
Elaborator reflection is now a part of the prelude. It is no longer necessary
to import Language.Reflection.Elab.
The PERF effect allows for simple performance metrics to be collected from
Effectful programs.
Some constructors that never actually occurred have been removed from the TT
and Raw reflection datatypes in Language.Reflection.
File IO operations (for example openFile/fread/fwrite) now return
Either FileError ty where the return type was previously ty to indicate
that they may fail.

Tool updates

Records are now shown as records in :doc, rather than as the underlying
datatype
iPKG files have a new option pkgs which takes a comma-separated list of
package names that the idris project depends on. This reduces bloat in the
opts option with multiple package declarations.
iPKG files now allow executable = "your filename here" in addition to the
Existing Executable = yourFilenameHere style. While the unquoted version is
limited to filenames that look like namespaced Idris identifiers
(your.filename.here), the quoted version accepts any valid filename.
Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs)
now adds missing clauses if there is already a definition.

Miscellaneous updates

Disable the deprecation warnings for %elim and old-style tactic scripts with
the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings
flags.

`v0.9.19`

Compare Source

The Idris Reference manual has been fleshed out with content originally found
on the GitHub wiki.
The Show class has been moved into Prelude.Show and augmented with the
method showPrec, which allows correct parenthesization of showed terms. This
comes with the type Prec of precedences and a few helper functions.
New REPL command :printerdepth that sets the pretty-printer to only descend
to some particular depth when printing. The default is set to a high number to
make it less dangerous to experiment with infinite structures. Infinite depth
can be set by calling :printerdepth with no argument.
Compiler output shows applications of >>= in do-notation
fromInteger i where i is an integer constant is now shown just as i in
compiler output
An interactive shell, similar to the prover, for running reflected elaborator
actions. Access it with :elab from the REPL.
New command-line option --highlight that causes Idris to save highlighting
information when successfully type checking. The information is in the same
format sent by the IDE mode, and is saved in a file with the extension ".idh".
Highlighting information is saved by the parser as well, allowing it to
highlight keywords like case, of, let, and do.
Use predicates instead of boolean equality proofs as preconditions on List
functions
More flexible 'case' construct, allowing each branch to target different
types, provided that the case analysis does not affect the form of any
variable used in the right hand side of the case.
Some improvements in interactive editing, particularly in lifting out
definitions and proof search.
Moved System.Interactive, along with getArgs to the Prelude.
Major improvements to reflected elaboration scripts, including the ability to run
them in a declaration context and many bug fixes.
decl syntax rules to allow syntax extensions at the declaration level
Experimental Windows support for console colours

`v0.9.18`

Compare Source

GHC 7.10 compatibility
Add support for bundled toolchains.
Strings are now UTF8 encoded in the default back end
Idris source files are now assumed to be in UTF8, regardless of locale
settings.
Some reorganisation of primitives:
- Buffer and BitVector primitives have been removed (they were not tested
  sufficiently, and lack a maintainer)
- Float has been renamed Double (Float is defined in the Prelude for
  compatibility)
- Externally defined primitives and operations now supported with %extern
  directive, allowing back ends to define their own special purpose primitives
- Ptr and ManagedPtr have been removed and replaced with external primitives
Add %hint function annotation, which allows functions to be used as hints in
proof search for auto arguments. Only functions which return an instance of
a data or record type are allowed as hints.
Syntax rules no longer perform variable capture. Users of effects will need to
explicitly name results in dependent effect signatures instead of using the
default name result.
Pattern-matching lambdas are allowed to be impossible. For example,
Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
requiring a separate lemma.

Case alternatives are allowed to be impossible:

case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }

The default Semigroup and Monoid instances for Maybe are now prioritised
choice, keeping the first success as Alternative does. The version that
collects successes is now a named instance.
:exec REPL command now takes an optional expression to compile and run/show
The return types of Vect.findIndex, Vect.elemIndex and Vect.elemIndexBy
were changed from Maybe Nat to Maybe (Fin n)
A new :browse command shows the contents of a namespace
`{n} is syntax for a quotation of the reflected representation
of the name n. If n is lexically bound, then the resulting
quotation will be for it, whereas if it is not, then it will succeed
with a quotation of the unique global name that matches.
New syntax for records that closely matches our other record-like structures:
type classes. See the updated tutorial for details.
Records can be coinductive. Define coinductive records with the corecord
keyword.
Type class constructors can be assigned user-accessible names. This is done
using the same syntax as record constructors.
if ... then ... else ... is now built-in syntax instead of being defined in
a library. It is shown in REPL output and error messages, rather than its
desugaring.
The desugaring of if ... then ... else ... has been renamed to ifThenElse
from boolElim. This is for consistency with GHC Haskell and
scala-virtualized, and to reflect that if-notation makes sense with non-Bool
datatypes.
Agda-style semantic highlighting is supported over the IDE protocol.
Experimental support for elaborator reflection. Users can now script the
elaborator, for use in code generation and proof automation. This feature is
still under rapid development and is subject to change without notice. See
Language.Reflection.Elab and the %runElab constructs

`v0.9.17`

Compare Source

The --ideslave command line option has been replaced with a --ide-mode
command line option with the same semantics.
A new tactic claim N TY that introduces a new hole named N with type TY
A new tactic unfocus that moves the current hole to the bottom of the
hole stack
Quasiquotation supports the generation of Language.Reflection.Raw terms in
addition to Language.Reflection.TT. Types are used for disambiguation,
defaulting to TT at the REPL.
Language.Reflection.Quotable now takes an extra type parameter which
determines the type to be quoted to. Instances are provided to quote common
types to both TT and Raw.
Library operators have been renamed for consistency with Haskell. In
particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is now
an alias for Functor.map. Correspondingly, ($>) and (<$) have been renamed to
(<*) and (*>). The cascading effects of this rename are that
Algebra.(<*>) has been renamed to Algebra.(<.>) and Matrix.(<.>) is now
Matrix.(<:>).
Binding forms in DSL notation are now given an extra argument: a reflected
representation of the name that the user chose. Specifically, the rewritten
lambda, pi, and let binders will now get an extra argument of type
TTName. This allows more understandable dynamic errors in DSL code and more
readable code generation results.
DSL notation can now be applied with $
Added FFI_Export type which allows Idris functions to be exportoed and
called from foreign code
Instances can now have documentation strings.
Type providers can have documentation strings.
Unification errors now (where possible) contain information about provenance
of a type
New REPL command :core TM that shows the elaborated form of TM along with
its elaborated type using the syntax of TT. IDE mode has a corresponding
command :elaborate-term for serialized terms.
Effectful and IO function names for sending data to STDOUT have been
aligned, semantically.
- print is now for putting showable things to STDOUT.
- printLn is for putting showable things to STDOUT with a new line
- putCharLn for putting a single character to STDOUT, with a new line.
Classes can now be annotated with 'determining parameters' to say which must
be available before resolving instances. Only determining parameters are
checked when checking for overlapping instances.
New package contrib containing things that are less mature or less used than
the contents of base. contrib is not available by default, so you may need
to add -p contrib to your .ipkg file or Idris command line.
Arguments to class instances are now checked for injectivity. Unification
assumes this, so we need to check when instances are defined.

`v0.9.16`

Compare Source

Inductive-inductive definitions are now supported (i.e. simultaneously defined
types where one is indexed by the other.)
Implicits and type class constraints can now appear in scopes other than the
top level.
Importing a module no longer means it is automatically reexported. A new
public modifier has been added to import statements, which will reexport the
names exported from that module.
Implemented @-patterns. A pattern of the form x@p on the left hand side
matches p, with x in scope on the right hand side with value p.
A new tactic sourceLocation that fills the current hole with the current
source code span, if this information is available. If not, it raises an
error.
Better Unicode support for the JavaScript/Node codegen
:search and :apropos commands can now be given optional package lists to
search.
Vect, Fin and So moved out of prelude into base, in modules
Data.Vect, Data.Fin and Data.So respectively.
Several long-standing issues resolved, particularly with pattern matching and
coverage checking.
Modules can now have API documentation strings.

`v0.9.15`

Compare Source

Two new tactics: skip and fail. Skip does nothing, and fail takes a string
as an argument and produces it as an error.
Corresponding reflected tactics Skip and Fail. Reflected Fail takes a
list of ErrorReportParts as an argument, like error handlers produce,
allowing access to the pretty-printer.
Stop showing irrelevant and inaccessible internal names in the interactive
prover.
The proof arguments in the List library functions are now implicit and
solved automatically.
More efficient representation of proof state, leading to faster elaboration of
large expressions.
EXPERIMENTAL Implementation of uniqueness types
Unary negation now desugars to negate, which is a method of the Neg type
class. This allows instances of Num that can't be negative, like Nat, and
it makes correct IEEE Float operations easier to encode. Additionally, unary
negation is now available to DSL authors.
The Java and LLVM backends have been factored out for separate
maintenance. Now, the compiler distribution only ships with the C and
JavaScript backends.
New REPL command :printdef displays the internal definition of a name
New REPL command :pprint pretty-prints a definition or term with LaTeX or
HTML highlighting
Naming of data and type constructors is made consistent across the standard
library (see #1516)
Terms in code blocks inside of documentation strings are now parsed and type
checked. If this succeeds, they are rendered in full color in documentation
lookups, and with semantic highlighting for IDEs.
Fenced code blocks in docs defined with the "example" attribute are rendered
as code examples.
Fenced code blocks declared to be Idris code that fail to parse or type check
now provide error messages to IDE clients.
EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
Engine style)

`v0.9.14`

Compare Source

Tactic for case analysis in proofs
Induction and case tactic now work on expressions
Support for running tests for a package with the tests section of .ipkg files
and the --testpkg command-line option
Clearly distinguish between type providers and postulate providers at the use
site
Allow dependent function syntax to be overridden in dsl blocks, similarly to
functions and let. The keyword for this is pi.
Updated effects library, with simplified API
All new JavaScript backend (avoids callstack overflows)
Add support for %lib directive for NodeJS
Quasiquotes and quasiquote patterns allow easier work with reflected
terms. `(EXPR) quasiquotes EXPR, causing the elaborator to be
used to produce a reflected version of it. Subterms prefixed with ~
are unquoted - on the RHS, they are reflected terms to splice in,
while on the LHS they are patterns.

A quasiquote expression can be given a goal type for the elaborator,
which helps with disambiguation. For instance, `(() : ())
quotes the unit constructor, while `(() : Type) quotes the unit
type. Both goal types and quasiquote are typechecked in the global
environment.
Better inference of unbound implicits

`v0.9.13`

Compare Source

IDE support for retrieving structured information about metavariables
Experimental Bits support for JavaScript
IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
Command line option -e (or --eval) to evaluate expressions without loading
the REPL. This is useful for writing more portable tests.
Many more of the basic functions and datatypes are documented.
Primitive types such as Int and String are documented
Removed javascript lib in favor of idris-hackers/iQuery
Specify codegen for :compile REPL command (e.g. :compile javascript
program.js)
Remove :info REPL command, subsume and enhance its functionality in the :doc command

New (first class) nested record update/access syntax:

record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
record { a->b->c } x -- accesses field, equivalent to c (b (a x))

The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
:apropos now accepts space-delimited lists of query items, and searches for
the conjunction of its inputs. It also accepts binder syntax as search
strings - for instance, -> finds functions.
Totality errors are now treated as warnings until code generation time, when
they become errors again. This allows users to use the interactive editing
features to fix totality issues, but no programs that violate the stated
assumptions will actually run.
Added :makelemma command, which adds a new top level definition to solve a
metavariable.
Extend :addclause to add instance bodies as well as definitions
Reverse parameters to BoundedList -- now matches Vect, and is easier to
instantiate classes.
Move foldl into Foldable so it can be overridden.
Experimental :search REPL command for finding functions by type

Internal changes

New implementation of erasure

`v0.9.12`

Compare Source

Proof search now works for metavariables in types, giving some interactive
type inference.
New Lazy type, replacing laziness annotations.
JavaScript and Node codegen now understand the %include directive.
Concept of null is now understood in the JavaScript and Node codegen.
Lots of performance patches for generated JavaScript.
New commands :eval (:e) and :type (:t) in the prover, which either
normalise or show the type of expressions.
Allow type providers to return postulates in addition to terms.
Syntax for dealing with match failure in <- and pattern matching let.

New syntax for inline documentation. Documentation starts with |||, and
arguments are documented by preceding their name with @. Example:

||| Add two natural numbers
||| @&#8203; n the first number (examined by the function)
||| @&#8203; m the second number (not examined)
plus (n, m : Nat) -> Nat

Allow the auto-solve behaviour in the prover to be disabled, for easier
debugging of proof automation. Use :set autosolve and :unset autosolve.
Updated effects library
New :apropos command at REPL to search documentation, names, and types
Unification errors are now slightly more informative
Support mixed induction/coinduction with Inf type
Add covering function option, which checks whether a function and all
descendants cover all possible inputs

`v0.9.11`

Compare Source

Agda-style equational reasoning (in Syntax.PreorderReasoning)
'case' construct now abstracts over the scrutinee in its type
Added label type 'name (equivalent to the empty type). This is intended for
field/effect disambiguation. "name" can be any valid identifier. Two labels
are definitionally equal if they have the same name.
General improvements in error messages, especially %error_reverse annotation,
which allows a hint as to how to display a term in error messages
--ideslave mode now transmits semantic information about many of the strings
that it emits, which can be used by clients to implement semantic highlighting
like that of the REPL. This has been implemented in the Emacs mode and the IRC
bot, which can serve as examples.
New expression form: with NAME EXPR privileges the namespace NAME when
disambiguating overloaded names. For example, it is possible to write with Vect [1,2,3] at the REPL instead of the (Vect _ _) [1,2,3], because the
Vect constructors are defined in a namespace called Vect.
assert_smaller internal function, which marks an expression as smaller than
a pattern for use in totality checking. e.g. assert_smaller (x :: xs) (f xs) asserts that f xs will always be structurally smaller than (x :: xs)
assert_total internal function, which marks a subexpression as assumed to be
total, e.g assert_total (tail (x :: xs)).
Terminal width is automatically detected if Idris is compiled with curses
support. If curses is not available, automatic mode assumes 80 columns.
Changed argument order for Prelude.Either.either.
Experimental neweffects'library, intended to replace effects in the next
release.

Internal changes

Faster elaboration
Smaller .ibc files
Pretty-printer now used for all term output

Configuration

📅 Schedule: Branch creation - At any time (no schedule defined), Automerge - At any time (no schedule defined).

🚦 Automerge: Disabled by config. Please merge this manually once you are satisfied.

♻ Rebasing: Whenever PR becomes conflicted, or you tick the rebase/retry checkbox.

🔕 Ignore: Close this PR and you won't be reminded about this update again.

If you want to rebase/retry this PR, click this checkbox.

This PR has been generated by Mend Renovate. View repository job log here.

kachick · 2022-07-14T19:33:31Z

🎉

Update dependency idris-lang/Idris-dev to v1

46393e7

renovate bot added dependencies renovate labels Jul 14, 2022

kachick merged commit ecd3dc6 into main Jul 14, 2022

kachick deleted the renovate/idris-lang-idris-dev-1.x branch July 14, 2022 19:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update dependency idris-lang/Idris-dev to v1 #20

Update dependency idris-lang/Idris-dev to v1 #20

renovate bot commented Jul 14, 2022

kachick commented Jul 14, 2022

Update dependency idris-lang/Idris-dev to v1 #20

Update dependency idris-lang/Idris-dev to v1 #20

Conversation

renovate bot commented Jul 14, 2022

Release Notes

Library updates

Tool updates

Miscellaneous updates

Tool updates

Language updates

Library updates

Tool updates

Language updates

Library Updates

Tool Updates

Packaging Updates

Library Updates

Tool Updates

Library Updates

Tool Updates

Miscellaneous Updates

Language updates

Tool Updates

Library Updates

Language updates

Library updates

Tool updates

Miscellaneous updates

Internal changes

Internal changes

Configuration

kachick commented Jul 14, 2022