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
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.
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)
| ^^^^^^^^^
```
... 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.
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.
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.
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).
The `Decl` annotation should go directly on the name-type part. This
automatically fixes the `Decl` annotation being skipped, when no
docstring is found.
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 { ... }
```
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.
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`.
