Regular releases

[michael-emmi]

(Expanding on #149)

Now there is one tagged release (v2.4.1). But is there a policy and mechanism for future releases?

It would be great to have a plan for when to increment the version number and create a new release. Even better would be to have those steps automated, ideally with TravisCI or GitHub Actions.

Ultimately it would be ideal to have binary packages sent to NuGet.org automatically too, so that Boogie binaries could be installed like every other modern software package. Dotnet has made this pretty convenient with Global Tools.

By the way, I’ve created an example of this on NuGet. Happy to hand this package over to the appropriate owner(s) once we figure this out.

[michael-emmi]

@bkragl let’s get the conversation going

[shazqadeer]

@michael-emmi : It sounds like you are volunteering to be be release master for Boogie binaries. Do you think you could take charge of this responsibility?

[michael-emmi]

I am ok with being in charge, but wary of breaking previously-agreed upon conventions of which I am unaware!

Is there anybody else that should be part of this conversation? e.g., @RustanLeino @mike-barnett @delcypher ?

[mike-barnett]

Ha! No, there are no previously-agreed conventions. Please feel free to do what you wish with it!

[bkragl]

Setting up an automatic process that creates a release on GitHub and publishes a package on NuGet.org whenever a version tag is pushed sounds great. I can try to help setting it up.

Some (unordered) thoughts:

1) Git tags can have additional text, like a commit message. Perhaps we could put release notes there (and read them from there to attach to wherever a release is published).

2) Should there be releases in fixed periods, or should we have a place to discuss/request an upcoming release?

3) Z3 is platform dependent, so I guess we cannot really include it in a Boogie package. I would suggest that the code that looks for a Z3 binary is updated. IMO we should only look for z3 (or z3.exe) in the PATH, and not in the same directory as the Boogie binary (or similar).

4) Other tools like Dafny and Corral reference Boogie "as a library". @RustanLeino mentioned that there are plans to move Dafny also to .NET Core. I wonder if it is possible to have a single NuGet package that can be used both to install the command-line tool and to reference Boogie in other projects. Or is the preference that these other projects require and reference a copy of the Boogie source tree?

[michael-emmi]

Those are all great points.

Git tags can have additional text, like a commit message. Perhaps we could put release notes there (and read them from there to attach to wherever a release is published).

Do you have an example of a project using that?

Should there be releases in fixed periods, or should we have a place to discuss/request an upcoming release?

I would say that minor versions should probably be incremented every time something is merged into master, unless that thing should be a minor or major version instead.

IMO we should only look for z3 (or z3.exe) in the PATH, and not in the same directory as the Boogie binary (or similar).

Yes please!!

Or is the preference that these other projects require and reference a copy of the Boogie source tree?

I have no preference there.

I’ve also looked into easing version bumping using GitVersion with #174 for discussion. (So far this only affects the NetCore build.

[michael-emmi]

@bkragl @shazqadeer do you have accounts on nuget.org?

We will have to add a Boogie API key for NuGet to Travis CI for automated publishing.

To do that, I can make you co-owners of Boogie on nuget.org, or you can give me admin privileges to Boogie on travis-ci.org, or both.

[bkragl]

I'll create an account on nuget.org. However, I think I don't have admin privileges for Boogie on Travis CI myself.

Who is currently "owning" the Travis CI build?

[shazqadeer]

I have an account on nuget.

id: shaz_qadeer Affiliated with: shaz.qadeer@gmail.com

[michael-emmi]

Ok I’ve requested adding shaz_qadeer as a co-owner of Boogie on nuget.org.

Although, ideally a Boogie organization would own this. We would just need an organization email address… any ideas about what address we could use (and how to manage that email account)?

[shazqadeer]

@delcypher: Could you please give admin privileges to @michael-emmi for the travis build of boogie?

[delcypher]

@shazqadeer AFAIK permissions for TravisCI are tied to the permissions of the GitHub account. @michael-emmi needs to be added to the organization. I don't know which privilege level is needed.

Also please note that TravisCI are currently migrating projects from travis-ci.org to travis-ci.com and I've just done this for Boogie and Symboolix.

• https://travis-ci.com/boogie-org/boogie/settings
• https://travis-ci.com/boogie-org/symbooglix/settings

[delcypher]

Note you'll need to update the build badges of both repositories to point to a new URL.

[shazqadeer]

@delcypher : I have invited @michael-emmi to be an owner of the boogie organization. Hopefully, that gives him the requisite permissions.

[michael-emmi]

Thanks @delcypher I am now listed as a GitHub owner but @shazqadeer I’m still not able to get to the settings where I’d add the NuGet API key. Normally I am able to see a Settings choice under the More Options tab:

Do you see the Settings choice on your side?

[delcypher]

@michael-emmi I see "Settings" in the drop down. Are you looking at the new location (https://travis-ci.com/boogie-org/boogie/settings) ? You might also to go here and ask TravisCI to sync across your account details.

[michael-emmi]

Ahh now it has appeared — thanks!

[michael-emmi]

@bkragl Now I have added my nuget.org API key to Boogie’s travis environment, so publishing from travis should work — though we will probably want to wait on #174 first for versioning.

[michael-emmi]

So based on the what’s been happening in #166 I think the current plan goes like this:

1. Tag a commit with an incremented version number, e.g., v2.4.2.
2. Push the tags and merge the commit into master
3. Travis will publish a .NET Core package to nuget.org, and in a new GitHub release.
4. Anybody with dotnet installed can install the latest version with dotnet tool install -g boogie.

Also: looks like Mono builds are on the way out.

@zvonimir @bkragl please confirm the above.

[bkragl]

Hmm, I'm now a bit unsure about the procedure. I imagined that a release is created by tagging a commit with a version number and pushing the tag, but usually this commit would already be on the master branch. But then Travis would have already built and tested the commit. Does it then retrospectively trigger the deployment when it sees the tag?

Also something to clarify: What happens if a build fails? I would hope that in this case the default behavior is to not trigger the deployment.

[michael-emmi]

Does it then retrospectively trigger the deployment when it sees the tag?

Turns out that pushing a tag triggers a new build; so pushing a commit causes one build, and pushing a tag causes another. If you click on the Branches tab for a given project in Travis, each tag build will show up under Active Branches.

What happens if a build fails?

Failure is generally terminal, and deployment only happens when previous steps succeed.

[michael-emmi]

Does it then retrospectively trigger the deployment when it sees the tag?

Slight clarification (I’m learning just learning this now): it appears that pushing a tag is the same as pushing any other ref, e.g., a branch: the commits in their history are pushed as well. In other words, git tag v2 && git push --tags seems to have the same effect as git push if the current branch were named v2. (Of course if v2 were a branch, we would expect it could be pushed more than once.)

Just in case you were curious (as I was) about Travis/GitHub receiving a tag without an associated commit(s).

[bkragl]

This sounds good. So any (old) commit on the master branch could be tagged and pushing it will trigger a deployment.

Now there can be two kinds of build failures:

1. Spurious failures: I saw Travis builds spuriously failing for various reasons. For example, an error during setup (installation of packages), or a lit test randomly failing. In this case we would go to the Travis interface and restart the build.
2. Real failures:: For example, a syntax error, or truly breaking a regression test. In this case we would delete the tag, fix the error, and tag a new commit.

Is my understanding correct?

[michael-emmi]

In this case we would delete the tag, fix the error, and tag a new commit.

I’m not sure whether deleting a tag is generally a good idea (?) but even so, there are the following alternatives.

• wait to tag or push tag until verifying that that commit builds successfully (e.g., on the corresponding merge to master branch).
• just create a new tag (with incremented version number)

[bkragl]

I’m not sure whether deleting a tag is generally a good idea (?)

I guess there could be a conflict if somebody already pulled the tag before deletion, and then later pulls again receiving a tag with the same name pointing to a different commit.

but even so, there are the following alternatives.

* wait to tag or push tag until verifying that that commit builds successfully (e.g., on the corresponding merge to master branch).

Yes, absolutely. What I called "real failures" should never happen for a release tags. I'm mentioning it just in case we cannot refute Murphy's law.

[michael-emmi]

I guess everything is ready to give this a go. Shall we tag the last commit and see what happens?

[bkragl]

Yes, let's try 🤞

Maybe we can wait until tomorrow in case someone objects.

[michael-emmi]

@bkragl nice job — it worked!

Only a couple of small caveats.

1. The condition for deployment (configuration=Release) was ineffective, and so both builds tried to publish, with Debug winning in this case.
2. The generated release message should probably be customized; the auto-generated one currently says

   v2.4.2: Merge pull request #166 from boogie-org/netcore

[bkragl]

@bkragl nice job — it worked!

That's great!

1. The condition for deployment (configuration=Release) was ineffective, and so both builds tried to publish, with Debug winning in this case.

Hmm, I don't understand why this happened. ${CONFIGURATION} must have been defined in the deployment part, because otherwise the script would have failed. Here is the documentation. What I put is a valid bash condition, but could it be that Travis does not like the curly braces there or wants spaces before and after =?

2. The generated release message should probably be customized; the auto-generated one currently says

You can supply a message to a tag, similar to a commit. My suspicion is that this would then be used instead of the message of the commit that is tagged. Otherwise name and body could be set as described here. But then we would have to read this information from somewhere, for which the git tag seems like the most natural place.

[michael-emmi]

Figured it out: see 0414268 and d9dad75. The travis docs seem somewhat contradictory on this, but it works now.

[shazqadeer]

Great job, @michael-emmi and @bkragl . Has this issue been resolved now?

[michael-emmi]

Nearly!

Now releases to GitHub and NuGet are automated from the point where we tag a commit with vX.Y.Z.

But I’m still wondering about the mechanism and frequency with which we will tag. While we could continue to do this manually, it’s probably more reliable to have tags automatically created — particularly since management of this project is fairly loose without clear authority :-)

For instance, each time a pull request is merged into the master branch. (Supposing those automatic tags only bump the patch number, we could still add tags to bump the minor and major numbers.) I don’t imagine this being particularly hard to automate, especially given our integration with GitVersion.

What do others think about this? @bkragl @zvonimir @shazqadeer

[zvonimir]

If we are going to automate this, and especially if we'll push a new release with every pull request, then using semantic versioning does not really make sense. So I wonder if we should switch our versioning scheme to something else, such as http://calver.org/.

[michael-emmi]

@zvonimir why doesn’t it make sense to keep increasing patch number by default, allowing manual override when major/minor number should be incremented, according to semantic versioning?

[zvonimir]

There is a manual step then, which I thought we wanted to avoid. It is also not clear to me when we would increment major/minor numbers. To me it seems that all of the version updates will end up being more or less time/date-driven, and so I thought that something like calver (or some version of it) probably makes more sense. For example, our version numbers could be YY.MM format, and we automatically push out a release every month, or every few months (like every 6 months) if there were changes to the master branch.

[michael-emmi]

@zvonimir I guess we will need an extended discussion about this, but to quickly summarize my view:

• semantic versioning is fairly ubiquitous, and dictates that major version must increase on breaking (backward incompatible) changes, and minor version must increase on changes which introduce new features.
• the vast majority of changes would be patch-level changes, so that seems like a good default; when somebody adds a feature or breaking change, they (or somebody) should increment the major or minor version. Forgetting to do this just weakens adherence to strict semantic versioning, and might cause updates to break others’ builds when upgrading (since they’d assume any patch increment is safe).
• I don’t expect Boogie development to have any regularity, so timed releases is not obviously a good fit.
• I do expect users to be needing patches in a timely manner, so it would be good to be able to release as soon as a fix is merged.

[michael-emmi]

Also, I believe that if we neglected to ever increment major or minor numbers, the auto-increment-patch-number scheme would at the very least allow reactive releases.

If we do remember to increment major and minor numbers, then we get the bonus of a saner versioning model.

[zvonimir]

Ok, your last two points sold me on semantic versioning. So let's roll with that.

[michael-emmi]

Ok, so then what do you guys @zvonimir @bkragl think about #182?

[michael-emmi]

Note you'll need to update the build badges of both repositories to point to a new URL.

Done.

[michael-emmi]

I believe #182 finally solves this one.