HOL-Theorem-Prover/HOL

Error trying to build on MacOs

Oliver-Bagin opened this issue · 1 comments

I can't get latest to compile on my machine, build fails with a linked error.
Any help would be greatly appreciated!
Thanks

edit: I am running a M3 pro chip

➜  sw_vers
ProductName:		macOS
ProductVersion:		14.4
BuildVersion:		23E214

➜  bin poly --version
Poly/ML 5.9 Release

➜  bin which poly
/opt/homebrew/bin/poly

➜  HOL git:(develop) poly < tools/smart-configure.sml
Poly/ML 5.9 Release

HOL smart configuration.

Determining configuration parameters: holdir OS poly GNUMAKE polymllibdir
OS:                 macosx
poly:               /opt/homebrew/Cellar/polyml/5.9/bin/poly
polyc:              /opt/homebrew/Cellar/polyml/5.9/bin/polyc
polymllibdir:       /opt/homebrew/Cellar/polyml/5.9/lib
holdir:             /Users/oliverbagin/Documents/Git/HOL
DOT_PATH:           NONE
MLTON:              NONE
GNUMAKE:            make

Configuration will begin with above values.  If they are wrong
press Control-C.

Will continue in 1 seconds.

Loading system specific functions
Note: Int.maxInt = SOME 4611686018427387903
Compiling system specific functions (sml)
Beginning configuration.
Making mllex
ld: LINKEDIT overlap of start of LINKEDIT and symbol table in '/private/var/folders/jr/3zwrq3n12v3_wgtn1jvt7m0r0000gn/T/polyobj.57335.o' in '/private/var/folders/jr/3zwrq3n12v3_wgtn1jvt7m0r0000gn/T/polyobj.57335.o'
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Failed to make mllex (Fail "Command failed")

See the first question in the FAQ at https://hol-theorem-prover.org/faq.html