matita: remove broken package
As requested by Vincent Laporte.
This commit is contained in:
parent
0f8ef669ac
commit
c76ffb9253
@ -1,65 +0,0 @@
|
|||||||
{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, ocaml_mysql, ocamlnet, ulex08, camlzip, ocaml_pcre, automake, autoconf }:
|
|
||||||
|
|
||||||
let
|
|
||||||
version = "0.99.1pre130312";
|
|
||||||
pname = "matita";
|
|
||||||
in
|
|
||||||
|
|
||||||
stdenv.mkDerivation {
|
|
||||||
name = "${pname}-${version}";
|
|
||||||
|
|
||||||
src = fetchurl {
|
|
||||||
url = "http://matita.cs.unibo.it/sources/${pname}_130312.tar.gz";
|
|
||||||
sha256 = "13mjvvldv53dcdid6wmc6g8yn98xca26xq2rgq2jg700lqsni59s";
|
|
||||||
};
|
|
||||||
|
|
||||||
sourceRoot="${pname}-${version}";
|
|
||||||
|
|
||||||
unpackPhase = ''
|
|
||||||
mkdir $sourceRoot
|
|
||||||
tar -xvzf $src -C $sourceRoot
|
|
||||||
echo "source root is $sourceRoot"
|
|
||||||
'';
|
|
||||||
|
|
||||||
prePatch = ''
|
|
||||||
autoreconf -fvi
|
|
||||||
'';
|
|
||||||
|
|
||||||
buildInputs = [ocaml findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk ocaml_mysql ocamlnet ulex08 camlzip ocaml_pcre automake autoconf];
|
|
||||||
|
|
||||||
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_130312.patch ];
|
|
||||||
|
|
||||||
preConfigure = ''
|
|
||||||
# Setup for findlib.
|
|
||||||
OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
|
|
||||||
RTDIR=$out/share/matita
|
|
||||||
export configureFlags="--with-runtime-dir=$RTDIR"
|
|
||||||
'';
|
|
||||||
|
|
||||||
postInstall = ''
|
|
||||||
mkdir -p $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 = stdenv.lib.licenses.gpl2Plus;
|
|
||||||
maintainers = [ stdenv.lib.maintainers.roconnor ];
|
|
||||||
broken = true;
|
|
||||||
};
|
|
||||||
}
|
|
@ -1,11 +0,0 @@
|
|||||||
--- 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
|
|
||||||
|
|
@ -1,36 +0,0 @@
|
|||||||
--- 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
|
|
@ -1,35 +0,0 @@
|
|||||||
--- matita/configure 2011-11-22 06:04:17.000000000 -0500
|
|
||||||
+++ matita/configure 2011-11-24 11:43:11.584847938 -0500
|
|
||||||
@@ -1905,6 +1905,7 @@
|
|
||||||
# look for METAS dir
|
|
||||||
|
|
||||||
LIBSPATH="`pwd`/components"
|
|
||||||
+OLDCAMLPATH="$OCAMLPATH"
|
|
||||||
OCAMLPATH="$LIBSPATH/METAS"
|
|
||||||
|
|
||||||
# creating META.*
|
|
||||||
@@ -1927,7 +1928,7 @@
|
|
||||||
gdome2 \
|
|
||||||
http \
|
|
||||||
lablgtk2 \
|
|
||||||
-lablgtksourceview2.gtksourceview2 \
|
|
||||||
+lablgtk2.gtksourceview \
|
|
||||||
mysql \
|
|
||||||
netstring \
|
|
||||||
ulex08 \
|
|
||||||
@@ -1953,13 +1954,13 @@
|
|
||||||
FINDLIB_REQUIRES="\
|
|
||||||
$FINDLIB_CREQUIRES \
|
|
||||||
lablgtk2.glade \
|
|
||||||
-lablgtksourceview2.gtksourceview2 \
|
|
||||||
+lablgtk2.gtksourceview \
|
|
||||||
"
|
|
||||||
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
|
|
@ -1,52 +0,0 @@
|
|||||||
{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, lablgtkmathview, ocaml_mysql, ocaml_sqlite3, ocamlnet, ulex08, camlzip, ocaml_pcre }:
|
|
||||||
|
|
||||||
let
|
|
||||||
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 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 = ''
|
|
||||||
mkdir -p $out/bin
|
|
||||||
ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin
|
|
||||||
'';
|
|
||||||
|
|
||||||
meta = {
|
|
||||||
homepage = http://matita.cs.unibo.it/;
|
|
||||||
description = "Experimental, interactive theorem prover";
|
|
||||||
license = stdenv.lib.licenses.gpl2Plus;
|
|
||||||
maintainers = [ stdenv.lib.maintainers.roconnor ];
|
|
||||||
};
|
|
||||||
}
|
|
@ -21231,20 +21231,6 @@ with pkgs;
|
|||||||
|
|
||||||
ltl2ba = callPackage ../applications/science/logic/ltl2ba {};
|
ltl2ba = callPackage ../applications/science/logic/ltl2ba {};
|
||||||
|
|
||||||
#inherit (ocaml-ng.ocamlPackages_3_11_2) matita;
|
|
||||||
|
|
||||||
# Current version is 0.5.8. Official website says:
|
|
||||||
|
|
||||||
# Version 0.5.9, released on December 23, 2014, is an update of version 0.5.8
|
|
||||||
# to compile with the latter OCaml version and libraries.
|
|
||||||
# It is unsupported, but still used for teaching at the University of Bologna.
|
|
||||||
|
|
||||||
# It should allow us removing the dependency on OCaml 3.11 but I haven't been
|
|
||||||
# able to confirm because Matita depends on lablgtkmathview-0.7.2 which
|
|
||||||
# already reports as broken.
|
|
||||||
|
|
||||||
matita_130312 = lowPrio ocamlPackages.matita_130312;
|
|
||||||
|
|
||||||
metis-prover = callPackage ../applications/science/logic/metis-prover { };
|
metis-prover = callPackage ../applications/science/logic/metis-prover { };
|
||||||
|
|
||||||
mcrl2 = callPackage ../applications/science/logic/mcrl2 { };
|
mcrl2 = callPackage ../applications/science/logic/mcrl2 { };
|
||||||
|
@ -1051,12 +1051,6 @@ let
|
|||||||
camlp5 = camlp5_strict;
|
camlp5 = camlp5_strict;
|
||||||
};
|
};
|
||||||
|
|
||||||
matita = callPackage ../applications/science/logic/matita {
|
|
||||||
ulex08 = ulex08.override { camlp5 = camlp5_old_transitional; };
|
|
||||||
};
|
|
||||||
|
|
||||||
matita_130312 = callPackage ../applications/science/logic/matita/130312.nix { };
|
|
||||||
|
|
||||||
};
|
};
|
||||||
in (ocamlPackages.janeStreet // ocamlPackages);
|
in (ocamlPackages.janeStreet // ocamlPackages);
|
||||||
in lib.fix' (lib.extends overrides packageSet);
|
in lib.fix' (lib.extends overrides packageSet);
|
||||||
|
Loading…
Reference in New Issue
Block a user