gnatprove alt-ergo fails on macOS

[rod-chapman]

On macOS Ventura...

If I install gnatprove with "alr get gnatprove", then set PATH so I can run "gnatprove" directly from a Shell, I find that alt-ergo does not run owing to not being able to find libgmp.10.dylib

e.g.

gnatprove --version

0.0w
Why3 for gnatprove version 1.4.0+git
/Users/rodchap/gnatprove_12.1.1_eaf96349/libexec/spark/bin/alt-ergo: dyld[51421]: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: <9B1A84BD-548D-3389-B023-87417162EFAB> /Users/rodchap/gnatprove_12.1.1_eaf96349/libexec/spark/bin/alt-ergo
  Reason: tried: '/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/libgmp.10.dylib' (no such file)

I find I have to set the environment variable DYLD_FALLBACK_LIBRARY_PATH=gnatprove_xxx/libexec/spark/lib before this works properly.

It's very easy to miss this, since gnatprove still still seems to run OK and produces sub-standard proof results. This is very confusing for new users.

[Fabien-Chouteau]

Hi @rod-chapman, can you try again with GNATprove FSF 13 that we released a few days ago?

[rod-chapman]

No joy... I get

rodchap@f4d4889dcf6d ~ % which gnatprove 
/Users/rodchap/gnatprove_13.2.1_d088f8a1/bin/gnatprove
rodchap@f4d4889dcf6d ~ % gnatprove --version
0.0w
Why3 for gnatprove version 1.5.0+git
/Users/rodchap/gnatprove_13.2.1_d088f8a1/libexec/spark/bin/alt-ergo: dyld[68152]: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: <E50A49E2-D55B-3EB0-B620-F173488466DA> /Users/rodchap/gnatprove_13.2.1_d088f8a1/libexec/spark/bin/alt-ergo
  Reason: tried: '/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/usr/local/lib/libgmp.10.dylib' (no such file), '/usr/lib/libgmp.10.dylib' (no such file, not in dyld cache)
/Users/rodchap/gnatprove_13.2.1_d088f8a1/libexec/spark/bin/cvc5: This is cvc5 version 1.0.5 [git tag 1.0.5 branch HEAD]
compiled with GCC version Apple LLVM 13.0.0 (clang-1300.0.29.30)
on Mar 13 2023 16:20:16

[rod-chapman]

I also made sure that DYLD_FALLBACK_LIBRARY_PATH was undefined before I did that.

Oh... this is running Intel binaries on an Apple Silicon (ARM) MacBook Pro running macOS Ventura 13.5.2

[simonjwright]

I’ve only just had to resolve a similar problem myself. macOS dylibs are great until they behave like this. Fix by

$ cd gnatprove_xxx/libexec/spark/bin
$ install_name_tool -change \
    /usr/local/opt/gmp/lib/libgmp.10.dylib \
    @rpath/libgmp.10.dylib \
    alt-ergo
$  install_name_tool -add_rpath @executable_path/../lib alt-ergo

The first command changes the search path for libgmp.10.dylib from the useless /usr/local/opt/gmp/lib to the run path (rpath), which would normally have been baked into the executable at build time by use of the appropriate -rpath switch.

The second command adds to the run path: @executable_path is the path from which alt-ergo was loaded, from which ../lib finds libgmp.10.dylib.

You may want to make a copy of alt-ergo to experiment on.