tjh.dev
1{ stdenv, fetchFromGitHub, coq, ncurses, which
2, graphviz, withDoc ? false
3}:
4
5let param =
6
7 if stdenv.lib.versionAtLeast coq.coq-version "8.6" then
8 {
9 version = "1.7.0";
10 sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
11 }
12 else if stdenv.lib.versionAtLeast coq.coq-version "8.5" then
13 {
14 version = "1.6.1";
15 sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
16 }
17 else throw "No version of math-comp is available for Coq ${coq.coq-version}";
18
19in
20
21stdenv.mkDerivation rec {
22 name = "coq${coq.coq-version}-mathcomp-${version}";
23
24 # used in ssreflect
25 inherit (param) version;
26
27 src = fetchFromGitHub {
28 owner = "math-comp";
29 repo = "math-comp";
30 rev = "mathcomp-${param.version}";
31 inherit (param) sha256;
32 };
33
34 nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
35 buildInputs = [ coq ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
36
37 enableParallelBuilding = true;
38
39 buildFlags = stdenv.lib.optionalString withDoc "doc";
40
41 COQBIN = "${coq}/bin/";
42
43 preBuild = ''
44 patchShebangs etc/utils/ssrcoqdep || true
45 cd mathcomp
46 '';
47
48 installPhase = ''
49 make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
50 '' + stdenv.lib.optionalString withDoc ''
51 make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
52 '';
53
54 meta = with stdenv.lib; {
55 homepage = http://ssr.msr-inria.inria.fr/;
56 license = licenses.cecill-b;
57 maintainers = [ maintainers.vbgl maintainers.jwiegley ];
58 platforms = coq.meta.platforms;
59 };
60
61 passthru = {
62 compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5";
63 };
64
65}