Commit Graph

2198 Commits

Author SHA1 Message Date
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
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
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
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
CodingCellist
fac0e32f48
[ fix ] Chez channels (#1596) 2021-07-02 13:13:50 +01:00
G. Allais
b0e297658c
[ cli ] make package file optional (#1651) 2021-07-01 14:16:29 +01:00
Alissa Tung
2865a70a6e
[ base ] add List functions (#1550)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-07-01 08:00:12 +01:00
Johann Rudloff
08fb38b791 Mark bootstrap code as generated 2021-06-30 22:11:54 +01:00
Johann Rudloff
5e70a77310 [ docs ] Ignore empty record field docstrings 2021-06-30 22:01:26 +01:00
Johann Rudloff
7c1ab56ca0 [ docs ] Add record field docstrings to the RF-name as well
A record field can add two names to the context, a UN-name and an
RF-name.  The docstring is now saved for both names, so that it can
always be found when one of the names can be resolved.

Previously the docstring was only saved for the UN-name which led to the
docs missing when looking up the (.fieldName) version, e.g. when listing
docs for the record type.
2021-06-30 22:01:26 +01:00
Johann Rudloff
af9f72466f [ docs ] Fix record fields wrapped in parentheses in HTML doc
The (implicitly added) "."-prefix when calling `isOpName` with an RF-name
leads to `isOpName` always returning true (which is correct in most
cases, where the RF is displayed as such). In case of the docs however,
we only show the name root and thus should check the "real" name of the
field (without the added dot in the beginning).
2021-06-30 22:01:26 +01:00
Johann Rudloff
f2f83bd531 [ docs ] Fix HTML formatting for record projections
The `Decl` annotation should go directly on the name-type part. This
automatically fixes the `Decl` annotation being skipped, when no
docstring is found.
2021-06-30 22:01:26 +01:00
zseri
6fbba94c21 Nix: make nixpkgs options overridable
This allows for cross-flake testing of content-addressible nix derivations without
affecting other users of the flake (which would be the cases if CA-drvs would be
hard-coded upstream) and without losing the ability to quickly update to the latest
idris2 version (which would happen if a fork of the repo would be used).

See also: https://discourse.nixos.org/t/content-addressed-nix-call-for-testers/12881

The flake can still be used as usual, but it will gain an output `overrideOptions`, which can be used like e.g.
```nix
let
  idrisx = idris.overrideOptions {
    config.contentAddressedByDefault = true;
  };
in { ... }
```
2021-06-30 15:33:37 +01:00
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