summaryrefslogtreecommitdiffstats
path: root/pkgs/applications/science/logic/hol_light
diff options
context:
space:
mode:
authorMarco Maggesi <maggesi@math.unifi.it>2013-03-25 10:56:57 +0100
committerMarco Maggesi <maggesi@math.unifi.it>2013-03-25 10:56:57 +0100
commitfa2d85fded5b155ee9b95205195ae84e4cb7d66c (patch)
tree207e21e016b22f9dbb14f366b7df26585ab2862b /pkgs/applications/science/logic/hol_light
parentb1200f1a28d9a96dac4476afa1f29b23f8e64aa9 (diff)
Update HOL Light to rev 157
Diffstat (limited to 'pkgs/applications/science/logic/hol_light')
-rw-r--r--pkgs/applications/science/logic/hol_light/default.nix18
1 files changed, 5 insertions, 13 deletions
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index 3ba9e7eb49f6..f9549241a45c 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -4,28 +4,20 @@ let
start_script = ''
#!/bin/sh
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
stdenv.mkDerivation {
- name = "hol_light-20130124";
+ name = "hol_light-20130324";
src = fetchsvn {
url = http://hol-light.googlecode.com/svn/trunk;
- rev = "155";
- sha256 = "057223kcv7y2vcnyzvrygvdafn6mb7ycr1m5rj3fsrwz0yl8dqnr";
+ rev = "157";
+ sha256 = "0d0pbnkw2gb11dn30ggfl91lhdxv86kd1fyiqn170w08n0gi805f";
};
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 = ''
mkdir -p "$out/lib/hol_light" "$out/bin"
cp -a . $out/lib/hol_light
@@ -45,6 +37,6 @@ can extend it with new theorems and inference rules without compromising its
soundness.
'';
homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
- license = "BSD";
+ license = stdenv.lib.licenses.bsd2;
};
}