Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix README.TXT #177

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 21 additions & 8 deletions README.TXT
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ 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
compile with the command "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
Expand All @@ -37,6 +37,12 @@ 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).

Known issues with the autoconf approach: On Intel type processors x86 the
configure script might want you to support 32-bit code, even if your system
is natively 64-bit. This is known as cross-compiling and on Debian you need
the package gcc-multilib installed. For other Linux OS a similar extension
might be in order.


Optional enhancements
---------------------
Expand All @@ -50,18 +56,18 @@ 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".
run it inside of https://github.com/hanslub42/rlwrap (checked 18-Sep-2024)
which provides up-arrow command history and other command-line editing
features. After you install rlwrap per its instructions (see below), 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.
Using rlwrap as described below will also solve this problem.


Additional MacOSX information
Expand All @@ -82,12 +88,19 @@ 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)
https://github.com/hanslub42/rlwrap (checked 18-Sep-2024)

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".

On Debian flavoured Linux you can use:

sudo apt-get install rlwrap

Other Linux OS might require you to build this program from sources. Be
prepared to have a curses and readline library ready then.

The Windows version of the Metamath program was compiled with lcc, which has
similar features built-in.)

Expand Down
Loading