Package: mizar Depends: << mizar-bin (>= 8.1.02-5.22.1191), mizar-mml (>= 8.1.02-5.22.1191), mizar-doc (>= 8.1.02-5.22.1191) << Architecture: x86_64 Epoch: 1 Version: 8.1.02-5.22.1191 Revision: 1 Description: Build and check first-order formal proofs Recommends: mizar-semantic-mml, mizar-gab, mizar-mode, mizar-gab-html DescDetail: << The Mizar project started around 1973 as an attempt to reconstruct mathematical vernacular in a computer-oriented environment. Since then a vast number of articles, representing formal developments of various parts of mathematics, have been written. Accompanying this library of proofs is a verification system for checking the correctness of a proof. Installing this package will install the Mizar binaries (which are used to check proofs for correctness), user documentation, and the MML (Mizar Mathematical Library). See the Mizar homepage, http://www.mizar.org, for more information. The Mizar community maintains a wiki; it is available at http://wiki.mizar.org . Installing this package will install the Mizar binaries, documentation, and the MML. << Maintainer: Jesse Alama Homepage: http://www.mizar.org/ Source: ftp://mizar.uwb.edu.pl/pub/system/i386-darwin/%n-8.1.02_5.22.1191-i386-darwin.tar Source-Checksum: SHA256(52a9a51f6f7295f1c0271dc81d95d6514a507ea382042185bd4a92ea2ba20173) BuildDepends: fink (>= 0.24.12) PatchFile: %n.patch PatchFile-MD5: 18ca2d1bd347f22f085253c5cbe299b5 PatchScript: sed 's|@PREFIX@|%p|g' < %{PatchFile} | patch -p1 NoSourceDirectory: true DocFiles: README License: Commercial CompileScript: << << InstallScript: << mkdir -p %i/bin tar Cxfz %i/bin mizbin.tar.gz mkdir -p %i/share/doc/mizar tar Cxfz %i/share/doc/mizar mizdoc.tar.gz mkdir -p %i/share/mizar tar Cxfz %i/share/mizar mizshare.tar.gz # emacs mkdir -p %i/share/emacs/site-lisp/mizar mv %i/share/mizar/mizar.el %i/share/emacs/site-lisp/mizar # emacsen-common setup mkdir -p %i/lib/emacsen-common/packages/install mkdir -p %i/lib/emacsen-common/packages/remove install -m 755 emacsen-install %i/lib/emacsen-common/packages/install/mizar-mode install -m 755 emacsen-remove %i/lib/emacsen-common/packages/remove/mizar-mode # The graphviz package contains a file called # %p/bin/prune; let's mark mizar's prune with a special suffix. mv %i/bin/prune %i/bin/prune.mizar << SplitOff: << Package: mizar-bin Conflicts: mizar (<< 7.8.03-4.76.959-2) RuntimeVars: << MIZFILES: %p/share/mizar << Files: << bin << << SplitOff2: << Package: mizar-mml Conflicts: mizar (<< 7.8.03-4.76.959-2) Files: << share/mizar/abstr share/mizar/miz.xml share/mizar/mizar.dct share/mizar/mizar.msg share/mizar/mml share/mizar/mml.ini share/mizar/mml.lar share/mizar/mml.vct share/mizar/prel << << SplitOff3: << Package: mizar-doc Conflicts: mizar (<< 7.8.03-4.76.959-2) Files: << share/doc/mizar/example.bib share/doc/mizar/external.bib share/doc/mizar/fm.bib share/doc/mizar/fmbibs.zip share/doc/mizar/mml.txt share/doc/mizar/COPYING.interpretation share/doc/mizar/FAQ share/doc/mizar/Mizar_FLA.tex share/doc/mizar/Mizar_FLA.pdf share/doc/mizar/replthls.txt share/doc/mizar/replths.txt share/doc/mizar/syntax.txt share/doc/mizar/xml << << SplitOff4: << Package: mizar-mode Depends: emacsen-common, %N License: GPL Description: Work with Mizar files in Emacs Homepage: http://wiki.mizar.org/bin/view/Mizar/MizarMode Files: << lib/emacsen-common/packages/install/%n lib/emacsen-common/packages/remove/%n share/emacs/site-lisp/mizar/mizar.el << InfoDocs: MizarMode PostInstScript: %p/lib/emacsen-common/emacs-package-install %n PreRmScript: %p/lib/emacsen-common/emacs-package-remove %n DescDetail: << (For more information on Mizar, see http://www.mizar.org) The Emacs authoring environment for Mizar (MizarMode) is today the authoring tool of choice for many (probably the majority of) Mizar authors. Mizar is a non-programmable and non-tactical verifier; proofs are developed in the traditional `write-compile-correct' software programming loop. While this method is in the beginning more laborious than the methods employed in tactical and programmable proof assistants, it makes the `proof code' in the long-run more readable, maintainable and reusable. This seems to be a crucial factor for a long-term and large-scale formalization effort. MizarMode has been designed to facilitate this kind of proof development by a number of `code-generating', `code-browsing' and `code-searching' methods or tools programmed or integrated within it. These methods and tools now include e.g. the automated generation of proof skeletons, proof advice using trained machine learning tools like Mizar Proof Advisor or deductive tools like MoMM, semantic browsing of the articles and abstracts, structured viewing, etc. (Adapted from the abstract to "MizarMode - Integrated Proof Assistance Tools for the Mizar Way of Formalizing Mathematics", by Josef Urban, available at http://kti.ms.mff.cuni.cz/~urban/mizmode.ps .) << DescUsage: << To get started, simply add the forms (autoload 'mizar-mode "mizar" "Major mode for editing Mizar articles." t) (autoload 'mmlquery-decode "mizar") (autoload 'mmlquery-mode "mizar") to your emacs initialization file. To configure emacs to turn on mizar-mode whenever a Mizar file is loaded, add the forms (setq auto-mode-alist (append '( ("\\.miz" . mizar-mode) ("\\.abs" . mizar-mode)) auto-mode-alist)) to your emacs initialization file. Add the form (setq format-alist (append '( "::[ \t]*Content-[Tt]ype:[ ]*text/mmlquery" mmlquery-decode nil nil mmlquery-mode)) format-alist) if you would like to use the MML Query feature (for more information about MML query, see http://mmlquery.mizar.org). In any case, the main entry point into the system is the command `mizar-mode'; type the key sequence M-x mizar-mode to being structually editing Mizar code. Finally, consider using the abbreviations defined in %p/share/doc/mizar-mode/abbrev_defs; they may make editing Mizar texts easier. << <<