--- matita-0.5.8.orig/debian/changelog +++ matita-0.5.8/debian/changelog @@ -0,0 +1,188 @@ +matita (0.5.8-2ubuntu1) oneiric; urgency=low + + * Apply r11210 from upstream SVN to account for changes in the signatures + of Gramext.Slist0sep and Gramext.Slist1sep. + + -- Colin Watson Sat, 21 May 2011 09:44:50 +0100 + +matita (0.5.8-2build3) oneiric; urgency=low + + * Rebuild for OCaml 3.12.0. + + -- Colin Watson Fri, 20 May 2011 19:28:57 +0100 + +matita (0.5.8-2build2) lucid; urgency=low + + * No change rebuild for libmysqlclient transition. + + -- Chuck Short Fri, 16 Apr 2010 12:12:58 -0400 + +matita (0.5.8-2build1) lucid; urgency=low + + * No change rebuild for libmysqlclient transition. + + -- Chuck Short Mon, 12 Apr 2010 13:38:13 -0400 + +matita (0.5.8-2) unstable; urgency=low + + * Conflict and replace matita-standard-library (Closes: #559261) + * suggest matita-doc + + -- Enrico Tassi Fri, 04 Dec 2009 14:32:45 +0100 + +matita (0.5.8-1) unstable; urgency=low + + * New upstream release supporting lablgtksourceview2 + * Added docbook-xsl and docbook-xml as build-depend-indep (Closes: #532289) + * Removed debian/patches/lablgtk2.14.dpatch, added upstream + * Added README.source + * build-depend on lablgtksourceview2 + * build-depend on debhelper >= 5 + * Standards-version set to 3.8.3 + + -- Enrico Tassi Wed, 02 Dec 2009 00:10:57 +0100 + +matita (0.5.7-2) unstable; urgency=low + + * rebuild against ocaml 3.11 + * copyright file points to versioned licenses + + -- Enrico Tassi Fri, 20 Mar 2009 18:19:50 +0100 + +matita (0.5.7-1) unstable; urgency=low + + * New upstream release + + -- Enrico Tassi Sun, 15 Feb 2009 16:04:54 +0100 + +matita (0.5.6-1) experimental; urgency=low + + * New upstream bugfix release + + -- Enrico Tassi Mon, 01 Dec 2008 19:11:51 +0100 + +matita (0.5.5-2) experimental; urgency=low + + * Bumped standards-version to 3.8.0, no changes needed + * Added matita-doc package to contain the .html and .pdf versions of + the user manual + * Added matita-doc.doc-base to register the user manual shipped by + matita-doc + * Relaxed dependency of matita-standard-library to >= making it + bin-nmuable. The bin-nmu is safe only if the OCaml compiler used to + build the binary package has the same marshalling convention + of the one used to build the arch-all package. (Closes: #454176) + + -- Enrico Tassi Sat, 22 Nov 2008 15:45:34 +0100 + +matita (0.5.5-1) experimental; urgency=low + + * New upstream bugfix release + + -- Enrico Tassi Mon, 17 Nov 2008 18:24:52 +0100 + +matita (0.5.4-1) experimental; urgency=low + + * New upstream bugfix release + + -- Enrico Tassi Sun, 19 Oct 2008 10:24:36 +0200 + +matita (0.5.3-1) unstable; urgency=low + + * New upstream bugfix release + + -- Enrico Tassi Wed, 23 Jul 2008 23:32:19 +0200 + +matita (0.5.2-1) unstable; urgency=low + + * New upstream release + + -- Enrico Tassi Wed, 02 Jul 2008 11:39:06 +0200 + +matita (0.5.1-1) unstable; urgency=medium + + * New upstream release + + -- Enrico Tassi Thu, 29 May 2008 10:14:28 +0200 + +matita (0.5.0-1) unstable; urgency=low + + * New upstream release + + -- Enrico Tassi Fri, 09 May 2008 18:47:36 +0200 + +matita (0.5.0~rc1-1) unstable; urgency=low + + * New upstream release candidate, fixing many relevant bugs and cleaning up + the standard library of theorems + * Strict dependency over libgtkmathview >= 0.8.0-2 + + -- Enrico Tassi Thu, 01 May 2008 14:11:10 +0200 + +matita (0.4.98-7) unstable; urgency=medium + + * Added dependency on the bytecode interpreted (ocaml-base-nox-$OCAMLABI) + on architectures that do not compile in native code. + + -- Enrico Tassi Mon, 03 Mar 2008 10:34:52 +0100 + +matita (0.4.98-6) unstable; urgency=medium + + [ Stefano Zacchiroli ] + * setting me and Enrico as uploaders, d-o-m as maintainer + * fixing vcs-svn field with the new, official field name + * update standards-version, no changes needed + + [ Enrico Tassi ] + * rebuilt against ocaml 3.10.1 + + -- Enrico Tassi Sun, 02 Mar 2008 22:27:52 +0100 + +matita (0.4.98-5) unstable; urgency=low + + * Added patch to disallow native compilers on alpha and ia64 + + -- Enrico Tassi Sat, 08 Dec 2007 11:29:31 +0100 + +matita (0.4.98-4) unstable; urgency=low + + * Bumped version on camlp5 >= 5.04 and ulex08 >= 0.8-4 + * Added patch to remove dependency on Coq numbers in number_notation.ml + + -- Enrico Tassi Wed, 05 Dec 2007 13:45:27 +0100 + +matita (0.4.98-3) unstable; urgency=low + + * Bumped again dependencies over liblablgtkmathview-ocaml-dev + + -- Enrico Tassi Tue, 27 Nov 2007 10:31:55 +0100 + +matita (0.4.98-2) unstable; urgency=low + + * updated dependency among liblablgtkmathview-ocaml-dev to + possible fix FTBFS + + -- Enrico Tassi Mon, 26 Nov 2007 19:14:53 +0100 + +matita (0.4.98-1) unstable; urgency=low + + [ Stefano Zacchiroli ] + * fix Vcs-* fields to match pkg-ocaml-maint repository settings + + [ Enrico Tassi ] + * Fixed dependencies among camlp5, ulex08 and findlib (Closes: #451896) + + -- Enrico Tassi Tue, 20 Nov 2007 13:47:26 +0100 + +matita (0.4.97-1) unstable; urgency=low + + * New version svn tag 0.4.96. + + -- Enrico Tassi Fri, 16 Nov 2007 20:37:55 +0100 + +matita (0.4.96-1) unstable; urgency=low + + * First upload of svn tag 0.4.96 (Closes: #448156). + + -- Enrico Tassi Fri, 26 Oct 2007 11:25:03 +0200 + --- matita-0.5.8.orig/debian/matita.menu +++ matita-0.5.8/debian/matita.menu @@ -0,0 +1,6 @@ +?package(matita):needs="X11" \ + section="Applications/Science/Mathematics" \ + title="Matita" \ + longtitle="Matita interactive theorem prover" \ + command="/usr/bin/matita" \ + icon="/usr/share/matita/icons/matita-32.xpm" --- matita-0.5.8.orig/debian/rules +++ matita-0.5.8/debian/rules @@ -0,0 +1,61 @@ +#!/usr/bin/make -f + +include /usr/share/cdbs/1/class/makefile.mk +include /usr/share/cdbs/1/class/autotools.mk +include /usr/share/cdbs/1/rules/debhelper.mk +include /usr/share/cdbs/1/rules/dpatch.mk + +DEB_CONFIGURE_EXTRA_FLAGS := \ + --with-runtime-dir=/usr/share/matita \ + --prefix=/usr/ \ + --with-dbhost=FAKE_HOST +DEB_DESTDIR := debian/tmp/ +DEB_DH_INSTALL_SOURCEDIR := $(DEB_DESTDIR) +DEB_DH_COMPRESS_ARGS := -X.pdf +# don't perform regular installation +DEB_MAKE_INSTALL_TARGET := +OCAMLABI=$(shell ocamlc -version) + +common-install-arch:: + # install matita + make install-arch DESTDIR=$(DEB_DESTDIR) MATITA_CFLAGS=-noinnertypes + # generate manpages + mkdir -p $(DEB_DESTDIR)/usr/share/man/man1/ + MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \ + help2man --name="Matita interative theorem prover - batch compiler" -N \ + $(DEB_DESTDIR)/usr/share/matita/matitac \ + | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitac.1.gz + MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \ + help2man --name="Matita interative theorem prover - cleanup tool" -N \ + $(DEB_DESTDIR)/usr/share/matita/matitaclean \ + | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitaclean.1.gz + MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \ + help2man --name="Matita interative theorem prover - dependency analyzer" -N \ + $(DEB_DESTDIR)/usr/share/matita/matitadep \ + | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitadep.1.gz + if [ -e $(DEB_DESTDIR)/usr/share/matita/matitac.opt ]; then\ + ln -s /usr/share/man/man1/matitac.1.gz \ + $(DEB_DESTDIR)/usr/share/man/man1/matitac.opt.1.gz;\ + fi + # install .opt .byte (symlinks are installed with .install + mkdir -p debian/matita/usr/bin/ + cp matita/matita.byte debian/matita/usr/bin/ || true + cp matita/matitac.byte debian/matita/usr/bin/ || true + cp matita/matita.opt debian/matita/usr/bin/ || true + cp matita/matitac.opt debian/matita/usr/bin/ || true + # make depend on the interpreter if needed + if [ ! -e matita/matitac.opt ]; then \ + echo "interpreter:Depends=ocaml-base-nox-$(OCAMLABI)" \ + >> debian/matita.substvars; \ + else \ + echo "interpreter:Depends=" \ + >> debian/matita.substvars; \ + fi + + +common-install-indep:: + # doc generation and installation + mkdir -p debian/matita-doc/usr/share/doc/matita-doc/ + make -C matita/help/C/ install DESTDIR=$(shell pwd)/debian/matita-doc/usr/share/doc/matita-doc/ + # install matita library + make install-indep DESTDIR=$(DEB_DESTDIR) MATITA_CFLAGS=-noinnertypes --- matita-0.5.8.orig/debian/matita-standard-library.install +++ matita-0.5.8/debian/matita-standard-library.install @@ -0,0 +1,3 @@ +/usr/share/matita/ma/ +/usr/share/matita/xml/ +/usr/share/matita/metadata.db --- matita-0.5.8.orig/debian/svn-deblayout +++ matita-0.5.8/debian/svn-deblayout @@ -0,0 +1 @@ +tagsUrl=svn+ssh://svn.debian.org/svn/pkg-ocaml-maint/tags/packages/matita --- matita-0.5.8.orig/debian/matita-doc.doc-base +++ matita-0.5.8/debian/matita-doc.doc-base @@ -0,0 +1,12 @@ +Document: matita-manual +Title: Matita user manual +Author: HELM Team +Abstract: User manual of the Matita interactive theorem prover. +Section: Science/Mathematics + +Format: PDF +Files: /usr/share/doc/matita-doc/pdf/matita.pdf + +Format: HTML +Index: /usr/share/doc/matita-doc/html/index.html +Files: /usr/share/doc/matita-doc/html/* --- matita-0.5.8.orig/debian/README.source +++ matita-0.5.8/debian/README.source @@ -0,0 +1 @@ +Please refer to /usr/share/doc/dpatch/README.source.gz --- matita-0.5.8.orig/debian/matita.dirs +++ matita-0.5.8/debian/matita.dirs @@ -0,0 +1,2 @@ +/usr/bin +/usr/share/matita/ --- matita-0.5.8.orig/debian/compat +++ matita-0.5.8/debian/compat @@ -0,0 +1 @@ +5 --- matita-0.5.8.orig/debian/control +++ matita-0.5.8/debian/control @@ -0,0 +1,39 @@ +Source: matita +Section: math +Priority: optional +Maintainer: Ubuntu Developers +XSBC-Original-Maintainer: Debian OCaml Maintainers +Uploaders: Enrico Tassi , Stefano Zacchiroli +Build-Depends: ocaml (>= 3.10.2), ocaml-findlib (>= 1.2.1-2), libgdome2-ocaml-dev, liblablgtk2-ocaml-dev, liblablgtkmathview-ocaml-dev (>= 0.7.8-3), libsqlite3-ocaml-dev, libocamlnet-ocaml-dev, libzip-ocaml-dev, libhttp-ocaml-dev, ocaml-ulex08 (>= 0.8-4), libexpat-ocaml-dev, debhelper (>= 5), cdbs, libmysql-ocaml-dev, camlp5 (>= 5.04), liblablgtksourceview2-ocaml-dev, dpatch, help2man, libgtkmathview-dev (>= 0.8.0-2) +Build-Depends-Indep: xsltproc, dblatex, docbook-xsl, docbook-xml +Standards-Version: 3.8.3 +Vcs-Svn: svn://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/matita/trunk +Vcs-Browser: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/matita/trunk/ +Homepage: http://matita.cs.unibo.it + +Package: matita +Architecture: any +Depends: ${shlibs:Depends}, ${interpreter:Depends}, ${misc:Depends} +Recommends: graphviz, yelp +Suggests: matita-doc +Conflicts: matita-standard-library +Replaces: matita-standard-library +Description: interactive theorem prover + Matita is a graphical interactive theorem prover based on the Calculus of + (Co)Inductive Constructions. + . + Matita adopts XML-encoded proof objects are produced for storage and exchange. + This makes it compatible, at some extent, with Coq. + . + The graphical interface has been inspired by CtCoq and Proof General. It + supports high quality bidimensional rendering of proofs and formulae + transformed on-the-fly to MathML markup + +Package: matita-doc +Architecture: all +Suggests: matita, yelp +Depends: ${misc:Depends} +Section: doc +Description: user manual of the Matita interactive theorem prover + This package contains the PDF and HTML formatted Matita user manual. + --- matita-0.5.8.orig/debian/copyright +++ matita-0.5.8/debian/copyright @@ -0,0 +1,29 @@ +This package was debianized by Enrico Tassi +Wed Oct 17 17:48:32 CEST 2007. + +It was downloaded from http://matita.cs.unibo.it. + +Copyright © 2000-2007 The Matita Team. +The software is released under the terms of the GNU/GPL license. +See /usr/share/common-licenses/GPL-2 + +File components/extlib/trie.ml: +Copyright (C) 2000 Jean-Christophe FILLIATRE +Released under LGPL version 2 +See /usr/share/common-licenses/LGPL-2 + +File components/syntax_extensions/data/dictionary-tex.xml: +Copyright (C) 2002-2003 Luca Padovani , + 2003 Paolo Marinelli . +Released under LGPL version 2.1 +See /usr/share/common-licenses/LGPL-2.1 + +All .ma files are released under LGPL version 2.1 +See /usr/share/common-licenses/LGPL-2.1 + +Files components/tactics/setoids.ml, components/tactics/setoids.mli and +components/tactics/fourier.ml are part of The Coq Proof Assistant +Copyright (C) The Coq Development Team +Released under LGPL version 2.1 +See /usr/share/common-licenses/LGPL-2.1 + --- matita-0.5.8.orig/debian/matita.install +++ matita-0.5.8/debian/matita.install @@ -0,0 +1,15 @@ +usr/share/matita/help +usr/share/matita/icons +usr/share/matita/AUTHORS +usr/share/matita/LICENSE +usr/share/matita/*.xml +usr/share/matita/*.lang +usr/share/matita/*.gtkrc +usr/share/matita/*.moo +usr/share/matita/*.templ +usr/share/matita/matita usr/bin/ +usr/share/matita/matitac usr/bin/ +usr/share/matita/matitadep usr/bin/ +usr/share/matita/matitaclean usr/bin/ +usr/share/man/* usr/share/man/ +/usr/share/matita/ma/ --- matita-0.5.8.orig/debian/matita-standard-library.dirs +++ matita-0.5.8/debian/matita-standard-library.dirs @@ -0,0 +1,2 @@ +/usr/share/matita/ma/ +/usr/share/matita/xml/ --- matita-0.5.8.orig/debian/TODO.Debian +++ matita-0.5.8/debian/TODO.Debian @@ -0,0 +1 @@ +- manpages have wrong patch for conffile --- matita-0.5.8.orig/debian/patches/slist-sep.dpatch +++ matita-0.5.8/debian/patches/slist-sep.dpatch @@ -0,0 +1,51 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## slist-sep.dpatch by Colin Watson +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Port to current OCaml/CamlP5. r11210 from upstream SVN. + +@DPATCH@ +diff -urNad '--exclude=CVS' '--exclude=.svn' '--exclude=.git' '--exclude=.arch' '--exclude=.hg' '--exclude=_darcs' '--exclude=.bzr' matita~/components/content_pres/cicNotationParser.ml matita/components/content_pres/cicNotationParser.ml +--- matita~/components/content_pres/cicNotationParser.ml 2009-09-21 11:01:28.000000000 +0100 ++++ matita/components/content_pres/cicNotationParser.ml 2011-05-21 09:18:45.000000000 +0100 +@@ -211,8 +211,8 @@ + match magic with + | Ast.List0 (_, None) -> Gramext.Slist0 s + | Ast.List1 (_, None) -> Gramext.Slist1 s +- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l) +- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l) ++ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false) ++ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false) + | _ -> assert false + in + [ Env (List.map Env.list_declaration p_names), +diff -urNad '--exclude=CVS' '--exclude=.svn' '--exclude=.git' '--exclude=.arch' '--exclude=.hg' '--exclude=_darcs' '--exclude=.bzr' matita~/components/grafite_parser/print_grammar.ml matita/components/grafite_parser/print_grammar.ml +--- matita~/components/grafite_parser/print_grammar.ml 2009-05-25 16:39:26.000000000 +0100 ++++ matita/components/grafite_parser/print_grammar.ml 2011-05-21 09:18:05.000000000 +0100 +@@ -87,7 +87,7 @@ + | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt + | Snterm e | Snterml (e, _) -> is_entry_dummy e + | Slist1 x | Slist0 x -> is_symbol_dummy x +- | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y ++ | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y + | Sopt x -> is_symbol_dummy x + | Sself | Snext -> false + | Stree t -> is_tree_dummy t +@@ -186,7 +186,7 @@ + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]} @ "; + todo +- | Slist0sep (symbol,sep) -> ++ | Slist0sep (symbol,sep,false) -> + Format.fprintf fmt "[@[ "; + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "{@[ "; +@@ -200,7 +200,7 @@ + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]}+ @ "; + todo +- | Slist1sep (symbol,sep) -> ++ | Slist1sep (symbol,sep,false) -> + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "{@[ "; + let todo = visit_symbol sep todo is_son in --- matita-0.5.8.orig/debian/patches/numbers.dpatch +++ matita-0.5.8/debian/patches/numbers.dpatch @@ -0,0 +1,24 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## numbers.dpatch by Enrico Tassi +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: disable Coq numbers + +@DPATCH@ +diff -urNad trunk~/components/cic_disambiguation/number_notation.ml trunk/components/cic_disambiguation/number_notation.ml +--- trunk~/components/cic_disambiguation/number_notation.ml 2009-05-14 15:43:55.000000000 +0200 ++++ trunk/components/cic_disambiguation/number_notation.ml 2009-10-11 23:06:41.000000000 +0200 +@@ -49,7 +49,7 @@ + + let _ = + DisambiguateChoices.add_num_choice +- ("natural number", `Num_interp interp_natural_number); ++ ("natural number", `Num_interp interp_natural_number); (* + DisambiguateChoices.add_num_choice + ("Coq natural number", + `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num))); +@@ -76,3 +76,4 @@ + HelmLibraryObjects.build_bin_pos num ] + else + assert false)) ++ *) --- matita-0.5.8.orig/debian/patches/native-compilers.dpatch +++ matita-0.5.8/debian/patches/native-compilers.dpatch @@ -0,0 +1,29 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## native-compilers.dpatch by Enrico Tassi +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: disable native compilers on ia64 and alpha + +@DPATCH@ +diff -urNad trunk~/Makefile.defs.in trunk/Makefile.defs.in +--- trunk~/Makefile.defs.in 2007-11-25 15:36:52.000000000 +0100 ++++ trunk/Makefile.defs.in 2007-12-11 14:20:44.000000000 +0100 +@@ -5,7 +5,17 @@ + endif + CAMLP5O = @CAMLP5O@ + LABLGLADECC = @LABLGLADECC@ +-HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ ++# debian specific limitation of architecture on which native compilers are used ++ifeq "$(shell dpkg-architecture -qDEB_HOST_ARCH)" "alpha" ++ HAVE_OCAMLOPT = no ++else ++ifeq "$(shell dpkg-architecture -qDEB_HOST_ARCH)" "ia64" ++ HAVE_OCAMLOPT = no ++else ++ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ ++endif ++endif ++ + DISTRIBUTED = @DISTRIBUTED@ + + MATITA_REQUIRES = @FINDLIB_REQUIRES@ --- matita-0.5.8.orig/debian/patches/matita.conf.xml.in.dpatch +++ matita-0.5.8/debian/patches/matita.conf.xml.in.dpatch @@ -0,0 +1,54 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## matita.conf.xml.in.dpatch by Enrico Tassi +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: patch to use sqlite backend in the default configuration + +@DPATCH@ +diff -urNad trunk~/matita/matita.conf.xml.in trunk/matita/matita.conf.xml.in +--- trunk~/matita/matita.conf.xml.in 2008-01-11 20:13:29.000000000 +0100 ++++ trunk/matita/matita.conf.xml.in 2009-10-11 23:20:31.000000000 +0200 +@@ -50,17 +50,18 @@ + + ++ so they can coexists on the same db + + @DBHOST@ matita helm none library + @DBHOST@ matita helm none user + ++ --> ++ + ++ file://$(matita.basedir) user.db helm helm user + + + + cic:/matita/ +- file://$(matita.rt_base_dir)/xml/standard-library/ +- ro +- +- +- cic:/matita/ + file://$(user.home)/.matita/xml/matita/ + ++ + + --- matita-0.5.8.orig/debian/patches/00dpatch.conf +++ matita-0.5.8/debian/patches/00dpatch.conf @@ -0,0 +1,2 @@ +conf_debianonly=1 +conf_origtargzpath=../tarballs/ --- matita-0.5.8.orig/debian/patches/00list +++ matita-0.5.8/debian/patches/00list @@ -0,0 +1,4 @@ +matita.conf.xml.in.dpatch +numbers.dpatch +native-compilers.dpatch +slist-sep.dpatch