Commit Graph

3617 Commits

Author SHA1 Message Date
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.

* 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>
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
Robert Wright
b2c42280bb Erase Fin fromInteger upper bound 2022-11-11 15:34:58 +00:00
CodingCellist
9cd92f1fc4
[ re #2742 ] Count no. processors online rather than configured (#2754)
* [ 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
2022-11-11 11:12:24 +01:00
Thomas E. Hansen
643c4be55f [ re #2649 ] Describe test naming pattern 2022-11-11 09:33:09 +01:00
Gregory Werbin
e0d6d0881e Remove unnecessary use of LDFLAGS 2022-11-11 09:33:09 +01:00
Gregory Werbin
b81f5280c1 Use consistent punctuation & indentation 2022-11-11 09:33:09 +01:00
Gregory Werbin
ecac93081b Add CPPFLAGS for consistency? 2022-11-11 09:33:09 +01:00
Gregory Werbin
c5c842726a Add support for standard C env vars
Also, organize the env var listing a bit more.
2022-11-11 09:33:09 +01:00
Gregory Werbin
1020437aad Use CPPFLAGS when needed 2022-11-11 09:33:09 +01:00
Mathew Polzin
25388ecac2 look for lib folders in package directories. 2022-11-04 18:10:03 -05:00
Guillaume Allais
8556c81014 [ new ] typed ABT 2022-11-04 16:20:46 +00:00
Thomas E. Hansen
dc1662ddf1 [ doc ] Add :doc for unquotes
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
2022-11-04 14:03:21 +00:00
G. Allais
fd46e31da3
[ new ] typed Krivine (#2749) 2022-11-04 10:05:31 +00:00
Stefan Höck
b5decdf729
[ new ] add --ttc-version command (#2752)
* [ new ] add --ttc-version command

* [ fix ] -v should still print version
2022-11-04 06:45:49 +00:00
stefan-hoeck
6f5b19c389 [ cleanup ] bifoldMap already in Prelude 2022-11-03 14:11:15 +00:00
Andy Lok
ddcbe795c6
[ fix ] DISallow grouping pi with different types (#2680)
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-11-02 14:33:19 +00:00
G. Allais
ad817538e0
[ new ] typed SECD (#2743) 2022-11-02 12:58:13 +00:00
Stefan Höck
9c9ffe4a31
[ fix ] isue 2745 (#2747)
* [ fix ] .ipkg install dir

* [ test ] .ipkg install dir

* [ doc ] update CHECKLIST

* [ doc ] add explanation to pkg016 test

* [ cleanup ] no need to clutter CHECKLIST
2022-11-02 12:01:19 +00:00