Update release process to include building a Dafny that's usable on M* Macs.

[keyboardDrummer]

Many Dafny users have trouble installing Dafny on their Mac:

• Trouble installing through VScode on macOS #2869
• 2.8.4. still fails to install dafny backend on macos  ide-vscode#283
• auto-install Dafny for Visual Studio Code 2.7.0 on M1 mac crashes wanting arm64e binaries rather than intel ide-vscode#246

Instead of making it easier for these users to build Dafny from source on their M* Mac, which so far has been an error prone process, we should ensure new versions of Dafny include a M* Mac build.

Implementation A

Use dotnet cross-compilation to let our GitHub actions MacOS machine build for both x64 and arm64. This can be done using the --arch option of dotnet: https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-build#options

Implementation B

Build a platform independent Dafny, which requires dotnet to be installed on the machine, and which does not include a Z3 binary. The Dafny VSCode extension will have to be updated so that it installs dotnet and downloads Z3.

Implementation C

Build a platform independent Dafny, which requires dotnet to be installed on the machine, and which includes the MacOS M* Z3 binary. The Dafny VSCode extension will have to be updated so that it installs dotnet.

[MikaelMayer]

I would prefer an alternative that does not depend on AWS if possible? But I am not knowledgeable enough.

[keyboardDrummer]

I would prefer an alternative that does not depend on AWS if possible? But I am not knowledgeable enough.

I think there could be several options available at the same time, AWS being just one of them. For AWS, I think the step of how to get an AWS account might be left out of the release manual since this GitHub organisation doesn't have any AWS budget. It'll be up to individual contributors to for example use the AWS free tier or other resources to use AWS, or use an alternative to AWS such as a personal M1 mac.

[cpitclaudel]

Option B sounds like a strict improvement over what we have now, right? (Since we require dotnet to build Dafny today on M*s.)

That said, I didn't follow the M* issues very closely, but is there a dotnet bug that prevents us from cross-compiling for that platform?

[keyboardDrummer]

That said, I didn't follow the M* issues very closely, but is there a dotnet bug that prevents us from cross-compiling for that platform?

Just tried it and it seems to work, at least for building for arm64 on my x64 laptop, although I only tested the building not running it on an M*.

This seems like the best approach then.

[MikaelMayer]

Related PR that should make the vscode extension installation process more reliable on M* Macs:
dafny-lang/ide-vscode#287