diff options
Diffstat (limited to 'pkgs/applications/science/logic/hol_light/default.nix')
-rw-r--r-- | pkgs/applications/science/logic/hol_light/default.nix | 61 |
1 files changed, 27 insertions, 34 deletions
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix index f923095f857..ea68738af57 100644 --- a/pkgs/applications/science/logic/hol_light/default.nix +++ b/pkgs/applications/science/logic/hol_light/default.nix @@ -1,43 +1,36 @@ -{stdenv, writeText, writeTextFile, ocaml, findlib, camlp5_transitional, hol_light_sources}: +{stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5}: -let - version = hol_light_sources.version; +stdenv.mkDerivation rec { + name = "hol_light-20110423"; + src = fetchsvn { + url = http://hol-light.googlecode.com/svn/trunk; + rev = "90"; + sha256 = "e10f32392eb94de559495f2a2977da9e325ff1f39edbcd28db701a1801566c89"; + }; - camlp5 = camlp5_transitional; + buildInputs = [ ocaml findlib camlp5 ]; - hol_light_src_dir = "${hol_light_sources}/lib/hol_light/src"; + start_script = '' + #!/bin/sh + cd "$out/lib/hol_light" + exec ${ocaml}/bin/ocaml -I "$(ocamlfind query camlp5)" -init make.ml + ''; - pa_j_cmo = stdenv.mkDerivation { - name = "pa_j.cmo"; - inherit ocaml camlp5; - buildInputs = [ ocaml camlp5 findlib ]; - buildCommand = '' - ocamlc -c \ - -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \ - -I "$(ocamlfind query camlp5)" \ - -o $out \ - "${hol_light_src_dir}/pa_j_`ocamlc -version | cut -c1-4`.ml" - ''; - }; + 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 + ''; - start_ml = writeText "start.ml" '' - Topdirs.dir_directory "${hol_light_src_dir}";; - Topdirs.dir_directory ("${camlp5}/lib/ocaml/"^Sys.ocaml_version^"/site-lib/camlp5");; - Topdirs.dir_load Format.std_formatter "camlp5o.cma";; - Topdirs.dir_load Format.std_formatter "${pa_j_cmo}";; - #use "${hol_light_src_dir}/make.ml";; + installPhase = '' + ensureDir "$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" ''; -in -writeTextFile { - name = "hol_light-${version}"; - destination = "/bin/start_hol_light"; - executable = true; - text = '' - #!/bin/sh - exec ${ocaml}/bin/ocaml -init ${start_ml} - ''; -} // { - inherit (hol_light_sources) version src; + meta = { description = "An interactive theorem prover based on Higher-Order Logic."; longDescription = '' |