blob: 61901d545d7a2a75a9cf323fa0e3a1dc7ae73f4e (
plain) (
blame)
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
|
# TODO:
# - ssrcoqide does not build successfully (missing coqide libraries in the coq installation).
# - ssrcoq needs to be invoked with the explicit path to the ssreflect theory
# e.g.. ssrcoq -I /nix/store/rp09dlb2y2hpddb0xa7fyrgjlzb284ar-ssreflect-1.2/lib/coq/user-contrib/theories/
{stdenv, fetchurl, ocaml, camlp5, coq}:
let
pname = "ssreflect";
version = "1.2";
name = "${pname}-${version}";
webpage = http://www.msr-inria.inria.fr/Projects/math-components;
in
stdenv.mkDerivation {
inherit name;
src = fetchurl {
url = "${webpage}/${name}.tgz";
sha256 = "0800b085e6a0caec5093c6c02aacdd8dfd9cc282177e8586f14f9a9e15f64d0b";
};
buildInputs = [ ocaml camlp5 coq ];
preBuild = ''
coq_makefile -f Make -o Makefile
substituteInPlace Makefile \
--replace 'install -D $$i $(COQLIB)' 'install -D $$i '$out'/lib/coq'
'';
# this fails
/*
postBuild = ''
cd src
coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
'';
*/
postInstall = ''
ensureDir $out/bin
#cp -a bin/ssrcoq bin/ssrcoqide $out/bin
cp -a bin/ssrcoq $out/bin
'';
meta = {
description = "Small Scale Reflection extension for Coq";
longDescription = ''
Small Scale Reflection (ssreflect) is an extension of the Coq Theorem
Prover which enable a formal proof methodology based on the pervasive
use of computation with symbolic representation
'';
homepage = webpage;
license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE";
};
}
|