Use the new `--build-library` mode introduced in Agda 2.8.0 to build
libraries instead of relying on ad-hoc `Everything` files. This
simplifies most derivations (except cubical-mini which imports generated
`Everything` files from various modules).
After final improvements to the official formatter implementation,
this commit now performs the first treewide reformat of Nix files using it.
This is part of the implementation of RFC 166.
Only "inactive" files are reformatted, meaning only files that
aren't being touched by any PR with activity in the past 2 months.
This is to avoid conflicts for PRs that might soon be merged.
Later we can do a full treewide reformat to get the rest,
which should not cause as many conflicts.
A CI check has already been running for some time to ensure that new and
already-formatted files are formatted, so the files being reformatted here
should also stay formatted.
This commit was automatically created and can be verified using
nix-build a08b3a4d19.tar.gz \
--argstr baseRev 78e9caf153
result/bin/apply-formatting $NIXPKGS_PATH
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 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.
