Update of /cvsroot/fink/dists/10.7/stable/main/finkinfo/sci
In directory vz-cvs-3.sog:/tmp/cvs-serv5580
Added Files:
mizar-i386.info mizar-semantic-mml.info mizar-x86_64.info
mizar.patch
Log Message:
Initial commit of some mizar packages to the new stable tree.
--- NEW FILE: mizar-x86_64.info ---
Package: mizar
Depends: mizar-bin, mizar-mml, mizar-doc
Architecture: x86_64
Epoch: 1
Version: 7.12.01-4.166.1132
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 <jesse.al...@gmail.com>
Homepage: http://www.mizar.org/
Source:
ftp://mizar.uwb.edu.pl/pub/system/i386-darwin/%n-7.12.01_4.166.1132-i386-darwin.tar
Source-MD5: 4585e71b4f7115a5138b32e991a5e26e
Source2: http://ktilinux.ms.mff.cuni.cz/~urban/MizarModeDoc/MizarMode.info
Source2-MD5: b669d27408817ee86769efa1c424b1e1
Source3: http://ktilinux.ms.mff.cuni.cz/~urban/MizarModeDoc/MizarMode.pdf
Source3-MD5: 54c351365b1d4b1ce3bd0a4c302069a0
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
# emacs doc
mkdir -p %i/share/info
install -m 644 MizarMode.info %i/share/info/MizarMode
mkdir -p %i/share/doc/mizar-mode
install -m 644 MizarMode.pdf %i/share/doc/mizar-mode
# 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/absedt
bin/accom
bin/addfmsg
bin/checkvoc
bin/chklab
bin/clearenv.pl
bin/constr
bin/edtfile
bin/errflag
bin/exporter
bin/findvoc
bin/inacc
bin/irrths
bin/irrvoc
bin/lisppars
bin/listvoc
bin/makeenv
bin/mglue
bin/miz2abs
bin/miz2prel
bin/mizf
bin/msplit
bin/prune.mizar
bin/ratproof
bin/relinfer
bin/reliters
bin/relprem
bin/remflags
bin/renthlab
bin/revedt
bin/revf
bin/transfer
bin/trivdemo
bin/verifier
<<
<<
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
share/doc/%n/MizarMode.pdf
share/info/MizarMode
<<
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.
<<
<<
--- NEW FILE: mizar-semantic-mml.info ---
Package: mizar-semantic-mml
Description: Semantic HTML presentation of the MML
Version: 4.166.1132
Revision: 1
Replaces: mizar-semantic-mml (<= 4.66.942)
License: Commercial
Homepage: http://mizar.org
Source: ftp://mizar.uwb.edu.pl/pub/xmlmml/html_abstr.%v.tar.gz
Source-MD5: f00b1f11bc86e27b42f56e67c1a2666b
CompileScript: <<
<<
SourceDirectory: html
InstallScript: <<
mkdir -p %i/share/mizar/html
cp *.html %i/share/mizar/html
mkdir -p %i/share/mizar/html/proofs
cp -R proofs/* %i/share/mizar/html/proofs
<<
DescDetail: <<
This package provides a hypertext version of a rich semantic
representation of the Mizar Mathematical Library (MML).
<<
Maintainer: Jesse Alama <jesse.al...@gmail.com>
--- NEW FILE: mizar.patch ---
diff -Naur --exclude='*~' mizar/emacsen-install mizar.fink/emacsen-install
--- mizar/emacsen-install 1970-01-01 01:00:00.000000000 +0100
+++ mizar.fink/emacsen-install 2010-04-20 15:36:01.000000000 +0100
@@ -0,0 +1,33 @@
+#!/bin/bash -e
+
+set -o posix
+
+FLAVOR=${1}
+
+echo >&2 "install/mizar-mode: Handling install of emacsen flavor ${FLAVOR}"
+
+if [ ${FLAVOR} == emacs20 ]
+then
+ echo "install/mizar-mode: Skipping unsupported flavor ${FLAVOR}"
+ exit 0
+fi
+
+if [ ${FLAVOR} == emacs ]
+then
+ echo "install/mizar-mode: done."
+ exit 0
+fi
+
+echo >&2 -n "install/mizar-mode: Byte-compiling for ${FLAVOR}..."
+mkdir -p @PREFIX@/share/${FLAVOR}/site-lisp/mizar;
+ln -s -f @PREFIX@/share/emacs/site-lisp/mizar/mizar.el \
+ @PREFIX@/share/${FLAVOR}/site-lisp/mizar;
+
+cd @PREFIX@/share/${FLAVOR}/site-lisp/mizar;
+
+(${FLAVOR} --no-init-file --no-site-file --batch -f batch-byte-compile
mizar.el >&1 >&1) | gzip -9qf >
@PREFIX@/share/doc/mizar-mode/CompilationLog-${FLAVOR}.gz
+
+echo >&2 "done."
+echo >&2 "install/mizar-mode: Compilation log saved in
@PREFIX@/share/doc/mizar-ode/CompilationLog-${FLAVOR}.gz."
+
+exit 0
diff -Naur --exclude='*~' mizar/emacsen-remove mizar.fink/emacsen-remove
--- mizar/emacsen-remove 1970-01-01 01:00:00.000000000 +0100
+++ mizar.fink/emacsen-remove 2010-04-20 15:36:10.000000000 +0100
@@ -0,0 +1,14 @@
+#!/bin/bash -e
+
+set -o posix
+
+FLAVOR=${1}
+
+echo "remove/mizar-mode: Handling removal for emacsen flavor ${FLAVOR}"
+
+echo >&2 -n "remove/mizar-mode: Purging compilation log and byte-compiled
files r ${FLAVOR}..."
+rm -f @PREFIX@/share/doc/mizar-mode/CompilationLog-${FLAVOR}.gz
+rm -Rf @PREFIX@/share/${FLAVOR}/site-lisp/mizar
+echo >&2 "done."
+
+exit 0
--- NEW FILE: mizar-i386.info ---
Package: mizar
Depends: mizar-bin, mizar-mml, mizar-doc
Architecture: i386
Epoch: 1
Version: 7.12.01-4.166.1132
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 <jesse.al...@gmail.com>
Homepage: http://www.mizar.org/
Source:
ftp://mizar.uwb.edu.pl/pub/system/i386-darwin/%n-7.12.01_4.166.1132-i386-darwin.tar
Source-MD5: 4585e71b4f7115a5138b32e991a5e26e
Source2: http://ktilinux.ms.mff.cuni.cz/~urban/MizarModeDoc/MizarMode.info
Source2-MD5: b669d27408817ee86769efa1c424b1e1
Source3: http://ktilinux.ms.mff.cuni.cz/~urban/MizarModeDoc/MizarMode.pdf
Source3-MD5: 54c351365b1d4b1ce3bd0a4c302069a0
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
# emacs doc
mkdir -p %i/share/info
install -m 644 MizarMode.info %i/share/info/MizarMode
mkdir -p %i/share/doc/mizar-mode
install -m 644 MizarMode.pdf %i/share/doc/mizar-mode
# 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/absedt
bin/accom
bin/addfmsg
bin/checkvoc
bin/chklab
bin/clearenv.pl
bin/constr
bin/edtfile
bin/errflag
bin/exporter
bin/findvoc
bin/inacc
bin/irrths
bin/irrvoc
bin/lisppars
bin/listvoc
bin/makeenv
bin/mglue
bin/miz2abs
bin/miz2prel
bin/mizf
bin/msplit
bin/prune.mizar
bin/ratproof
bin/relinfer
bin/reliters
bin/relprem
bin/remflags
bin/renthlab
bin/revedt
bin/revf
bin/transfer
bin/trivdemo
bin/verifier
<<
<<
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
share/doc/%n/MizarMode.pdf
share/info/MizarMode
<<
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.
<<
<<
------------------------------------------------------------------------------
Got Input? Slashdot Needs You.
Take our quick survey online. Come on, we don't ask for help often.
Plus, you'll get a chance to win $100 to spend on ThinkGeek.
http://p.sf.net/sfu/slashdot-survey
_______________________________________________
Fink-commits mailing list
Fink-commits@lists.sourceforge.net
http://news.gmane.org/gmane.os.apple.fink.cvs
