G. Allais
0194539ef7
[ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings ( #2819 )
...
* [ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings
* [ fix ] the point is to test whitespace being ignored
* [ fix ] golden values
2022-12-17 18:12:39 +00:00
G. Allais
2f55a3ef8a
[ fix ] elaboration of records' telescopes of parameters ( #2816 )
2022-12-15 17:55:50 +00:00
Justus Matthiesen
e673d05a67
[ fix ] jump-to-definition (":name-at" IDE command) ( #2811 )
2022-12-09 17:02:57 +00:00
Markus Pfeiffer
c3bbdb30a1
Add mustWork in GADT data declaration parser ( #2805 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-12-09 16:04:11 +00:00
Guillaume Allais
1d73e359e0
[ ci ] only run latest job
...
As discussed on discord a while ago, this kills runs when a new
commit lands on the same branch. It should save some CI ressources.
2022-12-09 14:40:14 +00:00
Guillaume Allais
caeb55b495
[ ci ] fix initialise step
...
Github is now failing hard on multiline commit messages it seems.
2022-12-09 14:40:14 +00:00
Guillaume Allais
9bcaa104f3
[ new ] logging topics autocompletion in the emacs REPL
2022-12-08 21:06:39 +00:00
locriacyber
cb30d7cda8
Install *.ttm on idris2 --install ( #2796 )
...
Co-authored-by: Justus Matthiesen <mail@justusmatthiesen.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-12-08 21:06:17 +00:00
Thomas E. Hansen
7a41606573
[ admin ] Fix PR template
2022-12-08 11:24:37 +00:00
Ruslan
d44ddc7f11
Let qualified do-notation apply to pure and to idiom brackets ( #2786 )
2022-12-07 22:27:58 +00:00
Ellis Kesterton
9931f35b6b
Improve parser error messages when using reserved identifiers in decls ( #2803 )
...
Co-authored-by: Ellis Kesterton <erk4@st-andrews.ac.uk>
2022-12-07 16:09:26 +00:00
G. Allais
32f92746b3
[ perf ] compile Core.CompileExpr.Pretty faster ( #2800 )
2022-12-07 10:08:31 +00:00
Guillaume Allais
085ea348ae
[ perf ] use integers in the buffer state
2022-12-06 21:13:55 +00:00
Guillaume Allais
ebc406c519
[ perf ] cherrypick fast weakenNVar from yaffle
2022-12-06 12:28:16 +00:00
Guillaume Allais
001f48fba8
[ test ] for io_bind inlining
2022-12-06 11:55:28 +00:00
G. Allais
fcbd9e9190
[ fix #2794 ] Do not ignore notinline lets in identity detection ( #2795 )
2022-12-06 11:41:30 +00:00
Denis Buzdalov
ff6afb0c59
[ minor ] Make NotBothZero parameter of standard gcd to be erased
2022-12-05 15:10:16 +00:00
Denis Buzdalov
8d7b993cca
[ cleanup ] Use several library functions instead of their code
2022-12-05 15:10:16 +00:00
Denis Buzdalov
33fe3f44db
[ cleanup ] Clean up existing code in the Arrow module
2022-12-05 15:10:16 +00:00
Denis Buzdalov
c8f625cad9
[ typo ] Fix typo in an issue template
2022-12-05 15:10:16 +00:00
Guillaume Allais
99eda4dd2b
[ papers ] fill last hole in lambda pi formalisation
2022-12-05 15:02:04 +00:00
Denis Buzdalov
59aadd650f
[ ci ] Replace deprecated feature with its functional equivalent
2022-12-01 20:35:22 +00:00
G. Allais
255cce9d9c
[ ci ] fix katla scripts following the TTC version subdirectory ( #2787 )
2022-12-01 20:20:01 +00:00
G. Allais
85bb822f3b
[ perf ] manually eta-expand unsaturated io_bind calls ( #2785 )
2022-12-01 15:31:00 +00:00
G. Allais
f96c5ca596
[ papers ] LambdaPi ( #2780 )
2022-12-01 13:48:48 +00:00
Steve Dunham
f443723f4e
[ parser ] fix issue where indentation is not checked in record parameters
2022-11-25 08:22:37 +00:00
Tim Engler
69f680e10a
Update introapp.rst
...
Further explain why the App passed to ``run`` can't throw an exception.
2022-11-21 10:55:52 +00:00
0xd34df00d
c6a8c9e7a7
[ base ] Move the worker outside of the Vect's reverse definition
2022-11-21 10:52:47 +00:00
Robert Wright
7d9d39c045
Use escaped version of system in Idris src
2022-11-21 10:51:43 +00:00
Robert Wright
edacf65182
Bump version of Idris used in CI
2022-11-21 10:51:43 +00:00
Steve Dunham
56a9bc6be4
[ error ] Improve locality of parse errors in implicit arguments
2022-11-21 10:40:40 +00:00
Tim Engler
bff18428b4
Added seqL to Control.App and updated docs to fix #2761
...
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
2022-11-21 10:39:43 +00:00
Marek L
0e657aeba1
[ ide-mode ] Do not include whole error message in building file
...
display result message.
Why:
Makes the error message being displayed twice in Emacs.
This change aligns IDEMode/REPL.idr with Idris/REPL.idr which
works as expected.
Relates to:
https://github.com/idris-hackers/idris-mode/pull/563
2022-11-21 10:34:23 +00:00
Tim Engler
811dcd864f
Similar to pull request #2136 , commit 8ffad8878f
...
except now packageDirs keeps getting added to. So rather than just
saving and replacing extraDirs, I'm replacing the whole dirs directory
within defs.options
2022-11-21 10:33:56 +00:00
Kamiλ Shakirov
dbb3853484
Do not build docs for papers
2022-11-15 16:38:13 +01:00
Kamil Shakirov
73733f03ff
Cleanup after rebase
2022-11-15 16:38:13 +01:00
Kamil Shakirov
8a35a9dc74
Fix IDRIS2_BOOT_PATH
2022-11-15 16:38:13 +01:00
Kamil Shakirov
8ebec8ebae
Make linter happy
2022-11-15 16:38:13 +01:00
Kamil Shakirov
7c6ab4e1b6
Do not use IDRIS2_BOOT_PATH in bootstrap-stage2.sh
...
It is not needed as bootstrapped intermediate version knows where to find import files.
`IDRIS2_BOOT_PATH` wasn't pointing to the correct directories anyways.
2022-11-15 16:38:13 +01:00
Kamil Shakirov
502aa6f4fc
Do not install papers library
2022-11-15 16:38:13 +01:00
Kamil Shakirov
dccb80d0bf
[ fix ] Fix Makefile targets for linear and papers libraries
2022-11-15 16:38:13 +01:00
Hattori, Hiroki
5c9f8e36a1
[ RefC ] Add 16 and 32 bit access to base/Data.Buffer . ( #2609 )
...
* Fix symbom mangling
* Revert "Fix symbom mangling"
This reverts commit 6481e80155#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>
2022-11-15 12:15:06 +01:00
CodingCellist
037b48eb29
[ re #2649 ] Update CHANGELOG ( #2765 )
2022-11-15 10:58:00 +01:00
CodingCellist
70ef197cf6
[ base ] Deprecate setByte in favour of setBits8 ( #2764 )
...
* [ 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.
2022-11-15 10:42:07 +01:00
Denis Buzdalov
f5f7e2eb80
[ error ] Make failing IAlternative w/ FirstSuccess print all errors
2022-11-15 10:28:59 +01:00
Tim Engler
774529fd70
Altered docs for `Exception` to reflect the code changes in Control.App
...
Exception is no longer an interface but just a synonym of ``HasErr``. Updated docs to reflect this.
2022-11-13 09:28:43 +00:00
Zoe Stafford
d0e761d63b
Merge pull request #2772 from dunhamsteve/issue2769
...
[ error ] Improve error messages on record and interface constructors (#2769 )
2022-11-13 09:17:40 +00:00
Steve Dunham
85c93c8018
[ error ] Add FC for errors on interface constructors ( #2769 )
2022-11-12 22:17:42 -08:00
Steve Dunham
ea733181c5
[ error ] Add an FC to record constructors for better error messages ( #2769 )
2022-11-12 21:59:16 -08:00
Zoe Stafford
d1e1d0636c
Merge pull request #2767 from madman-bob/erase-fin-fromInteger-upper-bound
...
Erase Fin fromInteger upper bound
2022-11-12 09:45:51 +00:00
