tjh.dev
Clone of https://github.com/NixOS/nixpkgs.git (to stress-test knotserver)
1{
2 lib,
3 stdenv,
4 fetchurl,
5 fetchzip,
6 callPackage,
7 newScope,
8 recurseIntoAttrs,
9 ocamlPackages_4_14,
10 fetchpatch,
11 makeWrapper,
12}@args:
13let
14 lib = import ../build-support/rocq/extra-lib.nix { inherit (args) lib; };
15in
16let
17 mkRocqPackages' =
18 self: rocq-core:
19 let
20 callPackage = self.callPackage;
21 in
22 {
23 inherit rocq-core lib;
24 rocqPackages = self // {
25 __attrsFailEvaluation = true;
26 recurseForDerivations = false;
27 };
28
29 metaFetch = import ../build-support/coq/meta-fetch/default.nix {
30 inherit
31 lib
32 stdenv
33 fetchzip
34 fetchurl
35 ;
36 };
37 mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { });
38
39 bignums = callPackage ../development/rocq-modules/bignums { };
40 hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
41 parseque = callPackage ../development/rocq-modules/parseque { };
42 rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
43 stdlib = callPackage ../development/rocq-modules/stdlib { };
44
45 filterPackages = doesFilter: if doesFilter then filterRocqPackages self else self;
46 };
47
48 filterRocqPackages =
49 set:
50 lib.listToAttrs (
51 lib.concatMap (
52 name:
53 let
54 v = set.${name} or null;
55 in
56 lib.optional (!v.meta.rocqFilter or false) (
57 lib.nameValuePair name (
58 if lib.isAttrs v && v.recurseForDerivations or false then filterRocqPackages v else v
59 )
60 )
61 ) (lib.attrNames set)
62 );
63 mkRocq =
64 version:
65 callPackage ../applications/science/logic/rocq-core {
66 inherit
67 version
68 ocamlPackages_4_14
69 ;
70 };
71in
72rec {
73
74 /*
75 The function `mkRocqPackages` takes as input a derivation for Rocq and produces
76 a set of libraries built with that specific Rocq. More libraries are known to
77 this function than what is compatible with that version of Rocq. Therefore,
78 libraries that are not known to be compatible are removed (filtered out) from
79 the resulting set. For meta-programming purposes (inspecting the derivations
80 rather than building the libraries) this filtering can be disabled by setting
81 a `dontFilter` attribute into the Rocq derivation.
82 */
83 mkRocqPackages =
84 rocq-core:
85 let
86 self = lib.makeScope newScope (lib.flip mkRocqPackages' rocq-core);
87 in
88 self.filterPackages (!rocq-core.dontFilter or false);
89
90 rocq-core_9_0 = mkRocq "9.0";
91 rocq-core_9_1 = mkRocq "9.1";
92
93 rocqPackages_9_0 = mkRocqPackages rocq-core_9_0;
94 rocqPackages_9_1 = mkRocqPackages rocq-core_9_1;
95
96 rocqPackages = recurseIntoAttrs rocqPackages_9_0;
97 rocq-core = rocqPackages.rocq-core;
98}