From 9d1bce933d822732b8e1b57b89f5b6b26853a2af Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Wed, 18 Sep 2024 20:07:00 +0200 Subject: [PATCH 1/2] fix README.TXT --- README.TXT | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.TXT b/README.TXT index 341300ea..242cf0a6 100644 --- a/README.TXT +++ b/README.TXT @@ -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 @@ -61,7 +61,7 @@ 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 @@ -82,7 +82,7 @@ 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 From 080b0e1b4cfae86c2af48ed764fda310dc5bc000 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Fri, 20 Sep 2024 14:18:41 +0200 Subject: [PATCH 2/2] include hints for Debian --- README.TXT | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/README.TXT b/README.TXT index 242cf0a6..07f4de4b 100644 --- a/README.TXT +++ b/README.TXT @@ -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 --------------------- @@ -50,10 +56,10 @@ 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 @@ -88,6 +94,13 @@ 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.)