2020-03-19 11:05:24 +00:00
|
|
|
{ stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, num, camlp5 }:
|
2010-02-15 11:00:02 +00:00
|
|
|
|
2011-12-16 07:44:29 +00:00
|
|
|
let
|
2018-10-05 13:14:25 +01:00
|
|
|
load_num =
|
|
|
|
if num == null then "" else
|
|
|
|
''
|
|
|
|
-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 =
|
|
|
|
''
|
2019-02-26 11:45:54 +00:00
|
|
|
#!${runtimeShell}
|
2018-10-05 13:14:25 +01:00
|
|
|
cd $out/lib/hol_light
|
|
|
|
exec ${ocaml}/bin/ocaml \
|
|
|
|
-I \`${camlp5}/bin/camlp5 -where\` \
|
|
|
|
${load_num} \
|
|
|
|
-init make.ml
|
|
|
|
'';
|
2011-12-16 07:44:29 +00:00
|
|
|
in
|
2014-09-16 15:55:56 +01:00
|
|
|
|
2015-11-03 14:24:32 +00:00
|
|
|
stdenv.mkDerivation {
|
2019-10-08 21:59:49 +01:00
|
|
|
name = "hol_light-2019-10-06";
|
2011-12-16 07:44:29 +00:00
|
|
|
|
2015-11-03 14:24:32 +00:00
|
|
|
src = fetchFromGitHub {
|
|
|
|
owner = "jrh13";
|
|
|
|
repo = "hol-light";
|
2019-10-08 21:59:49 +01:00
|
|
|
rev = "5c91b2ded8a66db571824ecfc18b4536c103b23e";
|
|
|
|
sha256 = "0sxsk8z08ba0q5aixdyczcx5l29lb51ba4ip3d2fry7y604kjsx6";
|
2011-12-16 07:44:29 +00:00
|
|
|
};
|
|
|
|
|
2020-03-19 11:05:24 +00:00
|
|
|
patches = [(fetchpatch {
|
2020-04-01 02:11:51 +01:00
|
|
|
url = "https://salsa.debian.org/ocaml-team/hol-light/-/raw/master/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch";
|
2020-03-19 11:05:24 +00:00
|
|
|
sha256 = "180qmxbrk3vb1ix7j77hcs8vsar91rs11s5mm8ir5352rz7ylicr";
|
|
|
|
})];
|
|
|
|
|
2015-09-13 17:01:04 +01:00
|
|
|
buildInputs = [ ocaml camlp5 ];
|
2018-10-05 13:14:25 +01:00
|
|
|
propagatedBuildInputs = [ num ];
|
2016-11-29 18:30:15 +00:00
|
|
|
|
2011-05-21 12:18:35 +01:00
|
|
|
installPhase = ''
|
2012-01-18 20:16:00 +00:00
|
|
|
mkdir -p "$out/lib/hol_light" "$out/bin"
|
2011-05-21 12:18:35 +01:00
|
|
|
cp -a . $out/lib/hol_light
|
|
|
|
echo "${start_script}" > "$out/bin/hol_light"
|
|
|
|
chmod a+x "$out/bin/hol_light"
|
2010-02-15 11:00:02 +00:00
|
|
|
'';
|
2011-05-21 12:18:35 +01:00
|
|
|
|
2014-09-16 15:55:56 +01:00
|
|
|
meta = with stdenv.lib; {
|
2013-10-06 10:49:53 +01:00
|
|
|
description = "Interactive theorem prover based on Higher-Order Logic";
|
2020-04-01 02:11:51 +01:00
|
|
|
homepage = "http://www.cl.cam.ac.uk/~jrh13/hol-light/";
|
2014-09-16 15:55:56 +01:00
|
|
|
license = licenses.bsd2;
|
|
|
|
platforms = platforms.unix;
|
2019-10-07 15:44:58 +01:00
|
|
|
maintainers = with maintainers; [ thoughtpolice maggesi vbgl ];
|
2010-02-15 11:00:02 +00:00
|
|
|
};
|
|
|
|
}
|