Sorry, the environment variable name should be LDFLAGS instead of LD_FLAGS ...
According to HOL4's FAQ page [1], Poly/ML works on M1 (or later) Macs, including macOS Sonoma (due to Xcode 15, otherwise -ld_classic won't be needed). [1] https://hol-theorem-prover.org/faq.html On Fri, Feb 23, 2024 at 1:38 PM Steve Arons <[email protected]> wrote: > Thank you for your reply, Chun; unfortunately the result is the same. I > now see that the Macports folks ran into the same problem with 5.9.1 in > December, which remains unsolved—they’re still distributing 5.9. > > Steve > > > On Feb 22, 2024, at 9:22 PM, Chun Tian (binghe) <[email protected]> > wrote: > > Try putting -ld_classic into your LD_FLAGS, i.e. > > export LD_FLAGS=-ld_classic > ./configure ... > > --Chun > > On Fri, Feb 23, 2024 at 1:09 PM Steve Arons <[email protected]> wrote: > >> The linker fails when writing the object code: >> >> ******Writing object code****** >> /bin/sh ./libtool --tag=CC --mode=link gcc -O3 -o poly >> polyexport.o libpolymain/libpolymain.la libpolyml/libpolyml.la >> -lstdc++ >> libtool: link: gcc -O3 -o .libs/poly polyexport.o >> libpolymain/.libs/libpolymain.a libpolyml/.libs/libpolyml.dylib -lstdc++ >> ld: LINKEDIT overlap of start of LINKEDIT and symbol table in >> '/Users/susanbeningson/poly/polyml/polyexport.o' in >> '/Users/susanbeningson/poly/polyml/polyexport.o' >> clang: *error: **linker command failed with exit code 1 (use -v to see >> invocation)* >> make[2]: *** [poly] Error 1 >> make[1]: *** [all-recursive] Error 1 >> make: *** [all] Error 2 >> >> This is clang from the Apple dev tools masquerading as gcc; is it >> necessary to use GNU gcc and the GNU bin tools? >> >> Thanks, >> Steve >> >> _______________________________________________ >> polyml mailing list >> [email protected] >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > >
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
