tjh.dev
1{
2 lib,
3 stdenv,
4 runtimeShell,
5 fetchFromGitHub,
6 ocaml,
7 findlib,
8 num,
9 zarith,
10 camlp5,
11 camlp-streams,
12}:
13
14let
15 use_zarith = lib.versionAtLeast ocaml.version "4.14";
16 load_num =
17 if use_zarith then
18 ''
19 -I ${zarith}/lib/ocaml/${ocaml.version}/site-lib/zarith \
20 -I ${zarith}/lib/ocaml/${ocaml.version}/site-lib/stublibs \
21 ''
22 else
23 lib.optionalString (num != null) ''
24 -I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \
25 -I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \
26 -I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs \
27 '';
28
29 start_script = ''
30 #!${runtimeShell}
31 cd $out/lib/hol_light
32 export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}${camlp5}/lib/ocaml/${ocaml.version}/site-lib/"
33 exec ${ocaml}/bin/ocaml \
34 -I \`${camlp5}/bin/camlp5 -where\` \
35 ${load_num} \
36 -I ${findlib}/lib/ocaml/${ocaml.version}/site-lib/ \
37 -I ${camlp-streams}/lib/ocaml/${ocaml.version}/site-lib/camlp-streams camlp_streams.cma \
38 -init make.ml
39 '';
40in
41
42stdenv.mkDerivation {
43 pname = "hol_light";
44 version = "unstable-2024-07-07";
45
46 src = fetchFromGitHub {
47 owner = "jrh13";
48 repo = "hol-light";
49 rev = "16b184e30e7e3fe9add7d1ee93242323ed2e1726";
50 hash = "sha256-V0OtsmX5pa+CH3ZXmNG3juXwXZ5+A0k13eMCAfaRziQ=";
51 };
52
53 patches = [ ./0004-Fix-compilation-with-camlp5-7.11.patch ];
54
55 strictDeps = true;
56
57 nativeBuildInputs = [
58 ocaml
59 findlib
60 camlp5
61 ];
62 propagatedBuildInputs = [
63 camlp-streams
64 (if use_zarith then zarith else num)
65 ];
66
67 installPhase = ''
68 mkdir -p "$out/lib/hol_light" "$out/bin"
69 cp -a . $out/lib/hol_light
70 echo "${start_script}" > "$out/bin/hol_light"
71 chmod a+x "$out/bin/hol_light"
72 '';
73
74 meta = with lib; {
75 description = "Interactive theorem prover based on Higher-Order Logic";
76 homepage = "http://www.cl.cam.ac.uk/~jrh13/hol-light/";
77 license = licenses.bsd2;
78 platforms = platforms.unix;
79 maintainers = with maintainers; [
80 thoughtpolice
81 maggesi
82 vbgl
83 ];
84 };
85}