Commit Graph

161 Commits

Author SHA1 Message Date
Zoe Stafford
ff822a747b
Js char io (#2887)
* Implement `{get,put}Char` for javascript backend

* Update changelog
2023-02-13 15:48:07 +00:00
Andy Lok
a1d0c7c478 [ fix #2087 ] Fix multiline string on CRLF 2023-02-13 14:21:09 +00:00
Mathew Polzin
2e9c7fb8b5
Create a separate Makefile for the Idris 2 support libraries. (#2869)
* Create a separate Makefile for the Idris 2 support libraries.

* Update INSTALL.md

* satisfy natural language linter

* Add to CHANGELOG

* Update CHANGELOG.md
2023-02-09 16:49:49 -06:00
G. Allais
7c66d10eae
[ papers ] Type-based Divide & Conquer (#2860) 2023-02-08 17:19:24 +00:00
Justus Matthiesen
7eed472ac5 [ termination ] update changelog 2023-02-08 16:13:04 +00:00
G. Allais
fba9f16a1c
[ fix ] positivity checker: assert_total & Lazy (#2876) 2023-02-07 12:35:33 +00:00
Stefan Höck
f6a731695d
[ new ] constructor plus trivial impl for Interpolation (#2871)
* [ new ] constructor plus trivial impl for Interpolation

* [ doc ] update CHANGELOG

* [ test ] adjust expected test output
2023-02-04 07:47:28 -06:00
Mathew Polzin
ad12f8335c
[ new ] popen/pclose for the NodeJS backend. (#2857)
* 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.
2023-01-30 09:38:42 -06:00
G. Allais
966a4813fb
[ fix ] respect totality annotations for data (#2862) 2023-01-26 11:03:22 +00:00
G. Allais
ea4a4c0f85
[ base ] fix the definition of die (#2854) 2023-01-19 11:09:28 +00:00
Mathew Polzin
24ac56de88
Moving Data.List.HasLength into base (#2844) 2023-01-16 00:07:21 -06:00
Denis Buzdalov
936b7270ae [ prelude ] Add lacking implementation of Traversable for Pair 2023-01-09 15:56:21 +00:00
Mathew Polzin
4005b40a95
[new] Vect.Quantifiers.All QoL (#2843)
* 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.
2023-01-09 00:57:00 -06:00
Mathew Polzin
63a22b819d
[docs] javascript FFIs and packaging of JS or C support files (#2842)
* 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.
2023-01-07 21:40:47 +00:00
Stefan Höck
8db12f5a49
[ performance ] improve some Char functions (#2839) 2023-01-06 09:08:38 +00:00
Zoe Stafford
217271a623
Js shebang (#2830)
* 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...
2022-12-22 14:56:44 +00:00
Stefan Höck
d2c8cf461b
[ performance ] Compile non-recursive top-level constants to constants in Chez (#2817) 2022-12-21 08:48:20 +00:00
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
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
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
dc1662ddf1 [ doc ] Add :doc for unquotes
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
2022-11-04 14:03:21 +00:00
Edwin Brady
102d7ebc18
Update version number in CHANGELOG (#2734) 2022-10-27 16:41:13 +01:00
CodingCellist
59460c2f46
[ admin ] Update CHANGELOG and CONTRIBUTORS (#2703)
* [ 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>
2022-10-21 16:48:37 +02:00
CodingCellist
47c2de3148
[ repl ] Add the ability to get detailed help, e.g. :help :help (#2722)
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>
2022-10-21 14:35:33 +02:00
CodingCellist
bb602643b1
[ fix #2712 ] Don't consider CyclicMeta recoverable (#2713) 2022-10-14 14:57:55 +01:00
Thomas E. Hansen
a598fec4f7 [ repl ] Add :import command 2022-10-13 11:31:05 +02:00
G. Allais
1f3809c49a
[ re #2675 ] Do not build libs/{contribs,papers} during bootstrap (#2677)
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
2022-10-04 13:37:45 +01:00
Sam Phillips
358c107c53 Update CHANGELOG.md and CONTRIBUTORS 2022-10-04 10:24:27 +02:00
0xd34df00d
c2dd824c58 [ base ] Implement Uninhabited for impossible Pointwise equalities 2022-10-02 21:41:26 +01:00
stefan-hoeck
9aa9e98a35 [ lint ] this is so silly 2022-09-27 12:29:09 +02:00
stefan-hoeck
f04a29926d [ doc ] update changelog 2022-09-27 12:15:17 +02:00
Zoe Stafford
02dfd6ff6c
Trans deps v3 (#2584)
* 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>
2022-09-09 07:08:39 +01:00
0xd34df00d
b3c80e0765 [ base ] Add finToNatEqualityAsPointwise, an inverse of finToNatQuotient 2022-09-05 12:45:28 +01:00
Adowrath
1914606d40 Fix connect in linear module and add bytes-specific functions 2022-09-01 12:23:29 +01:00
Zoe Stafford
86c060ef13
Reimplement %nomangle in terms of %export (#2604)
* Reimplement %nomangle in terms of %export
Also deprecate %nomangle

* [ lint ] fix linter errors
2022-08-15 13:26:06 +01:00
G. Allais
84a504738c
[ doc ] add comments to generated javascript (#2594) 2022-07-18 17:30:56 +01:00
Denis Buzdalov
c03a39789f [ breaking ] Make arguments of runRWST like in other transformers
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.
2022-07-07 15:19:41 +01:00
Thomas E. Hansen
268a3520f3 [ base ] Port most of List.Quantifiers to List1
This doesn't include `Interleaving` and `Split`.
2022-06-09 09:05:10 +02:00
Thomas E. Hansen
5da3bc7d7c [ base ] Port List.Elem to List1 2022-06-09 09:05:10 +02:00
Zoe Stafford
b9001439b3 Revert "Transitive dependencies v2 (#2496)"
This reverts commit 51f952714d.
2022-06-08 06:35:39 +01:00
Zoe Stafford
51f952714d
Transitive dependencies v2 (#2496)
* 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
2022-06-07 14:31:14 +01:00
Zoe Stafford
932a24baa1 Revert "make depends collect all transitive dependencies (#2469)"
This reverts commit fde6269c7e.
2022-05-21 06:49:07 +01:00
Zoe Stafford
fde6269c7e
make depends collect all transitive dependencies (#2469)
* 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
2022-05-20 16:20:54 +01:00
Denis Buzdalov
72f0a2ab09 [ re #950 ] Remove redunant legacy data definition
`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).
2022-05-14 08:24:20 +01:00
CodingCellist
36e38860b7
[ contrib ] Implement Show ParsingError (#2407) 2022-04-09 12:37:45 +01:00
Thomas E. Hansen
a644a85a57 [ base ] public export quantifier functions 2022-04-04 13:24:12 +02:00