Commit Graph

2403 Commits

Author SHA1 Message Date
Edwin Brady
a5abb5b2a3
Merge pull request #1702 from stepancheg/rm-prim-get-errno
Remove prim__getErrno from Prelude.IO
2021-07-14 14:56:03 +01:00
Edwin Brady
1dbc9a7143 Fix 'with' under implicit parameters
The 'with' type and application need to treat the parameters with the
same plicity, but the application has just always treated them as
explicit since it never looked. It's easiest just to make them all
explicit, since this isn't a user visible type. Fixes #1695.
2021-07-14 14:51:52 +01:00
Mathew Polzin
830e5dc12d Fix bug with what value was propagated from rhs of alt parse failure and add test case for '@' as value constructor. 2021-07-14 00:25:02 -07:00
Stiopa Koltsov
291823c752 Remove prim__getErrno from Prelude.IO
The function is not used, and it is defined incorrectly.
2021-07-14 03:15:49 +01:00
André Videla
bd4245ccaf
Merge pull request #1699 from stepancheg/refc-generated
Use the same generated string in RefC backend as in other backends
2021-07-13 23:46:26 +00:00
Stiopa Koltsov
f81c37ea3a Pass Buffer as char* when using C functions in RefC
To be able to use `C` functions for both Scheme and RefC: it was
not possible for `Buffer` before this PR.

As an example, `writeBufferData` and `readBufferData` functions are
removed: generic C backend implementations are used instead.
2021-07-13 23:04:36 +01:00
Stiopa Koltsov
13a9676805 Use the same generated string in RefC backend as in other backends 2021-07-13 23:00:13 +01:00
Stiopa Koltsov
9f61e542b4 Move rm -rf to the beginning of the test
While the discussion about how to refactor test framework is not
finished (#1654), make this change: move `rm -rf build` in the
beginning of the test. For these reasons:

* it is useful to inspect the contents of the `build` directory
  especially after the test failure
* if build crashes mid-test (e.g. process killed), next run should
  not be affected by the `build` directory from the previous run
2021-07-13 22:54:53 +01:00
Mathew Polzin
385a61a364 fix linting errors and use a public import of List1 instead of forcing other files to import List1 just to use Libraries.Text.Parser 2021-07-13 10:53:58 -07:00
Thomas E. Hansen
bfbe974254
[ doc ] Add topics (#1498) for pragmas. Implements --help pragma.
This adds the ability to do `idris2 --help pragma` and get a list of the
various pragmas and their options, similar to `idris2 --help logging`.
2021-07-13 17:52:40 +02:00
Nick Drozd
9cca3a7d35
Use Not instead of -> Void (#1667) 2021-07-13 15:32:01 +01:00
Stiopa Koltsov
d910677d74 IDRIS2_VERIFY macro
```
IDRIS2_VERIFY(cond, message_format, ...)
```

When condition is false, crash.

Used in native functions where correct error handling is hard or
not impossible.

For example, `malloc` rarely fails, but if it fails, better crash
with clear error message than spend time debugging null pointer
dereference.
2021-07-13 13:57:24 +01:00
Johann Rudloff
d5abff4e46
[ fix #1260 ] Use blodwen-stringbytelen instead of C's strlen (#1261) 2021-07-13 11:52:15 +01:00
Niklas Larsson
eb0c59c908
Enable incremental compilation on Windows. (#1694) 2021-07-13 11:29:34 +01:00
stefan-hoeck
f6b4f188e1 [ new ] support compile time evaluation of new integer primops 2021-07-13 11:28:02 +01:00
Rujia Liu
9dfad52173
[fix] refc backend broken with msys2 (#1668) 2021-07-13 11:27:36 +01:00
stefan-hoeck
fdb2d4f2a4 [ doc ] updated javascript documentation 2021-07-13 11:15:20 +01:00
CodingCellist
80e7e179ad
[ fix #1652 ] Save casefnty to TTC (#1686) 2021-07-13 11:04:07 +01:00
Stiopa Koltsov
1617d95961 System.Errno.strerror
* add `strerror` function
* move `getErrno` to `System.Errno`
* use `strerror` in `Show FileError`
* on node there's no access to `strerror`, so `strerror` just converts the number to string
2021-07-13 10:34:04 +01:00
Stiopa Koltsov
d676ea6ab4 Expose malloc and free from System.FFI
* Move `malloc`/`free` from `Network.FFI` to `System.FFI`
* Might be useful by other code
2021-07-13 10:24:26 +01:00
Mathew Polzin
fd9045bc4a update tests 2021-07-12 23:25:49 -07:00
Mathew Polzin
8e1f2cf4ce fix lack of error for @ used as identifier and display multiple alternative errors. 2021-07-12 23:11:43 -07:00
Stiopa Koltsov
ed40b212b2 Make System.Signal async-signal-safe
It is not safe to call `malloc` or `pthread_mutex_lock` from signal
handler.
2021-07-12 20:43:26 +01:00
Stiopa Koltsov
1fac812435 In RefC, allocate the exact size of value subtype
* remove `Value.payload` field
* `IDRIS2_NEW_VALUE` macro now allocates the size needed for the struct
2021-07-12 16:27:09 +01:00
Nick Drozd
a07d42ac91
Delete old Order file, update changelog and contributors (#1685) 2021-07-12 10:53:45 +01:00
Edwin Brady
b05ec6eff5
Merge pull request #1676 from edwinb/inc-fix
Need --script for incrementally compiled apps
2021-07-11 18:22:20 +01:00
Edwin Brady
9bd32c4a3d Fix chez033 on windows
This prints lots of warnings since incremental compilation is not
available, so turn that off when running on windows for now.
2021-07-11 17:04:07 +01:00
Edwin Brady
c95ebd554d Disable incremental compilation on Windows
It currently doesn't work anyway, so fall back to whole program
compilation which at least means the test doesn't get in the way.
2021-07-11 16:20:47 +01:00
Stiopa Koltsov
c292437a28 Remove Value_Buffer.len field
It is not used.

Also change `buffer` field type to avoid confusion.
2021-07-11 12:00:01 +01:00
Stiopa Koltsov
b4918d51ff Add parameter names to Buffer builtins parameter names
Also rename `loc` -> `offset`.
2021-07-11 10:43:12 +01:00
Edwin Brady
c839c98c7d Add test for incremental compilation
Ideally we'd have a complete incremental build in CI, but that could be
a bit fiddly to set up at the moment (updating bootstrap code might make
it easier). This tests that the basic facilities work, though - there's
a lot can go wrong even in a small test like this, trust me, I have made
those mistakes :).
2021-07-11 00:05:00 +01:00
Edwin Brady
886962aa43 Need --script for incrementally compiled apps
Otherwise it doesn't load the compiled modules and can't find the
compiled definitions!
2021-07-10 23:55:45 +01:00
Edwin Brady
3e92863e1c
Merge pull request #1674 from edwinb/parameters
A couple of parameters block fixes
2021-07-10 21:18:07 +01:00
Edwin Brady
86c75bae2c Add test for interfaces in parameter blocks
I thought these didn't work. Apparently they do. I should find out when
that happened because it might have been a side effect of something
else!
2021-07-10 20:15:50 +01:00
Edwin Brady
b34eade6fb Placate linter again 2021-07-10 19:18:49 +01:00
Edwin Brady
2bd89cee36 Placate linter
It should not care about spacing in tests. Not an issue here in
practice, but who knows if we might want to test a spacing related thing
some day.
2021-07-10 19:17:08 +01:00
Edwin Brady
ab5623efa9 Update CHANGELOG 2021-07-10 19:16:29 +01:00
Edwin Brady
4ca8caeb13 Fix case split in parameter blocks
We need to make sure variables are bound as PVar, in the end, otherwise
the case split machinery doesn't know how to handle them.
2021-07-10 19:13:27 +01:00
Edwin Brady
26cdfc7830 Make records work in parameter blocks
This involves making 'unelab' aware of nested names so that it can
remove the parameters from names in the current block. It's a bit of a
hacky solution, but it is also the easiest one.
Ideally we'd build the getter types directly, rather than using unelab,
but that's one to save for another time.
Fixes #1482
2021-07-10 18:12:44 +01:00
Edwin Brady
8b45ccd264 Use chez --program rather than --script
We're running our executables as top level programs, so this gives more
scope for optimisations, doesn't use the Chez REPL, etc.
2021-07-10 16:40:19 +01:00
Stefan Höck
599d0635e9
[ refactor ] JS backend overhaul (#1609) 2021-07-10 11:15:21 +01:00
Alex Humphreys
cd81cff241 Update README status badges
Github Action status are based on workflows, not jobs. When #1645 was
merged, it changed multiple workflows into 1 workflow with multiple
jobs. This meant several badges on the README were now linking to
workflows which don't exist. This change makes a badge for the new
single workflow which does exist.

While it would probably be better to have statuses per job, I think the
only way to achieve that would be with an extra action like
https://github.com/marketplace/actions/bring-your-own-badge. So I'll
just stick with this minor fix for now.
2021-07-10 11:14:01 +01:00
Nick Drozd
61b9a3e4e5
Define and implement Relation interfaces (#1472)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-07-09 09:06:27 +01:00
Zoe Stafford
0ecbd517e8
[ improvement ] VMCode (#1662) 2021-07-07 17:06:59 +01:00
Stiopa Koltsov
8fd58b3bdd More reliable exception handling in Control.App
Convert `App.Control.Exception` interface to an alias to `HasErr`.

Probably `Exception` interface need to be deprecated or removed.

Note similar problem exists with `PrimIO` calling `PrimIO, Exception`,
also need to be fixed.

Fix this scenario:

```
throwBoth : Has [Exception String, Exception Int] es => App es ()

throwOne : Has [Exception Int] es => App es Int
throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
```

With this commit it works, before this commit it failed with:

```
Error: While processing right hand side of throwOne. Can't find an implementation for Exception Int (String :: es).

TestException.idr:8:48--8:57
   |
 8 | throwOne {es} = handle {err = String} {e = es} throwBoth (\r => pure 1) (\e => pure 3)
   |                                                ^^^^^^^^^
```
2021-07-06 10:43:54 +01:00
Stiopa Koltsov
9c63e90fd2 Write compiler version into generated files 2021-07-06 09:35:48 +01:00
Stiopa Koltsov
fb1d118b2d Test System.system 2021-07-06 09:34:47 +01:00
Stiopa Koltsov
afaf416673 Write files into bootstrap-build directory during bootstrap
... instead of `bootstrap` which contains source files. Make it easier to understand
how build works, and in particular, which files are sources and
which files are generated.
2021-07-04 03:17:13 +01:00
Edwin Brady
4fdec0682e
Merge pull request #1655 from edwinb/proofsearch-fix
Don't inline holes that are user defined names
2021-07-03 12:23:19 +01:00
Edwin Brady
6a60680af6 Don't inline holes that are user defined names
We inline some holes when solving them if they pose no risk to breaking
sharing, since this can speed up a few things. But if the hole was
originally a user name, we might want to refer to it, and inlining it
menas we can't since it won't be saved to disk.
2021-07-02 15:59:56 +01:00