Installing on Apple Silicon

[ReubenJ]

I'm having some issues attempting to build/run the project on a MacBook Pro with an M2 Pro chip. I'm trying on the Linux branch.

Building with the current instructions in the Linux branch emits some warnings regarding the platform as the instructions ask you to specify x64 explicitly.

What I've Tried

• Updated the projects to use net8.0 instead of the unsupported netcoreapp3.1 version they are currently using (updates pushed to the Linux branch on my fork)
  - Result: the project builds successfully, but upon running the example command listed in the README.md, it appears there is something wrong with the Z3 install as running the BMA tool results in the following error:

Unhandled exception. System.IO.FileNotFoundException: Could not load file or assembly 'Microsoft.Z3, Version=4.12.2.0, Culture=neutral, PublicKeyToken=9c8d792caae602a2'. The system cannot find the file specified.

File name: 'Microsoft.Z3, Version=4.12.2.0, Culture=neutral, PublicKeyToken=9c8d792caae602a2'
[1]    97180 abort      DOTNET_ROOT=/nix/store/9zqlmf2ja3rf72cmkba08x82cyf9hk9l-dotnet-sdk-8.0.201
(devbox)

The only other relevant issue I could come up with was this one from the Z3 repo leading me to think it might be a Z3 issue and not BMA.

Has anyone had any luck with this on MacOS/arm64?

[hallba]

I’ve not tried installing on apple silicon and unfortunately I don’t have a machine to test. However some thoughts on your issue

• the error looks like the libraries haven’t been found and loaded successfully. How have you installed the Z3 packages, and do all of the links still work. I believe there are arm binaries for z3, and I’ve used Mac binaries on apple intel before
• I have compiled the console tool on Intel Mac before (prior to the Linux release, using the main branch). I used visual studio community for Mac and wrote a short shell script to download the dependencies. You could try run the unixprepare script and open in visual studio to see if it will compile

[ReubenJ]

Thank you for your tips!

How have you installed the Z3 packages, and do all of the links still work.

I was installing the Z3 package with paket, and it seemed to work without any complaints as far as I could see. You're right, there are definitely arm binaries for Z3—I've used them outside of the dotnet context without issue.

You could try run the unixprepare script and open in visual studio to see if it will compile

I'll give this a try too. I was trying with VS Code as well since VS for Mac is being discontinued, but I'll try anyways. Maybe there are some dependencies or settings that I'm missing when compiling/running directly from the terminal.

[shorthouse-lab]

Hi there - I am also trying to install BMA on an apple silicon Mac (M3), with difficulty. I have been able to run msbuild using the adaptations made by @ReubenJ - but generated executables are all .dll files that do not execute (they are .dll files).

I am used to compiling things for linux so have no idea really how to solve these issues.

If you manage to get it working I would very much appreciate you sharing how!

[ReubenJ]

Good to know that others are running into the same issues. I'll certainly update here when I have something, @shorthouse-lab.

[hallba]

For another project I revisited the linux compile which I've successfully completed, though the instructions on the wiki would benefit from updating. I did note though that I was able to use the -roll-forward Major option for the app to get the tool to use the version of the framework I had installed on ubuntu- @ReubenJ did you try this? I'm going to try install on apple intel soon with my updated protocol

[hallba]

Just adding to my comments above, I've installed the bma linux console tool successfully on apple intel, with.a different protocol from the above. I'm using an older dotnet and framework but it does appear to work; if I can find a machine I'll try the same on apple silicon.

The updated linux install protocol is (roughly)

• install the latest dotnet (on ubuntu I use apt)
• install paket on dotnet dotnet tool install --global Paket
• install dependencies paket install
• go to bmalinux directory cd BmaLinux
• restore some packages dotnet restore
• build dotnet msbuild BioCheckConsoleMulti.sln /p:Configuration=Release /p:Platform="x64" /t:Rebuild

Finally, on ubuntu because I was using a later framework, I run the tool with the roll-forward command line option i.e.

./BioCheckConsoleMulti --roll-forward Major -model some.json -engine SCM

[shorthouse-lab]

Thanks for this - unfortunately this isn't working on an M3 Mac running macOS. Msbuild appears to work but running the ./BioCheckConsoleMulti command returns:

davidshorthouse@Davids-MacBook-Pro netcoreapp3.1 % ./BioCheckConsoleMulti --roll-forward Major -model ../../../ToyModelStable.json -engine SCM
Failed to load A, error: dlopen(/Users/davidshorthouse/dotnet/host/fxr/8.0.4/libhostfxr.dylib, 0x0001): tried: '/usr/local/gromacs/lib/libhostfxr.dylib' (no such file), '/Users/davidshorthouse/dotnet/host/fxr/8.0.4/libhostfxr.dylib' (mach-o file, but is an incompatible architecture (have 'arm64', need 'x86_64')), '/System/Volumes/Preboot/Cryptexes/OS/Users/davidshorthouse/dotnet/host/fxr/8.0.4/libhostfxr.dylib' (no such file), '/Users/davidshorthouse/dotnet/host/fxr/8.0.4/libhostfxr.dylib' (mach-o file, but is an incompatible architecture (have 'arm64', need 'x86_64'))
The library libhostfxr.dylib was found, but loading it from /Users/davidshorthouse/dotnet/host/fxr/8.0.4/libhostfxr.dylib failed
  - Installing .NET Core prerequisites might help resolve this problem.
     https://go.microsoft.com/fwlink/?linkid=2063366

I've tried installing Paket using arm64 using:

dotnet tool install --global Paket --arch arm64

It seems it is looking for the wrong version of libhostfxr.dylib despite the x64 flag in the msbuild command. I've also run msbuild with "Any CPU" with no difference.

[shorthouse-lab]

I can update to say that this is now working on an M3 MacBook Pro running an Ubuntu virtual machine through UTM. I am using Ubuntu 22.04.4 (Jammy Jellyfish). I installed dotnet:

sudo apt-get install dotnet-sdk-8.0

Then followed the instructions given by @hallba above.

[ReubenJ]

An update on this: a non-virtual machine solution may be possible soon for M-series Macs. Z3Prover/z3#7846 added support for ARM Macs in the Dotnet bindings for Z3. The fact that the bindings were only compatible with Intel Macs was actually the root cause of the error I reported in this issue.

The bindings are available in the nightly build as mentioned in Z3Prover/z3#7843. I believe that BMA can run natively on M-series Macs with this nightly version of Z3, but I haven't managed to get it working as I'm not familiar enough with Dotnet/Nuget packaging tools and infra. Maybe someone with more familiarity could try it out and confirm?

[hallba]

Thank you for following up- this makes sense. I still don't have access to an M-series Mac but I have compiled Z3 in the past; let me see if I can borrow something and I'll try follow up when I can get hold of a relevant machine.

[ReubenJ]

A heads up if you try: I think the necessary .dylib for M-series Macs was missing from the .nupkg published on the nightly Github release (linked in the issue I mentioned above Z3Prover/z3#7843 (comment)). Not sure if this has been remedied yet or not.

I was able to build Z3 with the Dotnet bindings before, and the .nupkg included the .dylib file that was missing on the nightly version, so if you build it yourself, I think everything should work.