You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi in the downloads page instructions are given for getting started with metamath. In particular after unzipping the .tar.gz one cannot immediately run gcc *.c -o metamath and expect it to work. They need to update the command to gcc src/*.c -o metamath or cd into src before executing the command.
On May 07, 2024 I downloaded the file [metamath.tar.gz](https://us.metamath.org/downloads/metamath.tar.gz) onto my Mac running Mac OS Big Sur.
After downloading this file I unzipped it with tar xvzf this command ran successfully and created a metamath directory.
I was able to cd into this directory and here are its contents
At this stage of the instructions something goes awry
The instructions clearly state to run gcc *.c -o metamath however as my screenshot above shows, there are no .c files to be found in the root and so when I run it it fails as expected.
I believe that this command needs to be run from the src directory which appears to have all the .c and .h files needed.
This command appears to work fine. And furthermore executing ./metamath set.mm afterwards seems to be fine:
The text was updated successfully, but these errors were encountered:
I think the recommended instructions should be to just run ./build.sh, which is a lot easier to remember and also breaks less often. It's quite awkward for the installation instructions to be outside of the repository; we should have the website just point to a markdown page or the readme on this repo instead, for anything more complicated than ./build.sh.
Hi in the downloads page instructions are given for getting started with metamath. In particular after unzipping the
.tar.gz
one cannot immediately rungcc *.c -o metamath
and expect it to work. They need to update the command togcc src/*.c -o metamath
orcd
intosrc
before executing the command.https://us.metamath.org/index.html#downloads
On May 07, 2024 I downloaded the file
[metamath.tar.gz](https://us.metamath.org/downloads/metamath.tar.gz)
onto my Mac running Mac OS Big Sur.After downloading this file I unzipped it with
tar xvzf
this command ran successfully and created ametamath
directory.I was able to cd into this directory and here are its contents
At this stage of the instructions something goes awry
The instructions clearly state to run
gcc *.c -o metamath
however as my screenshot above shows, there are no.c
files to be found in the root and so when I run it it fails as expected.I believe that this command needs to be run from the
src
directory which appears to have all the.c
and.h
files needed.This command appears to work fine. And furthermore executing
./metamath set.mm
afterwards seems to be fine:The text was updated successfully, but these errors were encountered: