GNAT-FSF-builds icon indicating copy to clipboard operation
GNAT-FSF-builds copied to clipboard

gnatprove alt-ergo fails on macOS

Open rod-chapman opened this issue 1 year ago • 4 comments

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.

rod-chapman avatar Oct 31 '23 11:10 rod-chapman