@@ -23,8 +23,8 @@ For Unix/Linux/Cygwin/MacOSX using the gcc compiler, compile with the command
2323"cd src && gcc m*.c -o metamath", then type "./metamath set.mm" to run.
2424
2525As an alternative, if you have autoconf, automake, and a C compiler, you can
26- compile with the command "cd src && autoreconf -i && ./configure && make".
27- This "autoconf" approach automatically finds your compiler and its options, and
26+ compile with the command "autoreconf -i && ./configure && make". This
27+ "autoconf" approach automatically finds your compiler and its options, and
2828configure takes the usual options (e.g., "--prefix=/usr"). The resulting
2929executable will typically be faster because it will check for and enable
3030available optimizations; tests found that the "improve" command ran 28% faster
@@ -37,6 +37,12 @@ set.mm locally (cp /usr/share/metamath/set.mm . ; metamath set.mm), or run
3737metamath and type: read "/usr/share/metamath/set.mm" (note that inside
3838metamath, filenames containing "/" must be quoted).
3939
40+ Known issues with the autoconf approach: On Intel type processors x86 the
41+ configure script might want you to support 32-bit code, even if your system
42+ is natively 64-bit. This is known as cross-compiling and on Debian you need
43+ the package gcc-multilib installed. For other Linux OS a similar extension
44+ might be in order.
45+
4046
4147Optional enhancements
4248---------------------
@@ -50,18 +56,18 @@ If your compiler supports it, you can also add the option -DINLINE=inline to
5056achieve the 28% performance increase described above.
5157
5258On Linux/MacOSX/Unix, the Metamath program will be more pleasant to use if you
53- run it inside of rlwrap http ://utopia.knoware.nl/~hlub /rlwrap/ (checked
54- 3-Jun-2015) which provides up-arrow command history and other command-line
55- editing features. After you install rlwrap per its instructions, invoke the
56- Metamath program with "rlwrap ./metamath set.mm".
59+ run it inside of https ://github.com/hanslub42 /rlwrap (checked 18-Sep-2024)
60+ which provides up-arrow command history and other command-line editing
61+ features. After you install rlwrap per its instructions (see below) , invoke
62+ the Metamath program with "rlwrap ./metamath set.mm".
5763
5864In some Linux distributions (such as Debian Woody), if the Backspace key does
5965not delete characters typed after the "MM>" prompt, try adding this line to
6066your ~/.bash_profile file:
6167
6268 stty echoe echok echoctl echoke
6369
64- Using rlwrap as described above will also solve this problem.
70+ Using rlwrap as described below will also solve this problem.
6571
6672
6773Additional MacOSX information
@@ -82,12 +88,19 @@ Optional rlwrap user interface enhancement
8288On Linux/MacOSX/Unix, the Metamath program will be more pleasant to use if you
8389run it inside of rlwrap:
8490
85- http ://utopia.knoware.nl/~hlub/uck/ rlwrap/ (checked 15-Feb-2014 )
91+ https ://github.com/hanslub42/ rlwrap (checked 18-Sep-2024 )
8692
8793which provides up-arrow command history and other command-line editing
8894features. After you install rlwrap per its instructions, invoke the Metamath
8995program with "rlwrap ./metamath set.mm".
9096
97+ On Debian flavoured Linux you can use:
98+
99+ sudo apt-get install rlwrap
100+
101+ Other Linux OS might require you to build this program from sources. Be
102+ prepared to have a curses and readline library ready then.
103+
91104The Windows version of the Metamath program was compiled with lcc, which has
92105similar features built-in.)
93106
0 commit comments