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.