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.
* [ 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>
* 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.
* make color output toggling simpler and also more robust
* don't unintentionally assert that tests are run in an environment where colors are turned on.
* Update src/Idris/Env.idr
* 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.
Also updated test real002 to use the actual Control.App from
libs/base/Control/App.idr. Before it was using a different version that
existed within its test directory, tests/idris2/real002/Control/App.idr
* 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.
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>
This completes the implementation of the examples in the paper
"Applications of Applicative Proof Search" (Liam O'Connor, 2016).
Unfortunately, the final example is an example of something that _can_
be expressed, but _cannot_ be model-checked by the approach in the
paper.
(Side note on `petersonsCorrect`: The paper mentions that it checks in
~3 minutes on a 2013 MacBook Pro. Assuming they mean "type-checks", this
is roughly consistent with our observations of just short of 2 minutes.
I doubt that they evaluated it, since an attempt at doing this on a
reasonably modern server (Intel Xeon Gold 5220R, 502 GB of RAM) was
killed after just over 3 hours, producing the following resource log:
Command exited with non-zero status 255
Time: 11320.46s user, 35.12s system, 3h09m46s elapsed, 99%CPU
Memory: 57644016 Kbytes RAM
)
On average across 10 runs on an Intel Core i7-8750H with 15.2GB of
available system memory (16GB installed in system), type-checking
`libs/papers/Search/GCL.idr` WITH `petersonsCorrect` takes:
* 1 minute 48.7 seconds, consuming 3.92GB of RAM
By contrast, commenting `petersonsCorrect` out results in type-checking
taking on average (same #runs, same config):
* 0 minutes 1.2 seconds, consuming 0.25GB of RAM
And good luck trying to evaluate the thing!
(This might be a good performance test at some point, but uh, we're not
there yet...)
Thanks to the debug info supplied by #2673, I was able to spot which
functions were blocking and `public import` the relevant files in
`papers/Search/Properties.idr`.
As a result the GCL file now type-checks, albeit extremely slowly!
I stopped an evaluation of `petersonsCorrect` at the REPL after 15
minutes and ~14GB of RAM consumed.
* Currying the `ops` function makes the totality checker spot that it
_is_ actually total.
* Instance arguments are heavily abused in the paper, along with
implicit `open` magic, but Idris allows no such ~~luxury~~
obfuscation, so we have to pass things explicitly.
* `decSo` is not `public export`ed, so we have to define `IsTT` by
pattern-matching (which is fine).
Currently, it gets stuck on checking `petersonsCorrect` for some,
currently unknown, reason. (And the log output is loooooong O.O)
Once again, this would not have been possible without gallais insigths.
Many thanks!
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
* Switch to `Inf` to actually use codata/corecursion.
* Add `%hint`s to mark the interface implementations as such, despite
use of a record for `DepthInv` (this is necessary for other stuff).
* Pass in `Oh` to `reaches10.evidence` in order for things to work.
With huge thanks to gallais for helping me put the final things in
place!
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Termination checking needs figuring out. There is some funky stuff going
on with the half-deciders and their constructors. Other than that, I
**think** it's nearly done. God knows how much RAM it'll take though...
