From: Enrico Tassi Date: Sat, 17 Nov 2007 17:33:43 +0000 (+0000) Subject: moved to pkg-ocaml-maint X-Git-Tag: 0.4.98@7921~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8e7751f97e50bdc18537aac7478d0621d45ab956;p=helm.git moved to pkg-ocaml-maint --- diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml index a4267c5fc..73f137a43 100644 --- a/components/metadata/metadataConstraints.ml +++ b/components/metadata/metadataConstraints.ml @@ -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) diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index b9ce25174..6a1ab20e6 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -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 = diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli index cfb31a8c4..a40d00fc5 100644 --- a/components/tactics/auto.mli +++ b/components/tactics/auto.mli @@ -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 diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml index 45f981be1..874a20dcc 100644 --- a/components/tactics/autoTypes.ml +++ b/components/tactics/autoTypes.ml @@ -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 *) diff --git a/components/tactics/autoTypes.mli b/components/tactics/autoTypes.mli index 306c42daa..ab05564ff 100644 --- a/components/tactics/autoTypes.mli +++ b/components/tactics/autoTypes.mli @@ -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 diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma index 950639fed..3b2afd5dc 100644 --- a/matita/dama/excedence.ma +++ b/matita/dama/excedence.ma @@ -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 ?). diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma index 28f7858a0..0df357af5 100644 --- a/matita/dama/groups.ma +++ b/matita/dama/groups.ma @@ -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/pkg-matita/tarballs/matita-0.4.97.tar.gz b/pkg-matita/tarballs/matita-0.4.97.tar.gz deleted file mode 100644 index df3dad637..000000000 Binary files a/pkg-matita/tarballs/matita-0.4.97.tar.gz and /dev/null differ diff --git a/pkg-matita/tarballs/matita_0.4.97.orig.tar.gz b/pkg-matita/tarballs/matita_0.4.97.orig.tar.gz deleted file mode 120000 index fec03f8b9..000000000 --- a/pkg-matita/tarballs/matita_0.4.97.orig.tar.gz +++ /dev/null @@ -1 +0,0 @@ -matita-0.4.97.tar.gz \ No newline at end of file diff --git a/pkg-matita/trunk/debian/TODO.Debian b/pkg-matita/trunk/debian/TODO.Debian deleted file mode 100644 index 241896b13..000000000 --- a/pkg-matita/trunk/debian/TODO.Debian +++ /dev/null @@ -1,5 +0,0 @@ -- manpages have wrong patch for conffile -- hide: - - publish - - hbugs in cicbrowser - - light bulb diff --git a/pkg-matita/trunk/debian/changelog b/pkg-matita/trunk/debian/changelog deleted file mode 100644 index 0771f5d4e..000000000 --- a/pkg-matita/trunk/debian/changelog +++ /dev/null @@ -1,12 +0,0 @@ -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 - diff --git a/pkg-matita/trunk/debian/compat b/pkg-matita/trunk/debian/compat deleted file mode 100644 index 7ed6ff82d..000000000 --- a/pkg-matita/trunk/debian/compat +++ /dev/null @@ -1 +0,0 @@ -5 diff --git a/pkg-matita/trunk/debian/control b/pkg-matita/trunk/debian/control deleted file mode 100644 index 351f28f7c..000000000 --- a/pkg-matita/trunk/debian/control +++ /dev/null @@ -1,35 +0,0 @@ -Source: matita -Section: math -Priority: optional -Maintainer: Enrico Tassi -Uploaders: Stefano Zacchiroli -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/pkg-matita/trunk/debian/copyright b/pkg-matita/trunk/debian/copyright deleted file mode 100644 index 14913710d..000000000 --- a/pkg-matita/trunk/debian/copyright +++ /dev/null @@ -1,29 +0,0 @@ -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 - -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 - diff --git a/pkg-matita/trunk/debian/matita-standard-library.dirs b/pkg-matita/trunk/debian/matita-standard-library.dirs deleted file mode 100644 index a1564d174..000000000 --- a/pkg-matita/trunk/debian/matita-standard-library.dirs +++ /dev/null @@ -1,2 +0,0 @@ -/usr/share/matita/ma/ -/usr/share/matita/xml/ diff --git a/pkg-matita/trunk/debian/matita-standard-library.install b/pkg-matita/trunk/debian/matita-standard-library.install deleted file mode 100644 index 0627e0813..000000000 --- a/pkg-matita/trunk/debian/matita-standard-library.install +++ /dev/null @@ -1,3 +0,0 @@ -/usr/share/matita/ma/ -/usr/share/matita/xml/ -/usr/share/matita/metadata.db diff --git a/pkg-matita/trunk/debian/matita.dirs b/pkg-matita/trunk/debian/matita.dirs deleted file mode 100644 index 0dc001e7f..000000000 --- a/pkg-matita/trunk/debian/matita.dirs +++ /dev/null @@ -1,2 +0,0 @@ -/usr/bin -/usr/share/matita/ diff --git a/pkg-matita/trunk/debian/matita.install b/pkg-matita/trunk/debian/matita.install deleted file mode 100644 index 5b4c76d3c..000000000 --- a/pkg-matita/trunk/debian/matita.install +++ /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/pkg-matita/trunk/debian/matita.menu b/pkg-matita/trunk/debian/matita.menu deleted file mode 100644 index 162bf8e7b..000000000 --- a/pkg-matita/trunk/debian/matita.menu +++ /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/pkg-matita/trunk/debian/patches/00dpatch.conf b/pkg-matita/trunk/debian/patches/00dpatch.conf deleted file mode 100644 index 96bcc8772..000000000 --- a/pkg-matita/trunk/debian/patches/00dpatch.conf +++ /dev/null @@ -1,2 +0,0 @@ -conf_debianonly=1 -conf_origtargzpath=../tarballs/ diff --git a/pkg-matita/trunk/debian/patches/00list b/pkg-matita/trunk/debian/patches/00list deleted file mode 100644 index 9a27854d1..000000000 --- a/pkg-matita/trunk/debian/patches/00list +++ /dev/null @@ -1 +0,0 @@ -matita.conf.xml.in.dpatch diff --git a/pkg-matita/trunk/debian/patches/matita.conf.xml.in.dpatch b/pkg-matita/trunk/debian/patches/matita.conf.xml.in.dpatch deleted file mode 100755 index 45f1c0caf..000000000 --- a/pkg-matita/trunk/debian/patches/matita.conf.xml.in.dpatch +++ /dev/null @@ -1,60 +0,0 @@ -#! /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: 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 @@ - -- -+ - - file://$(matita.rt_base_dir) metadata.db helm helm library - file://$(matita.basedir) user.db helm helm user -- --> - - -+ - - cic:/matita/ - file://$(matita.rt_base_dir)/xml/standard-library/ -@@ -104,6 +106,7 @@ - cic:/matita/ - file://$(user.home)/.matita/xml/matita/ - -+ - - diff --git a/pkg-matita/trunk/debian/rules b/pkg-matita/trunk/debian/rules deleted file mode 100755 index 546caba1c..000000000 --- a/pkg-matita/trunk/debian/rules +++ /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 {} \;