search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
615 stars 137 forks source link

Error trying to build on MacOs #1270

Closed Oliver-Bagin closed 1 month ago

Oliver-Bagin commented 1 month ago

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")
mn200 commented 1 month ago

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