Update HOL Light to rev 157
This commit is contained in:
parent
b1200f1a28
commit
fa2d85fded
@ -4,28 +4,20 @@ let
|
|||||||
start_script = ''
|
start_script = ''
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
cd "$out/lib/hol_light"
|
cd "$out/lib/hol_light"
|
||||||
exec ${ocaml}/bin/ocaml -I "$(ocamlfind query camlp5)" -init make.ml
|
exec ${ocaml}/bin/ocaml -I "camlp5 -where" -init make.ml
|
||||||
'';
|
'';
|
||||||
in
|
in
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
stdenv.mkDerivation {
|
||||||
name = "hol_light-20130124";
|
name = "hol_light-20130324";
|
||||||
src = fetchsvn {
|
src = fetchsvn {
|
||||||
url = http://hol-light.googlecode.com/svn/trunk;
|
url = http://hol-light.googlecode.com/svn/trunk;
|
||||||
rev = "155";
|
rev = "157";
|
||||||
sha256 = "057223kcv7y2vcnyzvrygvdafn6mb7ycr1m5rj3fsrwz0yl8dqnr";
|
sha256 = "0d0pbnkw2gb11dn30ggfl91lhdxv86kd1fyiqn170w08n0gi805f";
|
||||||
};
|
};
|
||||||
|
|
||||||
buildInputs = [ ocaml findlib camlp5 ];
|
buildInputs = [ ocaml findlib camlp5 ];
|
||||||
|
|
||||||
buildPhase = ''
|
|
||||||
make pa_j.ml
|
|
||||||
ocamlc -c \
|
|
||||||
-pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
|
|
||||||
-I "$(ocamlfind query camlp5)" \
|
|
||||||
pa_j.ml
|
|
||||||
'';
|
|
||||||
|
|
||||||
installPhase = ''
|
installPhase = ''
|
||||||
mkdir -p "$out/lib/hol_light" "$out/bin"
|
mkdir -p "$out/lib/hol_light" "$out/bin"
|
||||||
cp -a . $out/lib/hol_light
|
cp -a . $out/lib/hol_light
|
||||||
@ -45,6 +37,6 @@ can extend it with new theorems and inference rules without compromising its
|
|||||||
soundness.
|
soundness.
|
||||||
'';
|
'';
|
||||||
homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
|
homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
|
||||||
license = "BSD";
|
license = stdenv.lib.licenses.bsd2;
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user