Ok, everything worked and I made a pull request! Hopefully nothing went wrong.
On Mon, Jan 20, 2025 at 11:00 AM Thierry Arnoux <[email protected]> wrote: > 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, and one with my downloaded copy > of metamath-exe (called set.mm and metamath respectively). I've been > running the script from the 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 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 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/CABJcXbTveocbyQDEXJbXbahuDr9m-si84F4nKhaq0ZRUji-2GA%40mail.gmail.com.
