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.
