* Change the printing of namespaced operator to show
parenthesis around operators
* Update warning when conflicting fixities are found
* Do not warn about redundant but compatible fixities
* [ fix ] Programmer-provided terms should be alwaysReduce
This ports Edwin's commit that fixes the original issue back to Idris
Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
* [ tests ] Added regression test for #1878
* Updated CHANGELOG.md and CONTRIBUTORS
---------
Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
This is required due to `Lazy` now being a reserved compiler primitive.
N.B. This may also break other dependencies and/or tools. Notably stuff
outwith the Idris2 upstream. There's been some discussion in #2987.
* [ fix ] collect constructors on LHS of cases alts
* [ tests ] Updated expected
These functions do refer to these constructors at runtime, so this is the correct output
* Update CHANGELOG.md
* [test] update test output again
* [ new ] Implement bit-rotation operators
Whereas `shiftR` and `shiftL` throw bits off the edge, the `rotR` and
`rotL` operations wrap the bits around to the start of the bit-stream.
* [ test ] visualise bit patterns instead
* [ fix ] print bit patterns the right way around
---------
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
* Create a separate Makefile for the Idris 2 support libraries.
* Update INSTALL.md
* satisfy natural language linter
* Add to CHANGELOG
* Update CHANGELOG.md
* implement popen and pclose (to an extent) for NodeJS
* bring node020 back into tests.
* ah, I see what was being done here. Fix the idris for the test.
* fix test's unreachable clause warning
* fix expectation
* Add note to CHANGELOG
* small tweaks to get popen into merge-ready state.
* Add Show for Vect.All
* Add an alias for HVect to Data.Vect.Quantifiers.All
* Add a few utilities for Vect.Quantifiers.All to make it more at home in listy uses.
* Add CHANGELOG entries.
* Add documentation on javascript FFIs and packaging of JS or C support files.
* Add to changelog.
* line length
* add some detail about the install directories for packages.
* add shebang to outputted node file
after `chmod`ing the file, it can be run directly
ie `./build/exec/test` rather than `node ./build/exec/test``
* update CHANGELOG.md
* [ linter ]
* [ linter ] again...
* Fix symbom mangling
* Revert "Fix symbom mangling"
This reverts commit 6481e80155.
* Fix typo
* [RefC] Add missed prims of setBuffer* .
* [ fix ] formatting
* [ re #2609 ] Use 'UInt' instead of 'Word'
More descriptive/to the point / Less assumed knowledge.
There are no *LE suffixes for UInt8, since endianness is to do with
multiple bytes and UInt8 is a single one.
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
* [ base ] Deprecate setByte in favour of setBits8
Deprecate getByte; fix Core.Binary.Prims
Along with `setByte`, the `getByte` function should similarly be
deprecated since it also assumes the value will have the given size,
rather than guaranteeing it in the type.
CI highlighted some required changes in `Core.Binary.Prims` thanks to
`-Werror`. The fix was to add some `cast` calls where the old `getByte`
and `setByte` used to be.
The RefC buffer test will need updating once we remove the functions
completely. Added a note for future peeps.
* [ re #2742 ] Count no. processors online rather than configured
Seems there might be some oddities with what is reported when, e.g.
reporting the maximum number of processors supported by the currently
installed motherboard, regardless of which processor is socketed.
* [ #2754 ] Update CHANGELOG
* [ 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).
