You probably simply have to add metamath to your PATH environment variable <https://en.wikipedia.org/wiki/PATH_(variable)>.
On 20/01/2025 16:44, Noam Pasman wrote:
Ok, everything's worked except for actually using the scripts/rewrap command itself. Currently, I have one folder with two separate directories: one with my forked repository of set.mm <http://set.mm>, and one with my downloaded copy of metamath-exe (called set.mm <http://set.mm> and metamath respectively). I've been running the script from the set.mm <http://set.mm> directory, since that's where the script is located, but the script calls ./metamath at the beginning which seems to only work while in the metamath/src directory. The commands in the script then refer to a set.mm <http://set.mm> file, but there is no such file in the metamath/src directory (there is one that comes with the metamath directory and one in the set.mm <http://set.mm> directory that I've been editing and intend to eventually commit). I think the error might be in where I put the directories? The script seems to have a precise notion of which directory is supposed to be where and I don't want to interfere with that too much. On Mon, Jan 20, 2025 at 12:26 AM Jim Kingdon <[email protected]> wrote: On 1/19/25 19:41, Noam Pasman wrote: > line 8: metamath: command not found > I assume this means I have to install metamath-exe? Yup! > I downloaded it and tried to run "gcc *.c -o metamath" but got another > error: > zsh: no matches found: *.c > Does this mean I don't have GCC and need to download it? The error means there are no files named *.c in the current directory. Did you cd to the src directory? The version of the above command, at least in the version of metamath-exe from git, is cd src && gcc m*.c -o metamath As for whether you have gcc, you can run "gcc -v" to print the gcc version if gcc is available. > Or is there a way to validate and format without it (preferably > without metamath-exe entirely)? You can make a github fork and push up a pull request to run the tests there. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbQDcHJDrZD3bXEQiC%3DuVtUfvAYRqQbPSXubDj5bej86Mw%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CABJcXbQDcHJDrZD3bXEQiC%3DuVtUfvAYRqQbPSXubDj5bej86Mw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/1ebe36bd-8363-4325-8b9b-78208fefeaf0%40gmx.net.
