Standalone binary

[wrwg]

Greetings Boogie team,

I wonder whether there is potentially some news on being able to create a standalone binary for Boogie. I looked at this a few years ago and even though .Net has a feature like this, did not get it to work.

A standalone binary which can be downloaded for Mac/Linux/Win would very much improve the user experience for the Move Prover, because we can then auto install all required tools without hassle and implement features like auto upgrade. Today users need to call a script which first installs .Net then boogie, and the process is hard to automate from within another executable.

Thanks, Wolfgang

[keyboardDrummer]

I think it has been possible for many years. You can find more information on the documentation page of dotnet build (https://learn.microsoft.com/en-us/dotnet/core/tools/dotnet-build), if you look at the option --self-contained. What problem did you run into last time you tried it?

Note that this removes the dependency on .NET, but not on an SMT solver being available. Boogie still depends on a solver being somewhere on the system, and packaging Z3 with the self-contained Boogie needs a solution by itself.

[junkil-park]

@keyboardDrummer, thanks for your response! Do you happen to know if Boogie also pre-builds and distributes dotnet-independent binaries, similar to how Z3 does it (https://github.com/Z3Prover/z3/releases)?

[shazqadeer]

I just tried the following based on the suggestion by @keyboardDrummer:

dotnet build Source/Boogie.sln --self-contained true -r osx-x64 -p:ImportByWildcardBeforeSolution=false -c release

It worked and the executable is generated here

/Users/shazqadeer/Source/boogie/Source/BoogieDriver/bin/Release/net6.0/osx-x64/BoogieDriver

If you drop the flag -c release the executable is generated in

/Users/shazqadeer/Source/boogie/Source/BoogieDriver/bin/Debug/net6.0/osx-x64/BoogieDriver

Possible values for the runtime id supplied via -r option can be found here.

[wrwg]

Thats great news @shazqadeer and @keyboardDrummer.

I wonder whether you'd consider putting the binary standalone releases on the release page of the repo, as @junkil-park mentioned above? I believe this could make usage of Boogie in end user applications smoother. We can also build those binaries ourselves and upload them to our repo, but there might be more folks which may benefit.

As a data point, in the entire Libra/Diem repo, and today's Aptos repo, really large repos which require a lot of extra installs, the only reason for the need to install .Net was always only Boogie. There is literally no .Net based tool we had ever use for.

[rahxephon89]

Hi @shazqadeer, when I tried the command, along with the binary, a set of libraries files are generated which the binary depends. Are they expected?

[shazqadeer]

Yeah, looks like it. I see that on my machine many libraries that were not being generated with the default build are now being generated. All of these libraries are in the folder:

/Users/shazqadeer/Source/boogie/Source/BoogieDriver/bin/Release/net6.0/osx-x64

So this must means that "self-contained" does not mean a single binary file. Instead, it means that all the library dependencies are provided into the build folder all of which must be copied to the target machine where Boogie needs to be executed.

Please try to copy the binary folder to a different clean machine from the one on which you did the build and see if you are able to run successfully.

[wrwg]

Perhaps this helps: https://learn.microsoft.com/en-us/dotnet/core/deploying/single-file/overview

…

On Sat, Sep 14, 2024 at 10:53 AM Shaz Qadeer ***@***.***> wrote: Yeah, looks like it. I see that on my machine many libraries that were not being generated with the default build are now being generated. All of these libraries are in the folder: /Users/shazqadeer/Source/boogie/Source/BoogieDriver/bin/Release/net6.0/osx-x64 So this must means that "self-contained" does not mean a single binary file. Instead, it means that all the library dependencies are provided into the build folder all of which must be copied to the target machine where Boogie needs to be executed. Please try to copy the binary folder to a different clean machine from the one on which you did the build and see if you are able to run successfully. — Reply to this email directly, view it on GitHub <#944 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AC2MSOWJXLJ6LOV64J2IEWTZWRZYZAVCNFSM6AAAAABN5V3OIWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNJRGA4DGNRWGA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[rahxephon89]

Hi @shazqadeer, When I tried using dotnet publish instead of dotnet build, I can also get a binary in the publish folder along with several pdb files. However, running ./BoogieDriver /help will lead the following errors:

Unhandled exception. System.ArgumentNullException: Value cannot be null. (Parameter 'path1')
   at System.IO.Path.Combine(String path1, String path2)
   at Microsoft.Boogie.ProverFactory.Load(String proverName) in /Users/tengzhang/boogie/Source/Provers/SMTLib/ProverUtil.cs:line 329
   at Microsoft.Boogie.CommandLineOptions.ApplyDefaultOptions() in /Users/tengzhang/boogie/Source/ExecutionEngine/CommandLineOptions.cs:line 1425
   at Microsoft.Boogie.CommandLineOptionEngine.Parse(String[] args) in /Users/tengzhang/boogie/Source/ExecutionEngine/CommandLineOptionEngine.cs:line 250
   at Microsoft.Boogie.OnlyBoogie.Main(String[] args) in /Users/tengzhang/boogie/Source/BoogieDriver/BoogieDriver.cs:line 22

There is no such error when I use the binary generated by the command dotnet build. Any idea why it is the case?

[keyboardDrummer]

Hi @shazqadeer, When I tried using dotnet publish instead of dotnet build, I can also get a binary in the publish folder along with several pdb files. However, running ./BoogieDriver /help will lead the following errors:

Unhandled exception. System.ArgumentNullException: Value cannot be null. (Parameter 'path1')
   at System.IO.Path.Combine(String path1, String path2)
   at Microsoft.Boogie.ProverFactory.Load(String proverName) in /Users/tengzhang/boogie/Source/Provers/SMTLib/ProverUtil.cs:line 329
   at Microsoft.Boogie.CommandLineOptions.ApplyDefaultOptions() in /Users/tengzhang/boogie/Source/ExecutionEngine/CommandLineOptions.cs:line 1425
   at Microsoft.Boogie.CommandLineOptionEngine.Parse(String[] args) in /Users/tengzhang/boogie/Source/ExecutionEngine/CommandLineOptionEngine.cs:line 250
   at Microsoft.Boogie.OnlyBoogie.Main(String[] args) in /Users/tengzhang/boogie/Source/BoogieDriver/BoogieDriver.cs:line 22

There is no such error when I use the binary generated by the command dotnet build. Any idea why it is the case?

Looking at the source based on your stracktrace:

        string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(
          cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
        path = System.IO.Path.Combine(codebase, "Boogie.Provers." + proverName + ".dll");

it seems System.Reflection.Assembly.GetExecutingAssembly().Location returned null or a path that looks like a root, leading to GetDirectoryName returning null and codebase being null, which causes an exception in Path.Combine.

Maybe Assembly.GetExecutingAssembly().Location returned a root looking path because of how it was packaged. The code would be more robust if it handled codebase == null elegantly by just skipping the Path.Combine call then.

[rahxephon89]

Thanks @keyboardDrummer and @shazqadeer! It turns out that adding

<PropertyGroup>
    <PublishSingleFile>true</PublishSingleFile>
    <IncludeAllContentForSelfExtract>true</IncludeAllContentForSelfExtract>
</PropertyGroup>

to BoogieDriver.csproj and then execute dotnet publish will resolve the issue!

[shazqadeer]

Great! You are welcome to put up a PR for this change.

[rahxephon89]

@shazqadeer @keyboardDrummer, the PR is up for review: #953