-
Notifications
You must be signed in to change notification settings - Fork 26
/
Copy pathold-quickstart.html
72 lines (66 loc) · 2.56 KB
/
old-quickstart.html
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
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="content-type">
<title>Quick Start</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
vlink="#ff0000" alink="#000088" link="#0000ff">
<h1>Quick Start</h1>
<p>
First, install the software
(See <a href="README..md">README.md</a> and
<a href="INSTALL.html">INSTALL.html</a>).
We'll assume you also have the Metamath set.mm database installed;
by default we assume it's in the default directory
c:\set.mm\ (Windows) or "$HOME/set.mm/" (everything else).
We'll also assume that mmj2 is installed in
C:\mmj2\ (Windows) or "$HOME/mmj2" (everything else).
Then:
<ul>
<li>Windows: Run mmj2\mmj2jar\mmj2.bat
(e.g., double-click from Windows Explorer)
<li>MacOS: Run mmj2/mmj2jar/MacMMJ2.command (e.g., double-click from Finder)
<li>Linux/Unix: Run mmj2/mmj2jar/mmj2.sh
(e.g., double-click from your GUI desktop environment)
<li>Cygwin: Run mmj2/mmj2jar/mmj2-cygwin.bat
(e.g., double-click from Windows Explorer)
</ul>
<p>
These files will try to load the Metamath database set.mm, by default
from the directory c:\set.mm on Windows and "$HOME/set.mm".
You can change this, by either setting the environment variable
METAMATH_DB_DIR to the directory you want to use, or can copy that
file and edit it as you wish.
<p>
BUT...WAIT!...before running mmj2, you might want to copy that file
somewhere and edit it, or edit one the file
<tt>mmj2/mmj2jar/RunParams.txt</tt> which defines the
commands that mmj2 runs on startup.
<p>
Note: mmj2 takes a time to get started (circa 60 seconds on a slow machine
loading the large database set.mm).
Once it gets started and you've done your first unification it should
generally be quite fast.
<p>
<b>Starting the tutorial</b>:
mmj2 comes with an interactive tutorial.
Use "File/Open New Proof File", if it asks if you want to save changes
you probably should say "No",
then go to the first tutorial file
(this is probably <tt>../PATutorial/Page101.mmp</tt> depending on
where you installed it)
If you just want to watch it, you can watch a
<a href="https://www.youtube.com/watch?v=87mnU1ckbI0"
>Walkthrough of the tutorial in mmj2</a>.
<p>
There are some other sample starter files in the mmj2jar directory,
though you may need to copy and edit them for your purposes.
There is documentation on mmj2
<a href="doc/mmj2CommandLineArguments.html">Command Line Arguments</a>.
The file
<a href="mmj2jar/AnnotatedRunParms.txt">AnnotatedRunParams.txt</a> explains
the RunParams.txt file.
</body>
</html>