Commit Graph

2165 Commits

Author SHA1 Message Date
zseri
96d914b93d Nix: improve buildIdris
- DRY
- idris2 is used as a compiler, should thus be in nativeBuildInputs
2021-06-30 15:33:37 +01:00
John Mager
dc755e1df5 Pretty instances for IntX 2021-06-30 08:18:37 +01:00
Nick Drozd
9cb20f3653
Clean up some assert_total instances (#1644) 2021-06-29 22:05:40 +01:00
Stefan Höck
39d596f3b9
[ new ] Support reflecting on new intX types (#1642) 2021-06-29 20:58:41 +01:00
G. Allais
168a69bdcf
[ ci ] just dump everything into a single file already (#1645) 2021-06-29 19:42:48 +01:00
Guillaume ALLAIS
a1ae5148b6 [ actions ] add quick check step 2021-06-29 11:36:22 +01:00
John Mager
8638849d26 [ fix ] Nix uses proper version 2021-06-29 09:10:24 +01:00
Stefan Höck
f5bcc81115
[ new ] Add FromChar and FromDouble interfaces to the prelude (#1641) 2021-06-29 08:37:02 +01:00
Stiopa Koltsov
35638048a3 Test for System.Info.os 2021-06-29 08:34:53 +01:00
kasiaMarek
6f9b926b1b
module Data.SnocList.Elem (#1478)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-06-28 20:34:39 +01:00
Stiopa Koltsov
6be2a54c0a Delete tyspec functions
I suspect this function is left there accidentally after FFI was
refactored.

These functions can mislead about how FFI works.

Note these functions are private (not exported) and not used.  Idris
compiler could emit a warning about such functions.
2021-06-28 20:01:19 +01:00
Stefan Höck
6ed266d306
[ new ] Missing integer type interfaces (#1629)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-06-28 20:00:10 +01:00
Edwin Brady
76715acc1f
Don't need benchmarks in the release (#1600)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-06-28 19:07:24 +01:00
Stiopa Koltsov
855ee3cbd0 Ignore @generated in super-linter
Super-linter supports it now
2021-06-28 17:26:32 +01:00
Zoe Stafford
deb90a6de2 [ fix ] generate lower level IRs if the option to dump that use phase is selected 2021-06-28 16:55:19 +01:00
Fabián Heredia Montiel
d5167a0108
[ fix #1581 ] public export Range functions and implementations (#1602)
Since `[a..b]` uses `takeUntil`/`takeBefore` indirectly those too had to
be changed to `public export` clashing with `Data.Stream` definitions.

A small readability refactor was made with the `compare` function from
`EqOrd`.
2021-06-28 16:52:23 +01:00
Tim Engler
05f28724ed
[ fix #1579 ] Nat hack for comparison operators (#1580)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-06-28 16:48:08 +01:00
Stepan Koltsov
8d7d13dd41
Insert @generated markers into generated launcher scripts (#1586)
Took me some time to figure out that `build/exec/idris2` is generated.
2021-06-28 16:44:33 +01:00
technic93
b5c2f28dae
Add comment about import from the contrib library (#1625) 2021-06-28 16:23:01 +01:00
Nick Drozd
63a6b16517 Cut unneeded type specifications 2021-06-28 16:22:27 +01:00
Nick Drozd
f49aa3c001 Simplify a few more lambdas 2021-06-28 15:57:21 +01:00
technic93
0aa968fe56
Add Split and SplitRec views for Vect (#1624)
Co-authored-by: Denis Buzdalov <public@buzden.ru>
2021-06-28 15:54:43 +01:00
Kamiλ Shakirov
8e30b296c0
[ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
Zoe Stafford
af871967ef [ error message ] include space in missing methods error 2021-06-28 13:38:26 +01:00
Stiopa Koltsov
60d597fccd Use pragma once instead of include guard
Pragma once is supported by all compilers for the last ten years.
Better use it instead of include guards (which use different styles
in different files).
2021-06-28 12:05:22 +01:00
Sören Tempel
3f681d2f5e Make sure _simple_handler is not exported
Support for simple signal handling was added in
a0a417240e. This commit also adds the
`_simple_handler` function. It seems to me that this function is
intended as a helper function which should only be visible in
`idris_signal.c`, it is not used outside this file. For this purpose it
is probably also marked as inline. However, the inline keyword does not
require the compiler to actually inline the function. As such, the
`_simple_handler` symbol may still be exported if the compiler doesn't
inline the function.

On my system this seems to be the case and causes the following error
during compilation of idris2:

	Exception: (while loading libidris2_support.so) Error relocating Idris2-0.4.0/build/exec/idris2_app/libidris2_support.so: _simple_handler: symbol not found

By marking the `_simple_handler` function as `static inline` it is
ensured that the symbol is not exported, thereby preventing the
relocation error.
2021-06-28 11:55:37 +01:00
claymager
594cb0039c
Nix fixes (#1623) 2021-06-28 11:47:47 +01:00
Stiopa Koltsov
a6555549ee Route System.prim__system through C function
To be able to eventually refactor/extend `system` function: to be
able to specify a directory, environment variables, specify arguments
as array etc. Ideally it should be something like Rust
[`std::process::Command`](https://doc.rust-lang.org/std/process/struct.Command.html).
2021-06-28 11:28:14 +01:00
Edwin Brady
78ff28faaa
Merge pull request #1622 from edwinb/missing-methods
Missing interface methods now cause an error
2021-06-27 20:49:59 +01:00
Edwin Brady
d6370380e6 Missing interface methods now cause an error
This was always the intended behaviour, but until now not implemented!
This caught a couple of issues in contrib and a test.
2021-06-27 20:03:19 +01:00
Edwin Brady
d88929ddd7
Merge pull request #1621 from edwinb/incremental-chez
Support for incremental compilation with Chez
2021-06-27 19:29:56 +01:00
Edwin Brady
452b0fc3f9 Fiddle with linter
We want duplicate headings in the CHANGELOG
2021-06-27 17:30:37 +01:00
Edwin Brady
74f0c3bf33 Add some documentation on incremental builds 2021-06-27 17:03:16 +01:00
Edwin Brady
84c2a497bc Add incremental compilation note to INSTALL.md 2021-06-27 16:35:43 +01:00
Edwin Brady
5a84623629 Update CHANGELOG 2021-06-27 16:33:04 +01:00
Edwin Brady
627bce068e Better errors/warnings for --inc
If the code generator doesn't support incremental builds, report an
error.
2021-06-27 16:28:17 +01:00
Edwin Brady
fc0e0f19d3 Use IDRIS2_CG for incremental library builds
This way there's no problem if chez isn't installed
2021-06-27 16:09:02 +01:00
Edwin Brady
6c319dbcaf Update API test for new Codegen fields 2021-06-27 16:00:03 +01:00
Edwin Brady
94088bea80 Support for incremental compilation with Chez
This adds a new flag '--inc <backend>' which, if set, compiles all
modules incrementally, and for executables, links the incrementally
compiled modules rather than building the whole program.

Also, adds an environment variable IDRIS2_INC_CGS for providing a comma
separated list of backends to use for incremental builds.

Also, adds '--whole-program', which overrides incremental builds for an
executable.

Incremental builds are much faster if there's nothing to recompile, but
for the Chez backend, generate code which runs at about half the speed.

Currently only works for Chez - other backends ignore the flag.

Also, incremental building of an executable will only work if *all*
required modules have been built incrementally for the backend in use.
2021-06-27 15:40:23 +01:00
Jan de Muijnck-Hughes
f77670814e
[ fix ] test Test.Golden with non-idris2 projects. (#1613) 2021-06-25 14:04:46 +01:00
Jan de Muijnck-Hughes
939bc8d8ff
Merge pull request #1610 from gallais/fix-golden
[ fix ] Various Test.Golden fixes
2021-06-24 20:27:20 +01:00
Guillaume ALLAIS
516b1b18f5 [ fix ] padding shouldn't be affected by ANSI escape codes 2021-06-24 16:38:27 +01:00
Guillaume ALLAIS
c217911573 [ fix ] Only pass --cg to test exec if requested
Do not pass a codegen choice when the test pool specifies it does
not require a codegen to be specified.
2021-06-24 16:36:03 +01:00
Edwin Brady
ea1ad1688f
Merge pull request #1599 from edwinb/prepare-040
Changes for next release, 0.4.0
2021-06-23 19:37:12 +01:00
Edwin Brady
00107730ae More version number updates 2021-06-23 18:46:38 +01:00
Edwin Brady
980b6174ec Added --mkdoc to CHANGELOG too 2021-06-23 18:31:31 +01:00
Edwin Brady
80aeecaac0 Add note on --mkdocs 2021-06-23 18:29:49 +01:00
Edwin Brady
6511412518 Change heading in CHANGELOG 2021-06-23 18:25:35 +01:00
Edwin Brady
a93def90a9 Merge github.com:idris-lang/Idris2 into prepare-040 2021-06-23 18:16:36 +01:00
Edwin Brady
991a4e8196 Update bootstrap scheme 2021-06-23 18:16:13 +01:00