blob: 4acfae48e40302d89c7035684cde33d3a39cf563 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
{ pkgs ? import <nixpkgs> {}
, branch
, wd
, project ? "xyz"
, bn ? "release"
}:
with pkgs;
# Coq from this directory
let coq = callPackage ./coq.nix { inherit branch wd; }; in
# Third-party libraries, built with this Coq
let coqPackages = mkCoqPackages coq; in
let mathcomp = coqPackages.mathcomp.overrideAttrs (o: {
name = "coq-git-mathcomp-git";
src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz;
}); in
let bignums = coqPackages.bignums.overrideAttrs (o:
if bn == "release" then {} else
if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else
{ src = fetchTarball bn; }
); in
let coqprime = coqPackages.coqprime.override { inherit coq bignums; }; in
let math-classes =
(coqPackages.math-classes.override { inherit coq bignums; })
.overrideAttrs (o: {
src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
}); in
let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in
# Environments for building CI libraries with this Coq
let projects = {
bedrock2 = callPackage ./bedrock2.nix {};
bignums = callPackage ./bignums.nix {};
CoLoR = callPackage ./CoLoR.nix {};
CompCert = callPackage ./CompCert.nix {};
coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
Corn = callPackage ./Corn.nix {};
cross_crypto = callPackage ./cross_crypto.nix {};
Elpi = callPackage ./Elpi.nix {};
fiat_crypto = callPackage ./fiat_crypto.nix {};
fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
flocq = callPackage ./flocq.nix {};
GeoCoq = callPackage ./GeoCoq.nix {};
HoTT = callPackage ./HoTT.nix {};
math_classes = callPackage ./math_classes.nix {};
mathcomp = {};
mtac2 = callPackage ./mtac2.nix {};
oddorder = callPackage ./oddorder.nix {};
VST = callPackage ./VST.nix {};
}; in
if !builtins.hasAttr project projects
then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}."
else
let prj = projects."${project}"; in
stdenv.mkDerivation {
name = "shell-for-${project}-in-${branch}";
buildInputs = [ coq ] ++ (prj.buildInputs or []);
configure = prj.configure or "true";
make = prj.make or "make";
clean = prj.clean or "make clean";
}
|
