public/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

hol_light: fix script, upgrade to r189

Browse Source 
This also tweaks the version number to just use the SVN revision (rather
than date), since it's unambiguous and increasing anyway.

Signed-off-by: Austin Seipp <aseipp@pobox.com>
This commit is contained in:
Austin Seipp 2014-04-27 13:25:19 -05:00
parent 6859853045
commit 0f1f2115e9
2 changed files with 21 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
pkgs/applications/editors/emacs-modes/hol_light/default.nix
View File

@ -1,15 +1,12 @@
{stdenv, fetchsvn}: { stdenv, fetchsvn }:
let stdenv.mkDerivation rec {
revision = "73"; name = "hol_light-mode-${version}";
in version = "73";
stdenv.mkDerivation {
name = "hol_light_mode-${revision}";
src = fetchsvn { src = fetchsvn {
url = http://seanmcl-ocaml-lib.googlecode.com/svn/trunk/workshop/software/emacs; url = http://seanmcl-ocaml-lib.googlecode.com/svn/trunk/workshop/software/emacs;
rev = revision; rev = version;
sha256 = "3ca83098960439da149a47e1caff32536601559a77f04822be742a390c67feb7"; sha256 = "3ca83098960439da149a47e1caff32536601559a77f04822be742a390c67feb7";
}; };
@ -20,6 +17,10 @@ stdenv.mkDerivation {
''; '';
meta = { meta = {
description = "A HOL Light mode for emacs"; description = "A HOL Light mode for Emacs";
homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
license = stdenv.lib.licenses.gpl2Plus;
platforms = stdenv.lib.platforms.all;
maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
}; };
} }

28
pkgs/applications/science/logic/hol_light/default.nix
View File

@ -1,19 +1,20 @@
{stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5}: { stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5 }:
let let
start_script = '' start_script = ''
#!/bin/sh #!/bin/sh
cd "$out/lib/hol_light" cd "$out/lib/hol_light"
exec ${ocaml}/bin/ocaml -I "camlp5 -where" -init make.ml exec ${ocaml}/bin/ocaml -I \`${camlp5}/bin/camlp5 -where\` -init make.ml
''; '';
in in
stdenv.mkDerivation rec {
name = "hol_light-${version}";
version = "189";
stdenv.mkDerivation {
name = "hol_light-20140112";
src = fetchsvn { src = fetchsvn {
url = http://hol-light.googlecode.com/svn/trunk; url = http://hol-light.googlecode.com/svn/trunk;
rev = "179"; rev = version;
sha256 = "1j402s7142fj09bjijrkargwx03fvbdwmn0hgzzmi6s4p1y7gww0"; sha256 = "1v10l64rs7da2kag3wlb651i09pn83icy9n5z84j8h1iwlxzajdh";
}; };
buildInputs = [ ocaml findlib camlp5 ]; buildInputs = [ ocaml findlib camlp5 ];
@ -27,16 +28,9 @@ stdenv.mkDerivation {
meta = { meta = {
description = "Interactive theorem prover based on Higher-Order Logic"; description = "Interactive theorem prover based on Higher-Order Logic";
longDescription = '' homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
HOL Light is a computer program to help users prove interesting license = stdenv.lib.licenses.bsd2;
mathematical theorems completely formally in Higher-Order Logic. It sets platforms = stdenv.lib.platforms.unix;
a very exacting standard of correctness, but provides a number of maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
automated tools and pre-proved mathematical theorems (e.g., about
arithmetic, basic set theory and real analysis) to save the user work.
It is also fully programmable, so users can extend it with new theorems
and inference rules without compromising its soundness.
'';
homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
license = stdenv.lib.licenses.bsd2;
}; };
} }