]> matita.cs.unibo.it Git - helm.git/commitdiff
moved to pkg-ocaml-maint
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 Nov 2007 17:33:43 +0000 (17:33 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 17 Nov 2007 17:33:43 +0000 (17:33 +0000)
23 files changed:
helm/software/components/metadata/metadataConstraints.ml
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/autoTypes.ml
helm/software/components/tactics/autoTypes.mli
helm/software/matita/dama/excedence.ma
helm/software/matita/dama/groups.ma
helm/software/pkg-matita/tarballs/matita-0.4.97.tar.gz [deleted file]
helm/software/pkg-matita/tarballs/matita_0.4.97.orig.tar.gz [deleted symlink]
helm/software/pkg-matita/trunk/debian/TODO.Debian [deleted file]
helm/software/pkg-matita/trunk/debian/changelog [deleted file]
helm/software/pkg-matita/trunk/debian/compat [deleted file]
helm/software/pkg-matita/trunk/debian/control [deleted file]
helm/software/pkg-matita/trunk/debian/copyright [deleted file]
helm/software/pkg-matita/trunk/debian/matita-standard-library.dirs [deleted file]
helm/software/pkg-matita/trunk/debian/matita-standard-library.install [deleted file]
helm/software/pkg-matita/trunk/debian/matita.dirs [deleted file]
helm/software/pkg-matita/trunk/debian/matita.install [deleted file]
helm/software/pkg-matita/trunk/debian/matita.menu [deleted file]
helm/software/pkg-matita/trunk/debian/patches/00dpatch.conf [deleted file]
helm/software/pkg-matita/trunk/debian/patches/00list [deleted file]
helm/software/pkg-matita/trunk/debian/patches/matita.conf.xml.in.dpatch [deleted file]
helm/software/pkg-matita/trunk/debian/rules [deleted file]

index a4267c5fc6825faa3ccd11da33dc7e8d00a789ce..73f137a432a5ac4bbb2323ebc239d00c1503d221 100644 (file)
@@ -377,11 +377,20 @@ and signature_concl =
     | Cic.Const (u,exp_named_subst) -> 
         UriManagerSet.singleton u
     | Cic.MutInd (u, t, exp_named_subst) -> 
+        let rec projections_of uris =
+          List.flatten
+           (List.map 
+            (fun uri ->
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+              projections_of (CicUtil.projections_of_record o uri))
+            uris)
+        in
         let uri = UriManager.uri_of_uriref u t None in
-       UriManagerSet.singleton uri
+        List.fold_right UriManagerSet.add
+          (projections_of [u]) (UriManagerSet.singleton uri)
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
         let uri = UriManager.uri_of_uriref u t (Some c) in
-       UriManagerSet.singleton uri
+        UriManagerSet.singleton uri
     | Cic.Cast (t, _) -> signature_concl t
     | Cic.Prod (_, s, t) -> 
        UriManagerSet.union (signature_concl s) (signature_concl t)
index b9ce25174edefc00c876253864f9172b52933507..6a1ab20e6b798a4153720d54c1a5d6f1804dfbeb 100644 (file)
@@ -281,7 +281,7 @@ let init_cache_and_tables
            try
              let ty' = unfold context ty in
              if is_an_equality ty' then Some(t,ty') else None
-           with _ -> None) (* catturare l'eccezione giusta di unfold *)
+           with ProofEngineTypes.Fail _ -> None) 
       equations
   in
   let bag = Equality.mk_equality_bag () in
@@ -1300,7 +1300,8 @@ let auto_main tables maxm context flags universe cache elems =
     | (m, s, _, _, [],_)::orlist ->
         (* complete success *)
         Proved (m, s, orlist, tables, cache, maxm)
-    | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
+    | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist 
+      when not flags.AutoTypes.do_types ->
         (* skip since not Prop, don't even check if closed by side-effect *)
         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
     | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
@@ -1330,7 +1331,7 @@ let auto_main tables maxm context flags universe cache elems =
         (* timeout *)
         debug_print (lazy ("FAIL: TIMEOUT"));
         Gaveup (tables, cache, maxm)
-    | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
+    | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
         (* attack g *)
         match calculate_goal_ty g s m with
         | None -> 
@@ -1519,6 +1520,7 @@ let flags_of_params params ?(for_applyS=false) () =
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
  let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
+ let do_type = bool "type" false in
  let timeout = int "timeout" 0 in
   { AutoTypes.maxdepth = 
       if use_only_paramod then 2 else depth;
@@ -1537,6 +1539,7 @@ let flags_of_params params ?(for_applyS=false) () =
     AutoTypes.close_more = close_more;
     AutoTypes.dont_cache_failures = false;
     AutoTypes.maxgoalsizefactor = gsize;
+    AutoTypes.do_types = do_type;
   }
 
 let applyS_tac ~dbd ~term ~params ~universe =
index cfb31a8c4c15a7f62d0b5405e89143ea7139dfe7..a40d00fc5970fa4bb569a0213c624ccdeb44f58e 100644 (file)
@@ -49,9 +49,14 @@ val solve_rewrite_tac:
     ProofEngineTypes.tactic
 
 type auto_status = 
-  Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * 
+  Cic.context * 
+  (* or list: goalno, goaltype, grey, depth, candidates: (goalno, c) *)
+  (int * Cic.term * bool * int * (int * Cic.term) list) list * 
+  (* and list *)
   (int * Cic.term * int) list *
+  (* last moves *)
   Cic.term list
+
 val get_auto_status : unit -> auto_status
 val pause: bool -> unit
 val step : unit -> unit
index 45f981be1ffebe1d6403921a42796ddb7efc5954..874a20dccf4b366bda48cae857dbf6744a2702f6 100644 (file)
@@ -34,6 +34,7 @@ type flags = {
   use_only_paramod : bool;
   close_more : bool; 
   dont_cache_failures: bool;
+  do_types: bool;
 }
 
 let default_flags _ =
@@ -46,7 +47,9 @@ let default_flags _ =
    use_paramod=true;
    use_only_paramod=false;
    close_more=false; 
-   dont_cache_failures=false}
+   dont_cache_failures=false;
+   do_types=false;
+}
 ;;
 
 (* (metasenv, subst, (metano,depth)list *)
index 306c42daa75c22c73af7b52a399def3cfac19b67..ab05564ff3c2099819feab9d3e971d6d5d41d8a9 100644 (file)
@@ -33,7 +33,8 @@ type flags = {
   use_paramod: bool;
   use_only_paramod : bool;
   close_more : bool;
-  dont_cache_failures: bool
+  dont_cache_failures: bool;
+  do_types: bool;
 }
 
 val default_flags : unit -> flags
index 950639fed11a8e0c0cc6e7b6f3fc53981bd8fcbd..3b2afd5dc982b86c8a8308018b72bc599bc04fc2 100644 (file)
@@ -79,22 +79,22 @@ lemma eq_reflexive:∀E. reflexive ? (eq E).
 intros (E); unfold; intros (x); apply ap_coreflexive; 
 qed.
 
-lemma eq_symmetric:∀E.symmetric ? (eq E).
+lemma eq_sym_:∀E.symmetric ? (eq E).
 intros (E); unfold; intros (x y Exy); unfold; unfold; intros (Ayx); apply Exy;
 apply ap_symmetric; assumption; 
 qed.
 
-lemma eq_symmetric_:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_symmetric.
+lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_sym_.
 
-coercion cic:/matita/excedence/eq_symmetric_.con.
+coercion cic:/matita/excedence/eq_sym.con.
 
-lemma eq_transitive_: ∀E.transitive ? (eq E).
+lemma eq_trans_: ∀E.transitive ? (eq E).
 (* bug. intros k deve fare whd quanto basta *)
 intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy); 
 [apply Exy|apply Eyz] assumption.
 qed.
 
-lemma eq_transitive:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_transitive_.
+lemma eq_trans:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_trans_.
 
 (* BUG: vedere se ricapita *)
 lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?).
index 28f7858a02426fd43e0fff2086a4229c0be254cb..0df357af57a4a52084a41ad238c2d62fc9c43859 100644 (file)
@@ -94,11 +94,11 @@ coercion cic:/matita/groups/feq_plusr.con nocomposites.
 
 (* generation of coercions to make *_rew[lr] easier *)
 lemma feq_plusr_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y →  y+x ≈ z+x.
-compose feq_plusr with eq_symmetric_ (H); apply H; assumption;
+compose feq_plusr with eq_sym (H); apply H; assumption;
 qed.
 coercion cic:/matita/groups/feq_plusr_sym_.con nocomposites.
 lemma feq_plusl_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y →  x+y ≈ x+z.
-compose feq_plusl with eq_symmetric_ (H); apply H; assumption;
+compose feq_plusl with eq_sym (H); apply H; assumption;
 qed.
 coercion cic:/matita/groups/feq_plusl_sym_.con nocomposites.
       
@@ -118,9 +118,9 @@ qed.
 lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z →  y+x # z+x. 
 intros (G x y z Ayz); apply (plus_strong_extr ? (-x));
 apply (ap_rewl ??? (y + (x + -x)));
-[1: apply (eq_symmetric ??? (plus_assoc ????)); 
+[1: apply (eq_sym ??? (plus_assoc ????)); 
 |2: apply (ap_rewr ??? (z + (x + -x)));
-    [1: apply (eq_symmetric ??? (plus_assoc ????)); 
+    [1: apply (eq_sym ??? (plus_assoc ????)); 
     |2: apply (ap_rewl ??? (y + (-x+x)) (plus_comm ? x (-x)));
         apply (ap_rewl ??? (y + 0) (opp_inverse ??));
         apply (ap_rewl ??? (0 + y) (plus_comm ???));
@@ -143,27 +143,65 @@ qed.
 theorem eq_opp_plus_plus_opp_opp: 
   ∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y.
 intros (G x y); apply (plus_cancr ??? (x+y));
-apply (eq_transitive ?? 0 ? (opp_inverse ??));
-apply (eq_transitive ?? (-x + -y + x + y)); [2: apply (eq_symmetric ??? (plus_assoc ????))]
-apply (eq_transitive ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
-apply (eq_transitive ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
-apply (eq_transitive ?? (-y + 0 + y)); 
-  [2: apply feq_plusr; apply feq_plusl; apply eq_symmetric; apply opp_inverse]
-apply (eq_transitive ?? (-y + y)); 
-  [2: apply feq_plusr; apply eq_symmetric
-      apply (eq_transitive ?? (0+-y)); [apply plus_comm|apply zero_neutral]]
-apply eq_symmetric; apply opp_inverse.
+apply (eq_trans ?? 0 ? (opp_inverse ??));
+apply (eq_trans ?? (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))]
+apply (eq_trans ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
+apply (eq_trans ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
+apply (eq_trans ?? (-y + 0 + y)); 
+  [2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse]
+apply (eq_trans ?? (-y + y)); 
+  [2: apply feq_plusr; apply eq_sym; 
+      apply (eq_trans ?? (0+-y)); [apply plus_comm|apply zero_neutral]]
+apply eq_sym; apply opp_inverse.
 qed.
 
 theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x.
 intros (G x); apply (plus_cancl ??? (-x));
-apply (eq_transitive ?? (--x + -x)); [apply plus_comm]
-apply (eq_transitive ?? 0); [apply opp_inverse]
-apply eq_symmetric; apply opp_inverse;
+apply (eq_trans ?? (--x + -x)); [apply plus_comm]
+apply (eq_trans ?? 0); [apply opp_inverse]
+apply eq_sym; apply opp_inverse;
 qed.
 
 theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption]
 intro G; apply (plus_cancr ??? 0);
-apply (eq_transitive ?? 0); [apply zero_neutral;]
-apply eq_symmetric; apply opp_inverse;
+apply (eq_trans ?? 0); [apply zero_neutral;]
+apply eq_sym; apply opp_inverse;
 qed.
+
+lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z.
+intros (G x y z H1 H2); apply (plus_cancr ??? z);
+apply (eq_trans ?? 0 ?? (opp_inverse ?z));
+apply (eq_trans ?? (-y + z) ? H2);
+apply (eq_trans ?? (-y + y) ? H1);
+apply (eq_trans ?? 0 ? (opp_inverse ??));
+apply eq_reflexive;
+qed.
+
+lemma feq_oppl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → -y ≈ x → -z ≈ x.
+intros (G x y z H1 H2); apply eq_sym; apply (feq_oppr ??y);
+[2:apply eq_sym] assumption;
+qed.
+
+lemma eq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y.
+intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive;
+qed.
+
+coercion cic:/matita/groups/eq_opp.con nocomposites.
+
+lemma eq_opp_sym: ∀G:abelian_group.∀x,y:G. y ≈ x → -x ≈ -y.
+compose eq_opp with eq_sym (H); apply H; assumption;
+qed.
+
+coercion cic:/matita/groups/eq_opp_sym.con nocomposites.
+
+lemma eq_opp_plusr: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(x + z) ≈ -(y + z).
+compose feq_plusr with eq_opp(H); apply H; assumption;
+qed.
+
+coercion cic:/matita/groups/eq_opp_plusr.con nocomposites.
+
+lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y).
+compose feq_plusl with eq_opp(H); apply H; assumption;
+qed.
+
+coercion cic:/matita/groups/eq_opp_plusl.con nocomposites.
diff --git a/helm/software/pkg-matita/tarballs/matita-0.4.97.tar.gz b/helm/software/pkg-matita/tarballs/matita-0.4.97.tar.gz
deleted file mode 100644 (file)
index df3dad6..0000000
Binary files a/helm/software/pkg-matita/tarballs/matita-0.4.97.tar.gz and /dev/null differ
diff --git a/helm/software/pkg-matita/tarballs/matita_0.4.97.orig.tar.gz b/helm/software/pkg-matita/tarballs/matita_0.4.97.orig.tar.gz
deleted file mode 120000 (symlink)
index fec03f8..0000000
+++ /dev/null
@@ -1 +0,0 @@
-matita-0.4.97.tar.gz
\ No newline at end of file
diff --git a/helm/software/pkg-matita/trunk/debian/TODO.Debian b/helm/software/pkg-matita/trunk/debian/TODO.Debian
deleted file mode 100644 (file)
index 241896b..0000000
+++ /dev/null
@@ -1,5 +0,0 @@
-- manpages have wrong patch for conffile
-- hide:
-  - publish
-  - hbugs in cicbrowser
-  - light bulb
diff --git a/helm/software/pkg-matita/trunk/debian/changelog b/helm/software/pkg-matita/trunk/debian/changelog
deleted file mode 100644 (file)
index 0771f5d..0000000
+++ /dev/null
@@ -1,12 +0,0 @@
-matita (0.4.97-1) unstable; urgency=low
-
-  * New version svn tag 0.4.96.
-
- -- Enrico Tassi <gareuselesinge@debian.org>  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 <gareuselesinge@debian.org>  Fri, 26 Oct 2007 11:25:03 +0200
-
diff --git a/helm/software/pkg-matita/trunk/debian/compat b/helm/software/pkg-matita/trunk/debian/compat
deleted file mode 100644 (file)
index 7ed6ff8..0000000
+++ /dev/null
@@ -1 +0,0 @@
-5
diff --git a/helm/software/pkg-matita/trunk/debian/control b/helm/software/pkg-matita/trunk/debian/control
deleted file mode 100644 (file)
index 351f28f..0000000
+++ /dev/null
@@ -1,35 +0,0 @@
-Source: matita
-Section: math
-Priority: optional
-Maintainer: Enrico Tassi <gareuselesinge@debian.org>
-Uploaders: Stefano Zacchiroli <zack@debian.org>
-Homepage: http://matita.cs.unibo.it
-Build-Depends: ocaml (>= 3.10.0), ocaml-findlib, libgdome2-ocaml-dev, liblablgtk2-ocaml-dev, liblablgtkmathview-ocaml-dev, liblablgtksourceview-ocaml-dev, libsqlite3-ocaml-dev, libocamlnet-ocaml-dev, libzip-ocaml-dev, libhttp-ocaml-dev, ocaml-ulex08, libexpat-ocaml-dev, debhelper, cdbs, libmysql-ocaml-dev, camlp5, dpatch, help2man
-Standards-Version: 3.7.2
-XS-Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/pkg-matita/trunk/
-XS-Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/pkg-matita/trunk/
-
-Package: matita
-Architecture: any
-Depends: ${shlibs:Depends}
-Recommends: matita-standard-library, graphviz
-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-standard-library
-Architecture: all
-Depends: matita (= ${binary:Version})
-Description: standard library for the Matita interactive theorem prover
- Matita is a graphical interactive theorem prover based on the Calculus of
- (Co)Inductive Constructions. 
- .
- This package contains the standard library of theorems of the
- matita interactive theorem prover.
diff --git a/helm/software/pkg-matita/trunk/debian/copyright b/helm/software/pkg-matita/trunk/debian/copyright
deleted file mode 100644 (file)
index 1491371..0000000
+++ /dev/null
@@ -1,29 +0,0 @@
-This package was debianized by Enrico Tassi <gareuselesinge@debian.org>
-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
-
-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 <lpadovan@cs.unibo.it>,
-                   2003 Paolo Marinelli <pmarinel@cs.unibo.it>.
-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
-
diff --git a/helm/software/pkg-matita/trunk/debian/matita-standard-library.dirs b/helm/software/pkg-matita/trunk/debian/matita-standard-library.dirs
deleted file mode 100644 (file)
index a1564d1..0000000
+++ /dev/null
@@ -1,2 +0,0 @@
-/usr/share/matita/ma/
-/usr/share/matita/xml/
diff --git a/helm/software/pkg-matita/trunk/debian/matita-standard-library.install b/helm/software/pkg-matita/trunk/debian/matita-standard-library.install
deleted file mode 100644 (file)
index 0627e08..0000000
+++ /dev/null
@@ -1,3 +0,0 @@
-/usr/share/matita/ma/
-/usr/share/matita/xml/
-/usr/share/matita/metadata.db
diff --git a/helm/software/pkg-matita/trunk/debian/matita.dirs b/helm/software/pkg-matita/trunk/debian/matita.dirs
deleted file mode 100644 (file)
index 0dc001e..0000000
+++ /dev/null
@@ -1,2 +0,0 @@
-/usr/bin
-/usr/share/matita/
diff --git a/helm/software/pkg-matita/trunk/debian/matita.install b/helm/software/pkg-matita/trunk/debian/matita.install
deleted file mode 100644 (file)
index 5b4c76d..0000000
+++ /dev/null
@@ -1,16 +0,0 @@
-usr/share/matita/help
-usr/share/matita/icons
-usr/share/matita/AUTHORS
-usr/share/matita/LICENSE
-usr/share/matita/*.xml
-usr/share/matita/*.in
-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/matitamake usr/bin/
-usr/share/matita/matitadep usr/bin/
-usr/share/matita/matitaclean usr/bin/
-usr/share/man/* usr/share/man/
diff --git a/helm/software/pkg-matita/trunk/debian/matita.menu b/helm/software/pkg-matita/trunk/debian/matita.menu
deleted file mode 100644 (file)
index 162bf8e..0000000
+++ /dev/null
@@ -1,6 +0,0 @@
-?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"
diff --git a/helm/software/pkg-matita/trunk/debian/patches/00dpatch.conf b/helm/software/pkg-matita/trunk/debian/patches/00dpatch.conf
deleted file mode 100644 (file)
index 96bcc87..0000000
+++ /dev/null
@@ -1,2 +0,0 @@
-conf_debianonly=1
-conf_origtargzpath=../tarballs/
diff --git a/helm/software/pkg-matita/trunk/debian/patches/00list b/helm/software/pkg-matita/trunk/debian/patches/00list
deleted file mode 100644 (file)
index 9a27854..0000000
+++ /dev/null
@@ -1 +0,0 @@
-matita.conf.xml.in.dpatch
diff --git a/helm/software/pkg-matita/trunk/debian/patches/matita.conf.xml.in.dpatch b/helm/software/pkg-matita/trunk/debian/patches/matita.conf.xml.in.dpatch
deleted file mode 100755 (executable)
index 45f1c0c..0000000
+++ /dev/null
@@ -1,60 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## matita.conf.xml.in.dpatch by Enrico Tassi <gareuselesinge@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: No description.
-
-@DPATCH@
-diff -urNad trunk~/matita/matita.conf.xml.in trunk/matita/matita.conf.xml.in
---- trunk~/matita/matita.conf.xml.in   2007-10-29 17:13:47.000000000 +0100
-+++ trunk/matita/matita.conf.xml.in    2007-11-07 15:57:56.000000000 +0100
-@@ -49,17 +49,17 @@
-     <!-- The following snippet is used by the helm team
-          note that user's tables are named diffrently from library tables,
-        so they can coexists on the same db -->
--
-+<!--
-     <key name="metadata">@DBHOST@ matita helm none legacy</key>
-     <key name="metadata">@DBHOST@ public helm none library</key>
-     <key name="metadata">@DBHOST@ matita helm none user</key>
--
-+-->
-     <!-- The following snippet it what you want to use a local sqlite db
-          and acess remotely to the coq library trought mowgli
-     <key name="metadata">@DBHOST@ matita helm none legacy</key>
-+-->
-     <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
-     <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
--    -->
-     <!-- 
-     If you have a large amount of metadata, you may be interested in using
-@@ -90,11 +90,13 @@
-       (e.g. the Matita standard library)
-     "legacy" implies "ro"
-     -->
-+<!--
-     <key name="prefix">
-       cic:/matita/
-       file:///projects/helm/library/matita_contribs/matita
-       ro
-     </key>
-+-->
-     <key name="prefix">
-       cic:/matita/
-       file://$(matita.rt_base_dir)/xml/standard-library/
-@@ -104,6 +106,7 @@
-       cic:/matita/
-       file://$(user.home)/.matita/xml/matita/
-     </key>
-+<!--
-     <key name="prefix">
-       cic:/
-       file://@RT_BASE_DIR@/xml/legacy-library/coq/
-@@ -119,5 +122,6 @@
-       http://mowgli.cs.unibo.it/xml/
-       legacy
-     </key>
-+-->
-   </section>
- </helm_registry>
diff --git a/helm/software/pkg-matita/trunk/debian/rules b/helm/software/pkg-matita/trunk/debian/rules
deleted file mode 100755 (executable)
index 546caba..0000000
+++ /dev/null
@@ -1,53 +0,0 @@
-#!/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)
-# don't perform regular installation
-DEB_MAKE_INSTALL_TARGET :=
-
-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 - build tool" -N \
-               $(DEB_DESTDIR)/usr/share/matita/matitamake \
-               | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitamake.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
-
-common-install-indep::
-       # install matita library
-       make install-indep DESTDIR=$(DEB_DESTDIR) MATITA_CFLAGS=-noinnertypes
-       # innerypes removal
-       # find $(DEB_DESTDIR) -name \*.xml.types.gz -exec rm {} \;