-
Notifications
You must be signed in to change notification settings - Fork 25
/
README.TXT
151 lines (102 loc) · 5.58 KB
/
README.TXT
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
This package contains the metamath program and several Metamath databases.
Copyright
---------
The metamath program is copyright under the terms of the GNU GPL license
version 2 or later. See the file LICENSE.TXT in this directory.
Individual databases (*.mm files) are either public domain or under the GNU
GPL, as indicated by comments in their headers.
See http://us.metamath.org/copyright.html for further license and copyright
information that applies to the content of this package.
Instructions
------------
For Windows, click on "metamath.exe" and type "read set.mm".
For Unix/Linux/Cygwin/MacOSX using the gcc compiler, compile with the command
"cd src && gcc m*.c -o metamath", then type "./metamath set.mm" to run.
As an alternative, if you have autoconf, automake, and a C compiler, you can
compile with the command "cd src && autoreconf -i && ./configure && make".
This "autoconf" approach automatically finds your compiler and its options, and
configure takes the usual options (e.g., "--prefix=/usr"). The resulting
executable will typically be faster because it will check for and enable
available optimizations; tests found that the "improve" command ran 28% faster
on gcc when using an autoconf-generated "configure". You can again type
"./metamath set.mm" to run. After "make" you may install it elsewhere using
"sudo make install" (note that this installs ".mm" files in the pkgdata
directory, by default "/usr/local/share/metamath/"). If you install it this
way, you can then run metamath as "metamath /usr/share/metamath/set.mm", copy
set.mm locally (cp /usr/share/metamath/set.mm . ; metamath set.mm), or run
metamath and type: read "/usr/share/metamath/set.mm" (note that inside
metamath, filenames containing "/" must be quoted).
Optional enhancements
---------------------
For optimized performance under gcc, you can compile as follows:
gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \
-fomit-frame-pointer -Wall -pedantic
If your compiler supports it, you can also add the option -DINLINE=inline to
achieve the 28% performance increase described above.
On Linux/MacOSX/Unix, the Metamath program will be more pleasant to use if you
run it inside of rlwrap http://utopia.knoware.nl/~hlub/rlwrap/ (checked
3-Jun-2015) which provides up-arrow command history and other command-line
editing features. After you install rlwrap per its instructions, invoke the
Metamath program with "rlwrap ./metamath set.mm".
In some Linux distributions (such as Debian Woody), if the Backspace key does
not delete characters typed after the "MM>" prompt, try adding this line to
your ~/.bash_profile file:
stty echoe echok echoctl echoke
Using rlwrap as described above will also solve this problem.
Additional MacOSX information
-----------------------------
On MacOSX, select the Terminal application from Applications/Utilities to get
to the command line. On recent versions of MacOSX, you need to install gcc
separately. Typing "whereis gcc" will return "/usr/bin/gcc" if it is
installed. The XCode package is typically used to install it, but it can also
be installed without XCode; see
https://github.com/kennethreitz/osx-gcc-installer/ (checked 15-Feb-2014)
Optional rlwrap user interface enhancement
------------------------------------------
On Linux/MacOSX/Unix, the Metamath program will be more pleasant to use if you
run it inside of rlwrap:
http://utopia.knoware.nl/~hlub/uck/rlwrap/ (checked 15-Feb-2014)
which provides up-arrow command history and other command-line editing
features. After you install rlwrap per its instructions, invoke the Metamath
program with "rlwrap ./metamath set.mm".
The Windows version of the Metamath program was compiled with lcc, which has
similar features built-in.)
Windows Compilation
-------------------
To reproduce the included metamath.exe for Windows, use lcc-win32 version 3.8,
with the following command:
lc -O m*.c -o metamath.exe
Further suggestions
-------------------
Once in the program, use the "help" command to guide you. For more
information, see the Metamath book available at http://metamath.org .
To uninstall
------------
To uninstall, just delete the "metamath" directory - nothing else (Registry,
etc.) is touched in your system.
If you used autoconf's "make install" to install it in system locations, you
can use "make uninstall" to remove it.
List of databases
-----------------
The database files included are:
set.mm - logic and set theory database (see Ch. 3 of the Metamath book).
The Metamath Proof Explorer pages were generated from this database.
nf.mm - logic and set theory database for Quine's New Foundations set
theory.
hol.mm - higher order logic (simple type theory) database.
iset.mm - intuitionistic logic database.
ql.mm - quantum logic database. The Quantum Logic Explorer pages were
generated from this database.
demo0.mm - demo of simple formal system (see Ch. 2 of the Metamath book)
miu.mm - Hofstadter's MIU-system (see Appendix D of the Metamath book)
big-unifier.mm - A unification stress test (see comments in the file).
peano.mm - A nicely commented presentation of Peano arithmetic, written
by Robert Solovay (unlike the ones above, this database is NOT public
domain but is copyright under the terms of the GNU GPL license).
Source code documentation
-------------------------
Many comments in the source code are written in
https://doxygen.nl/index.html
Doxygen (Qt variant) style. If you have Doxygen installed on your computer,
you may generate HTML documentation from them with its root page placed in
build/html/index.html by running build.sh with the -d option.