| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | build-support/agda: Keep passthru in mkDerivation | Rasheeq Azad | 2025-11-27 | 1 | -3/+8 |
| * | Conditionally create symlink to agda-mode if present | Carlos Tomé Cortiñas | 2025-10-28 | 1 | -0/+3 |
| * | Update pkgs/build-support/agda/default.nix•••Co-authored-by: Philip Taron <philip.taron@gmail.com> | Carlos Tomé Cortiñas | 2025-10-28 | 1 | -1/+1 |
| * | Remove agda-mode from executables | Carlos Tomé Cortiñas | 2025-10-28 | 1 | -1/+0 |
| * | Replace hardcoded agda binary by name from package | Carlos Tomé Cortiñas | 2025-10-28 | 1 | -3/+3 |
| * | agda.withPackages: add libraryFile to passthru | wrvsrx | 2025-10-02 | 1 | -3/+6 |
| * | agda: fixes for 2.8.0 (#424180) | Philip Taron | 2025-07-17 | 2 | -11/+5 |
| |\ |
|
| | * | agdaPackages: switch to `--build-library`•••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).
| Naïm Camille Favier | 2025-07-16 | 2 | -11/+5 |
| * | | haskellPackages.Agda: set `mainProgram` | Naïm Camille Favier | 2025-07-16 | 1 | -2/+2 |
| * | | agda: use `getBin Agda` instead of `Agda.bin`•••Makes the wrapper work if `enableSeparateBinOutput` is off.
| Naïm Camille Favier | 2025-07-16 | 1 | -2/+2 |
| |/ |
|
| * | agda.withPackages: allow installing Agda without GHC using `ghc = null;` | Tsung-Ju Chiang | 2025-05-28 | 1 | -1/+1 |
| * | treewide: format all inactive Nix files•••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 https://github.com/infinisil/treewide-nixpkgs-reformat-script/archive/a08b3a4d199c6124ac5b36a889d9099b4383463f.tar.gz \
--argstr baseRev b32a0943687d2a5094a6d92f25a4b6e16a76b5b7
result/bin/apply-formatting $NIXPKGS_PATH
| Silvan Mosberger | 2024-12-10 | 2 | -83/+124 |
| * | treewide: replace `stdenv.is` with `stdenv.hostPlatform.is`•••In preparation for the deprecation of `stdenv.isX`.
These shorthands are not conducive to cross-compilation because they
hide the platforms.
Darwin might get cross-compilation for which the continued usage of `stdenv.isDarwin` will get in the way
One example of why this is bad and especially affects compiler packages
https://www.github.com/NixOS/nixpkgs/pull/343059
There are too many files to go through manually but a treewide should
get users thinking when they see a `hostPlatform.isX` in a place where it
doesn't make sense.
```
fd --type f "\.nix" | xargs sd --fixed-strings "stdenv.is" "stdenv.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "stdenv'.is" "stdenv'.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "clangStdenv.is" "clangStdenv.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "gccStdenv.is" "gccStdenv.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "stdenvNoCC.is" "stdenvNoCC.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "inherit (stdenv) is" "inherit (stdenv.hostPlatform) is"
fd --type f "\.nix" | xargs sd --fixed-strings "buildStdenv.is" "buildStdenv.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "effectiveStdenv.is" "effectiveStdenv.hostPlatform.is"
fd --type f "\.nix" | xargs sd --fixed-strings "originalStdenv.is" "originalStdenv.hostPlatform.is"
```
| Artturin | 2024-09-25 | 1 | -1/+1 |
| * | build-support/agda: expose mkLibraryFile | Naïm Favier | 2024-07-04 | 1 | -5/+8 |
| * | haskellPackages.Agda: Split outputs to reduce closure size•••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`.
| Philipp Joram | 2024-04-07 | 1 | -3/+4 |
| * | Merge master into staging-next | github-actions[bot] | 2024-03-31 | 2 | -7/+9 |
| |\ |
|
| | * | agda: Don't be too picky about `everythingFile`•••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.
| ibbem | 2024-03-18 | 2 | -4/+7 |
| | * | agda: Remove the --local-interfaces flag•••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.
| ibbem | 2024-03-18 | 2 | -7/+6 |
| * | | Avoid top-level `with ...;` in pkgs/build-support/agda/default.nix | Philip Taron | 2024-03-19 | 1 | -10/+24 |
| |/ |
|
| * | agdaPackages.*: support literate Typst files | Naïm Favier | 2023-10-24 | 2 | -1/+2 |
| * | Merge remote-tracking branch 'origin/master' into haskell-updates | sternenseemann | 2023-02-18 | 1 | -1/+5 |
| |\ |
|
| | * | agda: fix passthru•••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`.
| Naïm Favier | 2023-02-12 | 1 | -1/+5 |
| * | | agda: 2.6.2.2 -> 2.6.3 | Ingo Blechschmidt | 2023-02-14 | 1 | -0/+7 |
| |/ |
|
| * | agda: pass through meta | Naïm Favier | 2023-01-12 | 1 | -1/+2 |
| * | Merge pull request #98214 from turion/dev_test_all_agda_packages•••Fix #98209. Test all agda packages | Manuel Bärenz | 2021-10-19 | 2 | -0/+10 |
| |\ |
|
| | * | agdaPackages: Build reverse dependencies on test | Manuel Bärenz | 2021-08-03 | 2 | -0/+10 |
| * | | build-support/agda: Make includePaths configurable | Manuel Bärenz | 2021-08-30 | 1 | -1/+3 |
| * | | treewide: runCommandNoCC -> runCommand•••This has been synonymous for ~5y.
| Robert Hensing | 2021-08-15 | 1 | -2/+2 |
| |/ |
|
| * | agdaPackages: Don't build broken packages on hydra | Manuel Bärenz | 2021-07-22 | 1 | -0/+2 |
| * | mkShell: introduce packages argument (#122180)•••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. | Jonas Chevalier | 2021-05-13 | 1 | -1/+1 |
| * | agda nixos test: add to passthru for agda + stdlib | Alex Rice | 2021-03-30 | 1 | -2/+5 |
| * | Merge pull request #110512 from neosimsim/agda-dont-install-Everything•••Agda don't install Everything module | Anderson Torres | 2021-02-03 | 2 | -1/+11 |
| |\ |
|
| | * | agdaPackages.mkDerivation: don't install Everything module•••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.
| Alexander Ben Nasrallah | 2021-01-24 | 2 | -1/+11 |
| * | | agda.withPackages: use GHC with ieee754 as default•••As mentioned in the package description of ieee on Hackage,
ieee is deprecated in favor of ieee754.
| Alexander Ben Nasrallah | 2021-01-22 | 1 | -1/+1 |
| |/ |
|
| * | agda: install literate files | Alex Rice | 2020-06-01 | 1 | -1/+12 |
| * | agda: rework builder | Alex Rice | 2020-05-14 | 1 | -76/+57 |
| * | treewide: fix *Flags | Robin Gloster | 2019-12-30 | 1 | -2/+2 |
| * | Remove myself (fuuzetsu) from maintainer lists•••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.
| Mateusz Kowalczyk | 2019-12-05 | 1 | -2/+0 |
| * | agda: use exec in agdaWrapper | Dmitry Kalinkin | 2018-12-07 | 1 | -1/+1 |
| * | agda: use writeShellScriptbin instead of writeScriptBin•••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.
| Moritz Kiefer | 2018-11-08 | 1 | -2/+2 |
| * | agda: Remove unused/uneeded abstractions, including `postprocess` | John Ericson | 2015-05-31 | 1 | -18/+11 |
| * | agda: Just `with` all of the string helper functions | John Ericson | 2015-05-31 | 1 | -3/+3 |
| * | agda: `postprocess` and `defaults` need not be in the scope of args | John Ericson | 2015-05-30 | 1 | -68/+67 |
| * | agda: Provide a `.env` like Haskell instead of `.extras` | John Ericson | 2015-05-30 | 1 | -19/+13 |
| * | agda: Wrapper is no longer built by default•••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`.
| John Ericson | 2015-05-20 | 1 | -16/+23 |
| * | agda: Agda dependencies are treated seperately••• - 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
| John Ericson | 2015-05-20 | 1 | -6/+14 |
| * | agda: Remove `extraBuildFlags`•••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.
| John Ericson | 2015-05-18 | 1 | -6/+5 |
| * | agda: Remove buildTools, it is unused | John Ericson | 2015-05-18 | 1 | -3/+1 |
| * | agda: Replace `eval` with `runHook`•••This is what haskell-ng does, so I figure it is the right thing to
do.
| John Ericson | 2015-05-17 | 1 | -6/+6 |
| * | agda: Remove unnecessary env-var export•••Derivation attributes are automatically exported as environment
variables already.
| John Ericson | 2015-05-17 | 1 | -1/+0 |
