diff options
author | Shea Levy <shea@shealevy.com> | 2011-08-24 19:16:43 +0000 |
---|---|---|
committer | Shea Levy <shea@shealevy.com> | 2011-08-24 19:16:43 +0000 |
commit | 4d70ba6cc960555c9e1f701a88517e99232b2148 (patch) | |
tree | 7fc328746167a757526bf4165584e3bfb8a83b4f /pkgs/applications/science/logic | |
parent | 5d62c65d6e085481a36c857e8b86f88d80b1c565 (diff) | |
parent | b58016b007444b25ab5256eb21896cd859038901 (diff) | |
download | nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.tar nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.tar.gz nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.tar.bz2 nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.tar.lz nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.tar.xz nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.tar.zst nixlib-4d70ba6cc960555c9e1f701a88517e99232b2148.zip |
Merge from trunk up through r28790
svn path=/nixpkgs/branches/stdenv-updates/; revision=28792
Diffstat (limited to 'pkgs/applications/science/logic')
14 files changed, 242 insertions, 248 deletions
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index a804d9f84e6a..35395bd25d1e 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -4,7 +4,7 @@ {stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}: let - version = "8.3"; + version = "8.3pl1"; in stdenv.mkDerivation { @@ -12,7 +12,7 @@ stdenv.mkDerivation { src = fetchurl { url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz"; - sha256 = "02iy4rxz1n1kc85fb3vs4xpxqfxjw87y2gvmi39fxrj8742qx0dx"; + sha256 = "0a791gsbf17y2wi0a376n78pxkhpl0lkzifhy5d3mx3lpn376j9s"; }; buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ]; @@ -23,7 +23,7 @@ stdenv.mkDerivation { configureFlagsArray=( -camldir ${ocaml}/bin -camlp5dir $(ocamlfind query camlp5) - -lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 -opt -coqide opt + -lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -opt -coqide opt ) ''; @@ -38,9 +38,12 @@ stdenv.mkDerivation { substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" substituteInPlace scripts/coqmktop.ml --replace \ "\"-I\"; \"+lablgtk2\"" \ - "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\"" + "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\"" ''; + # This post install step is needed to build ssrcoqide from the ssreflect package + # It could be made optional, but I see little harm in including it in the default + # distribution -- roconnor postInstall = '' cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/ ''; diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix index f923095f857e..d835e351cac6 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-20110813"; + src = fetchsvn { + url = http://hol-light.googlecode.com/svn/trunk; + rev = "102"; + sha256 = "5b972672db6aa1838dc5d130accd9ab6a62030c6b0c1dc4b69e42088b1ae86c9"; + }; - 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 = '' diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix b/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix deleted file mode 100644 index 9071d63c298a..000000000000 --- a/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix +++ /dev/null @@ -1,99 +0,0 @@ -{stdenv, writeTextFile, hol_light, dmtcp}: -let - mkRestartScript = checkpointFile: - let filename = "hol_light_${checkpointFile.variant}_dmtcp"; in - writeTextFile { - name = "${filename}-${hol_light.version}"; - destination = "/bin/${filename}"; - executable = true; - text = '' - #!/bin/sh - exec ${dmtcp}/bin/dmtcp_restart --quiet ${checkpointFile} - ''; - }; - - mkCkptFile = - { variant - , banner - , loads - , startCkpt ? null - , buildCommand ? '' - cp ${startCkpt} hol_light_restart.ckpt - (echo "$loadScript" | dmtcp_restart --quiet hol_light_restart.ckpt) || exit 0 - cp hol_light_restart.ckpt $out - '' - }: - stdenv.mkDerivation rec { - name = "hol_light_${variant}_dmtcp.checkpoint-${hol_light.version}"; - inherit variant banner buildCommand; - buildInputs = [ dmtcp hol_light ]; - loadScript = '' - ${loads} - dmtcp_checkpoint "${banner}";; - ''; - }; -in -rec { - hol_light_core_dmtcp = mkRestartScript hol_light_core_dmtcp_ckpt; - hol_light_sosa_dmtcp = mkRestartScript hol_light_sosa_dmtcp_ckpt; - hol_light_card_dmtcp = mkRestartScript hol_light_card_dmtcp_ckpt; - hol_light_multivariate_dmtcp = mkRestartScript hol_light_multivariate_dmtcp_ckpt; - hol_light_complex_dmtcp = mkRestartScript hol_light_complex_dmtcp_ckpt; - - hol_light_core_dmtcp_ckpt = mkCkptFile rec { - variant = "core"; - banner = ""; - loads = '' - #use "${./dmtcp_selfdestruct.ml}";; - ''; - buildCommand = '' - (echo "$loadScript" | dmtcp_checkpoint --quiet ${hol_light}/bin/start_hol_light) || exit 0 - mv ckpt* $out - ''; - }; - - hol_light_multivariate_dmtcp_ckpt = mkCkptFile { - variant = "multivariate"; - banner = "Preloaded with multivariate analysis"; - loads = '' - loadt "Multivariate/make.ml";; - ''; - startCkpt = hol_light_core_dmtcp_ckpt; - }; - - hol_light_sosa_dmtcp_ckpt = mkCkptFile { - variant = "sosa"; - banner = "Preloaded with analysis and SOS"; - loads = '' - loadt "Library/analysis.ml";; - loadt "Library/transc.ml";; - loadt "Examples/sos.ml";; - loadt "update_database.ml";; - ''; - startCkpt = hol_light_core_dmtcp_ckpt; - }; - - hol_light_card_dmtcp_ckpt = mkCkptFile { - variant = "card"; - banner = "Preloaded with cardinal arithmetic"; - loads = '' - loadt "Library/card.ml";; - loadt "update_database.ml";; - ''; - startCkpt = hol_light_core_dmtcp_ckpt; - }; - - hol_light_complex_dmtcp_ckpt = mkCkptFile { - variant = "complex"; - banner = "Preloaded with multivariate-based complex analysis"; - loads = '' - loadt "Multivariate/complexes.ml";; - loadt "Multivariate/canal.ml";; - loadt "Multivariate/transcendentals.ml";; - loadt "Multivariate/realanalysis.ml";; - loadt "Multivariate/cauchy.ml";; - loadt "Multivariate/complex_database.ml";; - ''; - startCkpt = hol_light_multivariate_dmtcp_ckpt; - }; -} diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml b/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml deleted file mode 100644 index f85a7a6c5fdf..000000000000 --- a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml +++ /dev/null @@ -1,19 +0,0 @@ -(* ------------------------------------------------------------------------- *) -(* Create a standalone HOL image. Assumes that we are running under Linux *) -(* and have the program "dmtcp" available to create checkpoints. *) -(* ------------------------------------------------------------------------- *) - -let dmtcp_checkpoint, dmtcp_selfdestruct = - let call_dmtcp opts bannerstring = - let longer_banner = startup_banner ^ " with DMTCP" in - let complete_banner = - if bannerstring = "" then longer_banner - else longer_banner^"\n "^bannerstring in - (Gc.compact(); Unix.sleep 1; - Format.print_string "Checkpointing..."; Format.print_newline(); - try ignore(Unix.system ("dmtcp_command -bc " ^ opts)) - with Unix.Unix_error _ -> (); - Format.print_string complete_banner; - Format.print_newline(); Format.print_newline()) - in - call_dmtcp "", call_dmtcp "-q";; diff --git a/pkgs/applications/science/logic/hol_light/parser_setup.patch b/pkgs/applications/science/logic/hol_light/parser_setup.patch deleted file mode 100644 index 0ad17ca1a0b0..000000000000 --- a/pkgs/applications/science/logic/hol_light/parser_setup.patch +++ /dev/null @@ -1,34 +0,0 @@ -diff -Nuar hol_light/hol.ml hol_light.nixos/hol.ml ---- hol_light/hol.ml 2010-11-03 23:09:01.000000000 +0100 -+++ hol_light.nixos/hol.ml 2010-11-03 23:10:31.000000000 +0100 -@@ -11,8 +11,8 @@ - - let hol_version = "2.20++";; - --let hol_dir = ref -- (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());; -+let hol_dir = ref "@HOL_LIGHT_SRC_DIR@";; -+Topdirs.dir_directory "@HOL_LIGHT_SRC_DIR@";; - - (* ------------------------------------------------------------------------- *) - (* Should eventually change to "ref(Filename.temp_dir_name)". *) -@@ -23,19 +23,6 @@ - let temp_path = ref "/tmp";; - - (* ------------------------------------------------------------------------- *) --(* Load in parsing extensions. *) --(* For Ocaml < 3.10, use the built-in camlp4 *) --(* and for Ocaml >= 3.10, use camlp5 instead. *) --(* ------------------------------------------------------------------------- *) -- --if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10" --then (Topdirs.dir_directory "+camlp5"; -- Topdirs.dir_load Format.std_formatter "camlp5o.cma") --else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");; -- --Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");; -- --(* ------------------------------------------------------------------------- *) - (* Load files from system and/or user-settable directories. *) - (* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual *) - (* $ character at the start of a directory. *) diff --git a/pkgs/applications/science/logic/hol_light/sources.nix b/pkgs/applications/science/logic/hol_light/sources.nix deleted file mode 100644 index b45ca4a90349..000000000000 --- a/pkgs/applications/science/logic/hol_light/sources.nix +++ /dev/null @@ -1,28 +0,0 @@ -{stdenv, fetchsvn}: - -stdenv.mkDerivation rec { - name = "hol_light_sources-${version}"; - version = "20101029"; - - src = fetchsvn { - url = http://hol-light.googlecode.com/svn/trunk; - rev = "64"; - sha256 = "91e9cac62586039b13c11af245f85a743e299892b24b39d3c7b2ee13157e87c9"; - }; - - buildCommand = '' - export HOL_DIR="$out/lib/hol_light" - ensureDir "$HOL_DIR" - cp -a "${src}" "$HOL_DIR/src" - cd "$HOL_DIR/src" - chmod +wX -R . - patch -p1 < ${./parser_setup.patch} - substituteInPlace hol.ml --subst-var-by HOL_LIGHT_SRC_DIR "$HOL_DIR/src" - ''; - - meta = { - description = "Sources for the HOL Light theorem prover"; - homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/; - license = "BSD"; - }; -} diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index b9e756e0423b..5705262f3771 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -3,7 +3,7 @@ let pname = "Isabelle"; - version = "2009-2"; + version = "2011"; name = "${pname}${version}"; theories = ["HOL" "FOL" "ZF"]; in @@ -13,7 +13,7 @@ stdenv.mkDerivation { src = fetchurl { url = "http://www.cl.cam.ac.uk/research/hvg/${pname}/dist/${name}.tar.gz"; - sha256 = "f92a275b78bd8844de47a5902e339b58f3b768c07a7fb19d8e606b68499d5ac4"; + sha256 = "ea85eb2a859891be387f020b2e45f8c9a0bd1d8bbc3902f28a429e9c61cb0b6a"; }; buildInputs = [ perl polyml nettools ]; diff --git a/pkgs/applications/science/logic/isabelle/settings.patch b/pkgs/applications/science/logic/isabelle/settings.patch index dc9c611d4886..bf509a4bac46 100644 --- a/pkgs/applications/science/logic/isabelle/settings.patch +++ b/pkgs/applications/science/logic/isabelle/settings.patch @@ -1,34 +1,32 @@ -diff -Naur Isabelle2009-1/etc/settings Isabelle2009-1-patched/etc/settings ---- Isabelle2009-1/etc/settings 2009-12-02 12:04:07.000000000 +0100 -+++ Isabelle2009-1-patched/etc/settings 2009-12-04 16:15:40.000000000 +0100 -@@ -16,15 +16,8 @@ - # Only one of the sections below should be activated. +diff -Nuar Isabelle2011/etc/settings Isabelle2011-fix/etc/settings +--- Isabelle2011/etc/settings 2011-01-30 13:02:18.000000000 +0100 ++++ Isabelle2011-fix/etc/settings 2011-05-14 22:56:04.000000000 +0200 +@@ -17,13 +17,7 @@ # Poly/ML 5.x (automated settings) --POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")" ML_PLATFORM="$ISABELLE_PLATFORM" --ML_HOME=$(choosefrom \ +-ML_HOME="$(choosefrom \ - "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ - "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ - "/usr/local/polyml/$ML_PLATFORM" \ - "/usr/share/polyml/$ML_PLATFORM" \ - "/opt/polyml/$ML_PLATFORM" \ -- $POLY_HOME) +- "")" +ML_HOME=@ML_HOME@ ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") ML_OPTIONS="-H 200" ML_SOURCES="$ML_HOME/../src" -@@ -185,13 +178,7 @@ +@@ -175,13 +169,7 @@ ### # Proof General home, look in a variety of places --PROOFGENERAL_HOME=$(choosefrom \ +-PROOFGENERAL_HOME="$(choosefrom \ - "$ISABELLE_HOME/contrib/ProofGeneral" \ - "$ISABELLE_HOME/../ProofGeneral" \ - "/usr/local/ProofGeneral" \ - "/usr/share/ProofGeneral" \ - "/opt/ProofGeneral" \ -- "") +- "")" +PROOFGENERAL_HOME=@PROOFGENERAL_HOME@ PROOFGENERAL_OPTIONS="" diff --git a/pkgs/applications/science/logic/leo2/default.nix b/pkgs/applications/science/logic/leo2/default.nix index eb3a13593480..04ab9a5b5ab3 100644 --- a/pkgs/applications/science/logic/leo2/default.nix +++ b/pkgs/applications/science/logic/leo2/default.nix @@ -11,10 +11,10 @@ let (builtins.attrNames (builtins.removeAttrs x helperArgNames)); sourceInfo = rec { baseName="leo2"; - version="1.2.6"; + version="1.2.8"; name="${baseName}_v${version}"; url="http://www.ags.uni-sb.de/~leo/${name}.tgz"; - hash="0gjgcm6nb9kzdl0y72sgvf2w2q92s1ix70lh6wjz9lj2qdf7gi1z"; + hash="d46a94f5991623386eb9061cfb0d748e258359a8c690fded173d45303e0e9e3a"; }; in rec { diff --git a/pkgs/applications/science/logic/matita/Makefile.patch b/pkgs/applications/science/logic/matita/Makefile.patch new file mode 100644 index 000000000000..64c9a13f2d07 --- /dev/null +++ b/pkgs/applications/science/logic/matita/Makefile.patch @@ -0,0 +1,11 @@ +--- matita-0.5.8/Makefile 2009-12-01 18:21:00.000000000 -0500 ++++ matita-0.5.8/Makefile 2010-09-16 10:33:59.665461260 -0400 +@@ -38,7 +38,7 @@ + uninstall: $(foreach d,$(SUBDIRS),rec@uninstall@$(d)) + + rec@%: +- $(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) DESTDIR=$(shell pwd)/$(DESTDIR) ++ $(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) + + # {{{ Distribution stuff + diff --git a/pkgs/applications/science/logic/matita/configure.patch b/pkgs/applications/science/logic/matita/configure.patch new file mode 100644 index 000000000000..9a3bbbb13f52 --- /dev/null +++ b/pkgs/applications/science/logic/matita/configure.patch @@ -0,0 +1,36 @@ +--- zzz/matita-0.5.8/configure 2009-12-01 18:21:00.000000000 -0500 ++++ matita-0.5.8/configure 2010-09-07 19:57:29.732139550 -0400 +@@ -1895,6 +1895,7 @@ + # look for METAS dir + + LIBSPATH="`pwd`/components" ++OLDCAMLPATH="$OCAMLPATH" + OCAMLPATH="$LIBSPATH/METAS" + + # creating META.* +@@ -1917,7 +1918,7 @@ + gdome2 \ + http \ + lablgtk2 \ +-lablgtksourceview2.gtksourceview2 \ ++lablgtk2.gtksourceview \ + lablgtkmathview \ + mysql \ + netstring \ +@@ -1951,14 +1952,14 @@ + $FINDLIB_CREQUIRES \ + lablgtk2.glade \ + lablgtkmathview \ +-lablgtksourceview2.gtksourceview2 \ ++lablgtk2.gtksourceview \ + helm-xmldiff \ + " + for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES + do + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $r ocaml library" >&5 + $as_echo_n "checking for $r ocaml library... " >&6; } +- if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then ++ if OCAMLPATH=$OCAMLPATH:$OLDCAMLPATH $OCAMLFIND query $r &> /dev/null; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5 + $as_echo "yes" >&6; } + else diff --git a/pkgs/applications/science/logic/matita/default.nix b/pkgs/applications/science/logic/matita/default.nix new file mode 100644 index 000000000000..6ac672193e27 --- /dev/null +++ b/pkgs/applications/science/logic/matita/default.nix @@ -0,0 +1,54 @@ +{stdenv, fetchurl, ocaml, camlp5, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, lablgtkmathview, ocaml_mysql, ocaml_sqlite3, ocamlnet, ulex08, camlzip, ocaml_pcre }: + +let + ocaml_version = (builtins.parseDrvName ocaml.name).version; + version = "0.5.8"; + pname = "matita"; + +in + +stdenv.mkDerivation { + name = "${pname}-${version}"; + + src = fetchurl { + url = "http://matita.cs.unibo.it/FILES/${pname}-${version}.orig.tar.gz"; + sha256 = "04sxklfak71khy1f07ks5c6163jbpxv6fmaw03fx8gwwlvpmzglh"; + }; + + buildInputs = [ocaml camlp5 findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre ]; + + postPatch = '' + BASH=$(type -tp bash) + substituteInPlace components/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH" + substituteInPlace matita/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH" + substituteInPlace configure --replace "ulex08" "ulex" + substituteInPlace components/METAS/meta.helm-content_pres.src --replace "ulex08" "ulex" + substituteInPlace components/content_pres/Makefile --replace "ulex08" "ulex" + substituteInPlace components/METAS/meta.helm-grafite_parser.src --replace "ulex08" "ulex" + substituteInPlace components/grafite_parser/Makefile --replace "ulex08" "ulex" + substituteInPlace configure --replace "zip" "camlzip" + substituteInPlace components/METAS/meta.helm-getter.src --replace "zip" "camlzip" + substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip" + ''; + + patches = [ ./configure.patch ./Makefile.patch ]; + + preConfigure = '' + # Setup for findlib. + OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH + RTDIR=$out/share/matita + export configureFlags="--with-runtime-dir=$RTDIR" + ''; + + postInstall = '' + ensureDir $out/bin + ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin + ''; + + meta = { + homepage = http://matita.cs.unibo.it/; + description = "Matita is an experimental, interactive theorem prover"; + license = "GPLv2+"; + maintainers = [ stdenv.lib.maintainers.roconnor ]; + }; +} diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix index 61901d545d7a..5a51fe2136a1 100644 --- a/pkgs/applications/science/logic/ssreflect/default.nix +++ b/pkgs/applications/science/logic/ssreflect/default.nix @@ -1,13 +1,12 @@ # TODO: -# - ssrcoqide does not build successfully (missing coqide libraries in the coq installation). -# - ssrcoq needs to be invoked with the explicit path to the ssreflect theory -# e.g.. ssrcoq -I /nix/store/rp09dlb2y2hpddb0xa7fyrgjlzb284ar-ssreflect-1.2/lib/coq/user-contrib/theories/ +# - coq needs to be invoked with the explicit path to the ssreflect theory +# e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ '' {stdenv, fetchurl, ocaml, camlp5, coq}: let pname = "ssreflect"; - version = "1.2"; + version = "1.3pl1"; name = "${pname}-${version}"; webpage = http://www.msr-inria.inria.fr/Projects/math-components; in @@ -16,18 +15,12 @@ stdenv.mkDerivation { inherit name; src = fetchurl { - url = "${webpage}/${name}.tgz"; - sha256 = "0800b085e6a0caec5093c6c02aacdd8dfd9cc282177e8586f14f9a9e15f64d0b"; + url = "${webpage}/${name}.tar.gz"; + sha256 = "0ykrhqb68aanl5d4dmn0vnx8m34gg0jsbdhwx2852rqi7r00b9ri"; }; buildInputs = [ ocaml camlp5 coq ]; - preBuild = '' - coq_makefile -f Make -o Makefile - substituteInPlace Makefile \ - --replace 'install -D $$i $(COQLIB)' 'install -D $$i '$out'/lib/coq' - ''; - # this fails /* postBuild = '' @@ -36,10 +29,9 @@ stdenv.mkDerivation { ''; */ - postInstall = '' + installPhase = '' + COQLIB=$out/lib/coq make -f Makefile.coq install -e ensureDir $out/bin - #cp -a bin/ssrcoq bin/ssrcoqide $out/bin - cp -a bin/ssrcoq $out/bin ''; meta = { diff --git a/pkgs/applications/science/logic/tptp/default.nix b/pkgs/applications/science/logic/tptp/default.nix new file mode 100644 index 000000000000..3211b6ebdc01 --- /dev/null +++ b/pkgs/applications/science/logic/tptp/default.nix @@ -0,0 +1,87 @@ +x@{builderDefsPackage + , yap, tcsh, perl, patchelf, pkgsi686Linux + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + ["pkgsi686Linux"]; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="TPTP"; + version="5.1.0"; + name="${baseName}-${version}"; + url="http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v${version}.tgz"; + hash="1wh2k575nn51ykg1jnwfwjqhg5x42k5vvn2spq09px26vhs4yksy"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + /* doConfigure should be removed if not needed */ + phaseNames = ["goTarget" "doUnpack" "fixPlace" "setVars" "installScripts" + "patchBinaries" "makeLinks"]; + + goTarget = a.fullDepEntry '' + ensureDir "$out"/share/ + cd "$out"/share/ + '' ["defEnsureDir" "minInit"]; + + fixPlace = a.fullDepEntry '' + cd .. + mv TPTP-* tptp + cd tptp + '' ["minInit" "doUnpack"]; + + setVars = a.noDepEntry '' + export TPTP="$PWD" + ''; + + installScripts = a.fullDepEntry '' + tcsh "$out/share/tptp/Scripts/tptp2T_install" -default + + sed -e 's@^ */bin/@@' -i TPTP2X/* + + tcsh "$out/share/tptp/TPTP2X/tptp2X_install" -default + '' ["addInputs"]; + + makeLinks = a.fullDepEntry '' + ensureDir "$out/bin" + ln -s "../share/tptp/TPTP2X/tptp2X" "$out/bin" + ln -s "../share/tptp/Scripts/tptp2T" "$out/bin" + ln -s "../share/tptp/Scripts/tptp4X" "$out/bin" + '' ["defEnsureDir" "minInit"]; + + patchBinaries = a.fullDepEntry '' + patchelf --set-interpreter "${pkgsi686Linux.glibc}"/lib/ld-linux.so.* \ + "Scripts/tptp4X" + '' ["addInputs"]; + + meta = { + description = "Thousands of problems for theorem provers and tools"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + # A GiB of data. Installation is unpacking and editing a few files. + # No sense in letting Hydra build it. + # Also, it is unclear what is covered by "verbatim" - we will edit configs + platforms = with a.lib.platforms; + []; + license = "verbatim-redistribution"; + }; + passthru = { + updateInfo = { + downloadPage = "http://tptp.org/"; + }; + }; +}) x + |