blob: 813397ba01f93c08eb1aa519a4543de2f9b04b2c (
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
56
57
58
59
60
61
62
63
64
65
|
{ lib, stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, findlib, num, camlp5, camlp-streams }:
let
load_num =
lib.optionalString (num != null) ''
-I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \
-I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \
-I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs \
'';
start_script =
''
#!${runtimeShell}
cd $out/lib/hol_light
export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}${camlp5}/lib/ocaml/${ocaml.version}/site-lib/"
exec ${ocaml}/bin/ocaml \
-I \`${camlp5}/bin/camlp5 -where\` \
${load_num} \
-I ${findlib}/lib/ocaml/${ocaml.version}/site-lib/ \
-I ${camlp-streams}/lib/ocaml/${ocaml.version}/site-lib/camlp-streams camlp_streams.cma \
-init make.ml
'';
in
lib.throwIf (lib.versionAtLeast ocaml.version "5.0")
"hol_light is not available for OCaml ${ocaml.version}"
stdenv.mkDerivation {
pname = "hol_light";
version = "unstable-2023-11-03";
src = fetchFromGitHub {
owner = "jrh13";
repo = "hol-light";
rev = "dcd765c6032f52a0c0bf21fce5da4794a823e880";
hash = "sha256-k2RBNDo4tc3eobKB84Y2xr0UQJvef0hv6jyFCaDCQFM=";
};
patches = [
(fetchpatch {
url = "https://salsa.debian.org/ocaml-team/hol-light/-/raw/master/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch";
sha256 = "180qmxbrk3vb1ix7j77hcs8vsar91rs11s5mm8ir5352rz7ylicr";
})
];
strictDeps = true;
nativeBuildInputs = [ ocaml findlib camlp5 ];
propagatedBuildInputs = [ camlp-streams num ];
installPhase = ''
mkdir -p "$out/lib/hol_light" "$out/bin"
cp -a . $out/lib/hol_light
echo "${start_script}" > "$out/bin/hol_light"
chmod a+x "$out/bin/hol_light"
'';
meta = with lib; {
description = "Interactive theorem prover based on Higher-Order Logic";
homepage = "http://www.cl.cam.ac.uk/~jrh13/hol-light/";
license = licenses.bsd2;
platforms = platforms.unix;
maintainers = with maintainers; [ thoughtpolice maggesi vbgl ];
};
}
|
