374e6bcc40
Format all Nix files using the officially approved formatter,
making the CI check introduced in the previous commit succeed:
nix-build ci -A fmt.check
This is the next step of the of the [implementation](https://github.com/NixOS/nixfmt/issues/153)
of the accepted [RFC 166](https://github.com/NixOS/rfcs/pull/166).
This commit will lead to merge conflicts for a number of PRs,
up to an estimated ~1100 (~33%) among the PRs with activity in the past 2
months, but that should be lower than what it would be without the previous
[partial treewide format](https://github.com/NixOS/nixpkgs/pull/322537).
Merge conflicts caused by this commit can now automatically be resolved while rebasing using the
[auto-rebase script](8616af08d9/maintainers/scripts/auto-rebase).
If you run into any problems regarding any of this, please reach out to the
[formatting team](https://nixos.org/community/teams/formatting/) by
pinging @NixOS/nix-formatting.
95 lines
2.5 KiB
Nix
95 lines
2.5 KiB
Nix
{
|
|
lib,
|
|
stdenv,
|
|
fetchurl,
|
|
fetchzip,
|
|
callPackage,
|
|
newScope,
|
|
recurseIntoAttrs,
|
|
ocamlPackages_4_14,
|
|
fetchpatch,
|
|
makeWrapper,
|
|
}@args:
|
|
let
|
|
lib = import ../build-support/rocq/extra-lib.nix { inherit (args) lib; };
|
|
in
|
|
let
|
|
mkRocqPackages' =
|
|
self: rocq-core:
|
|
let
|
|
callPackage = self.callPackage;
|
|
in
|
|
{
|
|
inherit rocq-core lib;
|
|
rocqPackages = self // {
|
|
__attrsFailEvaluation = true;
|
|
recurseForDerivations = false;
|
|
};
|
|
|
|
metaFetch = import ../build-support/coq/meta-fetch/default.nix {
|
|
inherit
|
|
lib
|
|
stdenv
|
|
fetchzip
|
|
fetchurl
|
|
;
|
|
};
|
|
mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { });
|
|
|
|
bignums = callPackage ../development/rocq-modules/bignums { };
|
|
rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
|
|
stdlib = callPackage ../development/rocq-modules/stdlib { };
|
|
|
|
filterPackages = doesFilter: if doesFilter then filterRocqPackages self else self;
|
|
};
|
|
|
|
filterRocqPackages =
|
|
set:
|
|
lib.listToAttrs (
|
|
lib.concatMap (
|
|
name:
|
|
let
|
|
v = set.${name} or null;
|
|
in
|
|
lib.optional (!v.meta.rocqFilter or false) (
|
|
lib.nameValuePair name (
|
|
if lib.isAttrs v && v.recurseForDerivations or false then filterRocqPackages v else v
|
|
)
|
|
)
|
|
) (lib.attrNames set)
|
|
);
|
|
mkRocq =
|
|
version:
|
|
callPackage ../applications/science/logic/rocq-core {
|
|
inherit
|
|
version
|
|
ocamlPackages_4_14
|
|
;
|
|
};
|
|
in
|
|
rec {
|
|
|
|
/*
|
|
The function `mkRocqPackages` takes as input a derivation for Rocq and produces
|
|
a set of libraries built with that specific Rocq. More libraries are known to
|
|
this function than what is compatible with that version of Rocq. Therefore,
|
|
libraries that are not known to be compatible are removed (filtered out) from
|
|
the resulting set. For meta-programming purposes (inspecting the derivations
|
|
rather than building the libraries) this filtering can be disabled by setting
|
|
a `dontFilter` attribute into the Rocq derivation.
|
|
*/
|
|
mkRocqPackages =
|
|
rocq-core:
|
|
let
|
|
self = lib.makeScope newScope (lib.flip mkRocqPackages' rocq-core);
|
|
in
|
|
self.filterPackages (!rocq-core.dontFilter or false);
|
|
|
|
rocq-core_9_0 = mkRocq "9.0";
|
|
|
|
rocqPackages_9_0 = mkRocqPackages rocq-core_9_0;
|
|
|
|
rocqPackages = recurseIntoAttrs rocqPackages_9_0;
|
|
rocq-core = rocqPackages.rocq-core;
|
|
}
|