mizar-mode _unstable_ port information

Package: mizar-mode
Description: Work with Mizar files in Emacs
Version: 2007.01
Revision: 5
BuildDepends: fink (>= 0.24.12)
Depends: emacsen, mizar
Recommends: mizar-gab, mizar-mode-extras
Maintainer: Jesse Alama
License: GPL
Homepage: http://wiki.mizar.org/cgi-bin/twiki/view/Mizar/MizarMode
InfoDocs: MizarMode
Source: http://www.stanford.edu/~alama/%n-%v.tar.gz
Source-MD5: 6d8fb8228806f6971cf9868eac1ecc44
PatchFile: %n.patch
PatchFile-MD5: cf45d2830665a7f494bc3a6389ff84fb
PatchScript: sed 's|@PREFIX@|%p|g' < %{PatchFile} | patch -p1
DocFiles: FAQ README_BROWSING.txt .abbrev_defs:abbrev_defs
SourceDirectory: mizar-mode
CompileScript: make -C doc info
InstallScript: <<
mkdir -p %i/share/emacs/site-lisp/mizar
install -m 644 mizar.el %i/share/emacs/site-lisp/mizar

mkdir -p %i/share/info
install -m 644 doc/MizarMode.info %i/share/info/MizarMode

mkdir -p %i/lib/emacsen-common/packages/install
mkdir -p %i/lib/emacsen-common/packages/remove
install -m 755 fink/emacsen-install %i/lib/emacsen-common/packages/install/%n
install -m 755 fink/emacsen-remove %i/lib/emacsen-common/packages/remove/%n
<<
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.
<<