Cannot build Boogie

[RustanLeino]

I’ve been trying to upgrade Dafny to use the latest Boogie, starting from @keyboardDrummer 's dafny-lang/dafny#876. I’m getting absolutely nowhere, and at some point I realized I can’t even build the current version of Boogie (or any other recent .NET Core version of Boogie). The problem is the

/usr/local/share/dotnet/sdk/3.1.404/Sdks/NuGet.Build.Tasks.Pack/build/NuGet.Build.Tasks.Pack.targets(288,11): error MSB4057: The target "GetVersion" does not exist in the project. [/Users/leino/Source/boogie/Source/CodeContractsExtender/CodeContractsExtender.csproj]
/usr/local/share/dotnet/sdk/3.1.404/Sdks/NuGet.Build.Tasks.Pack/build/NuGet.Build.Tasks.Pack.targets(288,11): error MSB4057: The target "GetVersion" does not exist in the project. [/Users/leino/Source/boogie/Source/Model/Model.csproj]

issue that others have encountered. I have tried the workaround of setting MSBUILDSINGLELOADCONTEXT=1, running dotnet build-server shutdown, and then trying again, but this still does not work on my Mac. (Curiously, if I repeat the dotnet build Source/Boogie.sln command, I get the error above for either just CodeContractsExtender.csproj, or for CodeContractsExtender.csproj plus either Model.csproj or Graph.csproj.)

Has anyone out there successfully built Boogie on a Mac?

[bkragl]

Hi @RustanLeino, I actually started to work on porting Dafny to use the Boogie NuGet package here:
https://github.com/bkragl/dafny/tree/boogie-dependency

It all works well. I just need to do a few small updates in Boogie and then I should be able to put up a PR. There will be failing regression tests because of different models, error traces, etc. It would be great to get help from the Dafny community for fixing the .expect files.

Anyway, it would still be good to fix your compilation issues. I don't have a Mac myself, but there are a number of people that built Boogie on Mac. @shazqadeer @michael-emmi @cbarrettfb

[bkragl]

@RustanLeino, could you try removing all build artifacts by running git clean -dfx, and then build again from a clean state? There might be weirdness caused by combining build artifacts from before and after the workaround steps.

If this still does not work, I realized that you can set export BOOGIE_NO_GITVERSION=1. I added this feature at some point because I found that on my machine builds are faster without GitVersion. I keep this setting in my shell initialization file. Note that with this setting the generated binaries and packages will get a default version number (1.0.0), but this should be fine for local builds.

[RustanLeino]

@bkragl Woohoo! Your git clean -dfx suggestion worked. So, to build Boogie from the latest master, I did

git clean -dfx
MSBUILDSINGLELOADCONTEXT=1 dotnet build-server shutdown
MSBUILDSINGLELOADCONTEXT=1 dotnet build Source/Boogie.sln

Thanks!

[RustanLeino]

@bkragl Also, thanks for working on getting Dafny to use the NuGet Boogie. I'm happy to help with the test suite and .expect files. The easiest is probably if you email me and we go from there.

[keyboardDrummer]

Related PR: #319