Re: [polyml] Poly/ML with libgmp on x86_64-darwin

[Lawrence Paulson]

It does indeed. I just tried again with the 5.7.1 release.
Larry

> On 12 Feb 2018, at 17:01, Bernard Berthomieu  
> wrote:
> 
> 
> Does the polyml version built on your MacBook run on your other mac ?
> 
>   Bernard.
> 
> 
> On 12/02/2018 12:45, Lawrence Paulson wrote:
>> I'm not able to build poly/ML on my Mac, with or without libgmp, for about a 
>> year. The funny thing is, it builds fine on my similarly-configured MacBook 
>> Pro at home. I've given up trying to figure out why.  Upgrading to High 
>> Sierra or downloading more recent versions of the sources hasn't changed 
>> this. Something in the setup must be very fragile.
>> 
>> ld: symbol(s) not found for architecture x86_64
>> clang: error: linker command failed with exit code 1 (use -v to see 
>> invocation)
>> make[1]: *** [polyimport] Error 1
>> make: *** [install-recursive] Error 1
>> 
>> I use Homebrew, not macports.
>> 
>> Larry
>> 
>>> On 10 Feb 2018, at 07:12, Matthew Fernandez >> > wrote:
>>> 
>>> Makarius, were you saying that building Poly/ML with libgmp *at all* has 
>>> been a challenge? Or specifically building a portable Poly/ML with libgmp? 
>>> I have never had a problem building Poly/ML on macOS using a 
>>> MacPorts-installed libgmp:
>>> 
>>>CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I 
>>> /opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure
>>>make
>>> 
>>> I don’t know what the scenario is for Homebrew users, but I imagine it 
>>> would be similar. For a long time I didn’t pay much attention to macOS 
>>> questions, not having a Mac myself and after ending up with one I just 
>>> assumed the cryptic flags juggling was common knowledge. Apologies if I was 
>>> mistaken.
>> 
>> 
>> 
>> ___
>> polyml mailing list
>> polyml@inf.ed.ac.uk 
>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml 
>> 

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Poly/ML with libgmp on x86_64-darwin

[Bernard Berthomieu]

Does the polyml version built on your MacBook run on your other mac ?

  Bernard.


On 12/02/2018 12:45, Lawrence Paulson wrote:
I'm not able to build poly/ML on my Mac, with or without libgmp, for 
about a year. The funny thing is, it builds fine on my 
similarly-configured MacBook Pro at home. I've given up trying to 
figure out why.  Upgrading to High Sierra or downloading more recent 
versions of the sources hasn't changed this. Something in the setup 
must be very fragile.


ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see 
invocation)

make[1]: *** [polyimport] Error 1
make: *** [install-recursive] Error 1

I use Homebrew, not macports.

Larry

On 10 Feb 2018, at 07:12, Matthew Fernandez 
> wrote:


Makarius, were you saying that building Poly/ML with libgmp *at all* 
has been a challenge? Or specifically building a portable Poly/ML 
with libgmp? I have never had a problem building Poly/ML on macOS 
using a MacPorts-installed libgmp:


   CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I 
/opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" 
./configure

   make

I don’t know what the scenario is for Homebrew users, but I imagine 
it would be similar. For a long time I didn’t pay much attention to 
macOS questions, not having a Mac myself and after ending up with one 
I just assumed the cryptic flags juggling was common knowledge. 
Apologies if I was mistaken.




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Poly/ML with libgmp on x86_64-darwin

[Lawrence Paulson]

I'm not able to build poly/ML on my Mac, with or without libgmp, for about a 
year. The funny thing is, it builds fine on my similarly-configured MacBook Pro 
at home. I've given up trying to figure out why.  Upgrading to High Sierra or 
downloading more recent versions of the sources hasn't changed this. Something 
in the setup must be very fragile.

ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[1]: *** [polyimport] Error 1
make: *** [install-recursive] Error 1

I use Homebrew, not macports.

Larry

> On 10 Feb 2018, at 07:12, Matthew Fernandez  
> wrote:
> 
> Makarius, were you saying that building Poly/ML with libgmp *at all* has been 
> a challenge? Or specifically building a portable Poly/ML with libgmp? I have 
> never had a problem building Poly/ML on macOS using a MacPorts-installed 
> libgmp:
> 
>CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I 
> /opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure
>make
> 
> I don’t know what the scenario is for Homebrew users, but I imagine it would 
> be similar. For a long time I didn’t pay much attention to macOS questions, 
> not having a Mac myself and after ending up with one I just assumed the 
> cryptic flags juggling was common knowledge. Apologies if I was mistaken.

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Poly/ML with libgmp on x86_64-darwin

[Makarius]

On 10/02/18 07:33, Bernard Berthomieu wrote:
> 
> I could build libgmp 6.1.2 for i386 on macOS Sierra by first setting
> the shell variable ABI to 32, then proceed as usual (configure, make, ..):

Great, that was the key hint. I have now managed to build libgmp for
x86-darwin as follows:

env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname
-r)" --libdir=/usr/local/lib32


For the Poly/ML build I merely include -L/usr/local/lib32 in LDFLAGS;
the header files are implicitly taken from /usr/local/include (i.e. from
the default installation location of libgmp for x86_64-darwin).

See also the full story in
http://isabelle.in.tum.de/repos/isabelle/file/4fb9cbe10f3e/Admin/polyml/README#l26


Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Poly/ML with libgmp on x86_64-darwin

[Matthew Fernandez]

Makarius, were you saying that building Poly/ML with libgmp *at all* has been a 
challenge? Or specifically building a portable Poly/ML with libgmp? I have 
never had a problem building Poly/ML on macOS using a MacPorts-installed libgmp:

CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I 
/opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure
make

I don’t know what the scenario is for Homebrew users, but I imagine it would be 
similar. For a long time I didn’t pay much attention to macOS questions, not 
having a Mac myself and after ending up with one I just assumed the cryptic 
flags juggling was common knowledge. Apologies if I was mistaken.

The above steps are probably not suitable for building a portable Poly/ML. If 
you’re building libgmp from source maybe you want to try building a static 
library (-disable-shared to the libgmp build system)? I have not tried this, 
but they claim it works [0].

  [0]: https://gmplib.org/manual/Known-Build-Problems.html#index-MacOS-X

> On Feb 9, 2018, at 14:06, Makarius  wrote:
> 
> Dear Poly/ML enthusiasts and experts of the gcc toolchain on macOS,
> 
> building Poly/ML with libgmp has always been a challenge, but I have now
> managed as follows for x86_64-darwin.
> 
> The approach works as follows:
> 
>  (1) Build libgmp from sources.
>  (2) Build Poly/ML --with-gmp using that homemade version.
>  (3) Copy libgmp.10.dylib into the Poly/ML lib directory and adjust
> locations with install_name_tool
> 
> Afterwards it is possible to copy the resulting Poly/ML target directory
> to a different location on a different machine, with a different (newer)
> macOS version.
> 
> The details are in the included build.txt (e.g. for macOS 10.12 Sierra).
> This is not a shell script! It should be run carefully line-by-line.
> Towards the end there are two install_name_tool invocations with
> locations determined beforehand by "otool -L". The final "otool -L" is
> just a sanity check, the result is like this:
> 
> target/bin/poly:
>   @executable_path/../lib/libpolyml.9.dylib (compatibility version
> 10.0.0, current version 10.0.0)
>   @executable_path/../lib/libgmp.10.dylib (compatibility version 14.0.0,
> current version 14.2.0)
>   /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version
> 307.4.0)
>   /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current
> version 1238.0.0)
> 
> 
> This setup is already part of "isabelle build_polyml", see
> http://isabelle.in.tum.de/repos/isabelle/file/8b19a8a7f029/src/Pure/Admin/build_polyml.scala
> -- but that assumes that libgmp has been installed in a standard place
> (e.g. /usr/local/lib).
> 
> 
> I wonder if anybody has managed to build libgmp for x86-darwin (32bit)
> platform. That platform variant still provides better performance for
> big applications like Isabelle, because it requires only half the memory.
> 
> 
>   Makarius
> ___
> polyml mailing list
> polyml@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Poly/ML with libgmp on x86_64-darwin

[Bernard Berthomieu]

Hi Makarius,

I could build libgmp 6.1.2 for i386 on macOS Sierra by first setting
the shell variable ABI to 32, then proceed as usual (configure, make, ..):

    file build/intel-pc/lib/libgmp.10.dylib
    build/intel-pc/lib/libgmp.10.dylib: Mach-O dynamically linked 
shared library i386


  Bernard.

On 09/02/2018 23:06, Makarius wrote:

I wonder if anybody has managed to build libgmp for x86-darwin (32bit)
platform. That platform variant still provides better performance for
big applications like Isabelle, because it requires only half the memory.


Makarius


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[polyml] Poly/ML with libgmp on x86_64-darwin

[Makarius]

Dear Poly/ML enthusiasts and experts of the gcc toolchain on macOS,

building Poly/ML with libgmp has always been a challenge, but I have now
managed as follows for x86_64-darwin.

The approach works as follows:

  (1) Build libgmp from sources.
  (2) Build Poly/ML --with-gmp using that homemade version.
  (3) Copy libgmp.10.dylib into the Poly/ML lib directory and adjust
locations with install_name_tool

Afterwards it is possible to copy the resulting Poly/ML target directory
to a different location on a different machine, with a different (newer)
macOS version.

The details are in the included build.txt (e.g. for macOS 10.12 Sierra).
This is not a shell script! It should be run carefully line-by-line.
Towards the end there are two install_name_tool invocations with
locations determined beforehand by "otool -L". The final "otool -L" is
just a sanity check, the result is like this:

target/bin/poly:
@executable_path/../lib/libpolyml.9.dylib (compatibility version
10.0.0, current version 10.0.0)
@executable_path/../lib/libgmp.10.dylib (compatibility version 14.0.0,
current version 14.2.0)
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version
307.4.0)
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current
version 1238.0.0)


This setup is already part of "isabelle build_polyml", see
http://isabelle.in.tum.de/repos/isabelle/file/8b19a8a7f029/src/Pure/Admin/build_polyml.scala
-- but that assumes that libgmp has been installed in a standard place
(e.g. /usr/local/lib).


I wonder if anybody has managed to build libgmp for x86-darwin (32bit)
platform. That platform variant still provides better performance for
big applications like Isabelle, because it requires only half the memory.


Makarius
# build libgmp (see also 
https://github.com/Homebrew/homebrew-core/blob/master/Formula/gmp.rb)
curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
cd gmp-6.1.2
make distclean
./configure --prefix="$PWD/target" --enable-cxx 
--build=core2-apple-darwin"$(uname -r)"
make && make check && make install

# build polyml with this libgmp
cd ../polyml
make distclean
rm -rf target
./configure --prefix="$PWD/target" CFLAGS="-arch x86_64 -O3 -I../libffi/include 
-I$PWD/../gmp-6.1.2/target/include" CXXFLAGS="-arch x86_64 -O3 
-I../libffi/include -I$PWD/../gmp-6.1.2/target/include" CCASFLAGS="-arch 
x86_64" LDFLAGS="-segprot POLY rwx rwx -L$PWD/../gmp-6.1.2/target/lib" 
--with-gmp
make compiler && make compiler && make install

# adjust runtime library path
cp ../gmp-6.1.2/target/lib/libgmp.10.dylib target/lib
otool -L target/bin/poly
install_name_tool -change 
/Users/wenzelm/lib/polyml/gmp-6.1.2/target/lib/libgmp.10.dylib 
"@executable_path/../lib/libgmp.10.dylib" target/bin/poly
install_name_tool -change 
/Users/wenzelm/lib/polyml/polyml-git/target/lib/libpolyml.9.dylib 
"@executable_path/../lib/libpolyml.9.dylib" target/bin/poly
otool -L target/bin/poly
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml