* [ admin ] Update CHANGELOG and CONTRIBUTORS
We really need to do a release at some point...
* [ ci ] Don't check capitalised proper names in links and code
Sometimes hyperlinks and code-blocks just don't use the "proper"
capitalisation (e.g. `.html` vs `.HTML`), and that's okay.
(or even critical as links may not be found without "incorrect" format)
* [ ci ] Don't check terminology in links and code-blocks
Hopefully this is the right fix for the problem in #2703
* [ ci ] 3rd attempt at fixing nl linter
* [ ci ] Attempt no. 4 at fixing nl linter
* [ ci ] Point NL linter at YAML config file
Was that actually it??
* Update CHANGELOG.md
* Add note about forward declaration of records
* [ admin ] Add PR template with CHANGELOG reminder
To hopefully help mitigate big crawl-throughs of what's changed,
à la #2703.
* [ admin ] Reflow CHANGELOG to 80 characters where possible
Only done for the "next version" changes for the sake of diff size.
(Personally, I'd want to have the linter enforce this, but that might be
too extreme; there's already a note in the CI config complaining about
line length...)
* [ admin ] Make linter happy
It never ends...
Co-authored-by: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Co-authored-by: Steve Dunham <dunhamsteve@gmail.com>
A common issue for users is that the behaviour of the various repl
commands are not documented anywhere despite some of them having complex
behaviour (e.g. `:set` which accepts a specific set of options). This
implements the ability to call `:?|:h|:help` on repl commands to request
detailed help for a specific repl command, while preserving the
behaviour that calling the help command without any arguments prints the
general help text.
Generic help is defined as the first line of the help text.
Detailed help is defined as the entire help text.
This means that `:help :t`, for example, does not error (there is no
detailed help) but instead just prints the single line of help text.
* [ repl ] Use unlines for detailed help (see #2087)
Ideally, the lines affected should be multiline strings. But for some
arcane reason, newlines in those get swallowed in Nix and Windows
**CI** only Ô.o
This was already documented in issue #2087.
* [ new ] --except for golden testing lib
To allow CI to pass despite #2087
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
* Actually install the version
This should make things start working
* [ fix ] use backtracking to resolve transitive dependencies
* [ fix ] use backtracking to resolve dependencies
* [ fix ] test pkg006
* Fix missing import
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
Put the `RWST` argument to be the last one. This makes such functions
to be easier used in point-free compositions and to be easily
interchangeable with existing `runStateT`-like functions.
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
* Actually install the version
This should make things start working
* make `depends` collect all transitive dependencies
This happens by installing the (modified) ipkg file along with ttc files
* [ fix ] parsing a package shouldn't always set sourceDir
* linter *sigh*
* Fix test, add changelog
`asDepends` has been changed to `setSrc` as that is for me more intuitive
in idris2/pkg006 the version field was removed from the ipkgs of bar-baz and quux
as idris now expects the version to match the folder
idris2/pkg010 explicitly disables incremental compilation, to prevent extra log info
* (hopefully) fix idris2/pkg13 test on windows
`Given` with `Always` from Idris 1 library are completely overridden by
`IsYes` and `ItIsYes` respectively, which have a more common naming.
This, however, may break some very old code (fixed by a trivial rename).
* [ CHANGELOG ] Fix CHANGELOG.
Apparently, the older version of record syntax has now been deprectated.
This was not reflected in the CHANGELOG, and the CHANGELOG entry for an earlier version of Idris2 was erroneously updated to use the new syntax.
THis commit fixes the CHANGELOG.
* deprecate Data.Nat.Order.decideLTE
* Add properties for LTE/GTE that produce the difference.
* remove deprecated function now that it is available in the base library.
* remove two deprecated lines.
* remove module deprecated since v0.4.0
* fix prelude reference to renamed primitive.
* finish removing Data.Num.Implementations
* remove deprecated dirEntry function.
* remove deprecated fastAppend. Update CHANGELOG.
* replace fastAppend in test case
* replace fastAppend uses in compiler.
* remove new properties that weren't actually very new.
* Update documentation and changelog for string interpolation
* Fix typo in changelog
* fix documentation about desugaring of interpolate
* Update CHANGELOG.md
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
This is for compiled evaluation at compile-time, for full normalisation. You can try it by setting the evaluation mode to scheme (that is, :set eval scheme at the REPL). It's certainly an order of magnitude faster than the standard evaluator, based on my playing around with it, although still quite a bit slower than compilation for various reasons, including:
* It has to evaluate under binders, and therefore deal with blocked symbols
* It has to maintain enough information to be able to read back a Term from the evaluated scheme object, which means retaining things like types and other metadata
* We can't do a lot of the optimisations we'd do for runtime evaluation particularly setting things up so we don't need to do arity checking
Also added a new option evaltiming (set with :set evaltiming) to display how long evaluation itself takes, which is handy for checking performance.
I also don't think we should aim to replace the standard evaluator, in general, at least not for a while, because that will involve rewriting a lot of things and working out how to make it work as Call By Name (which is clearly possible, but fiddly).
Still, it's going to be interesting to experiment with it! I think it will be a good idea to use it for elaborator reflection and type providers when we eventually get around to implementing them.
Original commit details:
* Add ability to evaluate open terms via Scheme
Still lots of polish and more formal testing to do here before we can
use it in practice, but you can still use ':scheme <term>' at the REPL
to evaluate an expression by compiling to scheme then reading back the
result.
Also added 'evaltiming' option at the REPL, which, when set, displays
how long normalisaton takes (doesn't count resugaring, just the
normalisation step).
* Add scheme evaluation mode
Different when evaluating everything, vs only evaluating visible things.
We want the latter when type checking, the former at the REPL.
* Bring support.rkt up to date
A couple of missing things required for interfacing with scheme objects
* More Scheme readback machinery
We need these things in the next version so that the next-but-one
version can have a scheme evaluator!
* Add top level interface to scheme based normaliser
Also check it's available - currently chez only - and revert to the
default slow normaliser if it's not.
* Bring Context up to date with changes in main
* Now need Idris 0.5.0 to build
* Add SNF type for scheme values
This will allow us to incrementally evaluate under lambdas, which will
be useful for elaborator reflection and type providers.
* Add Quote for scheme evaluator
So, we can now get a weak head normal form, and evaluate the scope of
a binder when we have an argument to plug in, or just quote back the
whole thing.
* Add new 'scheme' evaluator mode at the REPL
Replacing the temporary 'TmpScheme', this is a better way to try out the
scheme based evaluator
* Fix name generation for new UN format
* Add scheme evaluator support to Racket
* Add another scheme eval test
With metavariables this time
* evaltiming now times execution too
This was handy for finding out the difference between the scheme based
evaluator and compilation. Compilation was something like 20 times
faster in my little test, so that'd be about 4-500 times faster than the
standard evaluator. Ouch!
* Fix whitespace errors
* Error handling when trying to evaluate Scheme
* Update version numbers and bootstrap scheme
* Use wall clock time for search timeouts
That was always the intention in any case, rather than the process time.
* Small fix for incremental compilation
In incremental mode we need to add the arity of a compiled definition to
the hash, because if that changes, we need to rebuild the dependencies
too to make sure the arity is correct at the call site
* Fix indentation in CHANGELOG
