After enabling a separate binary output for the `Agda` Haskell package,
the new `bin` output measures ~100MiB, compared to the ~4.5GiB before.
Using it in `agdaWithPackages` reduces the closure size of an Agda
installation from ~5GiB to ~3GiB. The remaining space is taken up
mostly by the GHC backend.
With this change, derivations depending on `haskellPackages.Agda`
directly need to pick the right (binary) output. This concerns in
particular `emacsPackages.agda2-mode`.
The `-path` test of `find` does string comparison, not path comparison.
Hence, the format of `everythingFile` needed to be very specific. Now,
it can be denormalized (e.g. it can contain `/./`) and an error is
emitted if the everything file or its interface file can't be removed.
Upstream now provides a library file for the builtin library and ensured
that the existing interface files will be used regardless of whether
--local-interfaces is in effect. Hence, Agda will not try to write to
the Nix store anymore except if the build flags are changed.
The current `//` override to `agda.passthru.tests` is non-recursive so
it destroys everything else under `passthru`, and furthermore does not
go through `mkDerivation` so that we end up with different values for
`agda.tests` and `agda.passthru.tests`.
Fix it by moving the `allPackages` test to the definition of
`withPackages`.
The distinction between the inputs doesn't really make sense in the
mkShell context. Technically speaking, we should be using the
nativeBuildInputs most of the time.
So in order to make this function more beginner-friendly, add "packages"
as an attribute, that maps to nativeBuildInputs.
This commit also updates all the uses in nixpkgs.
The Everthing module is not part of a library and should therefore
not be copied to the nix store.
This is particularly bad, if the Everything module is defined in
an agda library included directory, e.g. consider an agda-lib with
include: .
and Everything.agda in the project root (.), in which case the
Everything module would become part of the library.
If multiple such projects are in the dependency tree, the Everything
module becomes ambiguous and the build would fail.
I haven't been doing any maintenance for a long time now and not only
do I get notified, it also creates a fake impression that all these
packages had at least one maintainer when in practice they had none.
This adds the shell shebang to the wrapper script. Without this,
emacs and in particular agda2-mode (but probably other applications as
well) return a format error when trying to execute agda.
Instead it is provided to the user who can choose whether or not
to include it in the final derivati. Example of including would
be:
```nix
callPackage ... (self: { inherit (self.extras) extraThing; })
```
These extras are also available downstream without being built by
default. This is achieved with `passthru`.
- Only they are added to the optional build path (share/agda)
- Only they are are passed as an include dir (share/agda)
- Only they are propigatedBuildInputs
This is unused, future users can just use override `buildFlags`
and extend/replace as needed. `includeDirs` is provided for this
purpose.
We should add `dirOf self.everythingFile` rather than `.`, but
`dirOf` breaks on relative paths so that is not an option.
