Skip to content

Commit

Permalink
Clean up readme (#212)
Browse files Browse the repository at this point in the history
* Clean up badges

* Update readme (documentation and getting help)
  • Loading branch information
bkragl authored Mar 3, 2020
1 parent 9ae2a77 commit 520eabc
Showing 1 changed file with 39 additions and 37 deletions.
76 changes: 39 additions & 37 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,17 +1,8 @@
# Boogie

## Build Status

| Linux | Windows |
|-------------------------------|---------------------------------|
| [![linux build status][1]][2] | [![windows_build_status][3]][4] |

[1]: https://travis-ci.com/boogie-org/boogie.svg?branch=master
[2]: https://travis-ci.com/boogie-org/boogie
[3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie
[4]: #FIXME

## About
[![License][license-badge]](LICENSE.txt)
[![NuGet package][nuget-badge]][nuget]
[![Travis build status][travis-badge]][travis]

Boogie is an intermediate verification language (IVL), intended as a layer on
which to build program verifiers for other languages. Several program verifiers
Expand All @@ -23,41 +14,32 @@ and the verifiers for [Dafny](https://github.com/dafny-lang/dafny),
[Spec#](https://www.microsoft.com/en-us/research/project/spec).
For a sample verifier for a toy language built on top of Boogie, see
[Forro](https://github.com/boogie-org/forro).
A previous version of the language was called BoogiePL. The current language
(version 2) is currently known as just Boogie, which is also the name of the
verification tool that takes Boogie programs as input.

Boogie is also the name of a tool. The tool accepts the Boogie language as
input, optionally infers some invariants in the given Boogie program, and then
generates verification conditions that are passed to an SMT solver. The default
SMT solver is [Z3](https://github.com/Z3Prover/z3).

The Boogie research project is being developed primarily in the [RiSE
group](http://research.microsoft.com/rise) at [Microsoft
Research](http://research.microsoft.com/) in Redmond. However, people at
several other institutions make the open-source Boogie tool what it is.

![boogie architecture](http://research.microsoft.com/en-us/projects/boogie/boogie.png)
## Documentation

More documentation can be found at http://boogie-docs.readthedocs.org/en/latest/ .
Here are some resources to learn more about Boogie. Be aware that some
information might be incomplete or outdated.

## Language Reference
* [Documentation](https://boogie-docs.readthedocs.org/en/latest/)
* [Language reference](https://boogie-docs.readthedocs.org/en/latest/LangRef.html).
* [This is Boogie 2](https://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf)
details many aspects of the Boogie IVL but is slightly out of date.

See [Language reference](http://boogie-docs.readthedocs.org/en/latest/LangRef.html).
## Getting help and contribute

Note: [This is Boogie2](http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf) details
many aspects of the Boogie IVL but is slightly out of date.
You can ask questions and report issues on our [issue tracker](https://github.com/boogie-org/boogie/issues).

## Getting help

We have a public [mailing list](https://mailman.ic.ac.uk/mailman/listinfo/boogie-dev) for users of Boogie.
You can also report issues on our [issue tracker](https://github.com/boogie-org/boogie/issues)
We are happy to receive contributions via [pull requests](https://github.com/boogie-org/boogie/pulls).

## Installation

Boogie releases are packaged as a .NET Core global tool available at
[nuget.org](https://www.nuget.org/packages/Boogie). To install Boogie simply
run:
[nuget.org][nuget]. To install Boogie simply run:

```
$ dotnet tool install --global boogie
Expand Down Expand Up @@ -156,19 +138,39 @@ See the [Unit test documentation](Source/UnitTests/README.md)

## Versioning and Release Automation

The https://github.com/boogie-org/boogie/blob/master/.github/workflows/main.yml workflow will create and push a new tag each time commits are pushed to the master branch (including PR merges). By default, the created tag increments the patch version number from the previous tag. For example, if the last tagged commit were `v2.4.3`, then pushing to master would tag the latest commit with `v2.4.4`. If incrementing minor or major number is desired instead of patch, simply add `#minor` or `#major` to the first line of the commit message. For instance:
The [Bump workflow](.github/workflows/main.yml) will create and push a new tag
each time commits are pushed to the master branch (including PR merges). By
default, the created tag increments the patch version number from the previous
tag. For example, if the last tagged commit were `v2.4.3`, then pushing to
master would tag the latest commit with `v2.4.4`. If incrementing minor or major
number is desired instead of patch, simply add `#minor` or `#major` to the first
line of the commit message. For instance:

> Adding the next greatest feature. #minor
If the last tagged commit were `v2.4.3`, then pushing this commit would generate the tag `v2.5.0`.
If the last tagged commit were `v2.4.3`, then pushing this commit would generate
the tag `v2.5.0`.

For pull-request merges, if minor or major version increments are desired, the first line of the merge commit message can be changed to include `#minor` or `#major`.
For pull-request merges, if minor or major version increments are desired, the
first line of the merge commit message can be changed to include `#minor` or
`#major`.

Note that on each push to `master`, the following will happen:
* A travis build for `master` is triggered.
* The GitHub workflow is also triggered.
* Once the workflow pushes a new tag `vX.Y.Z`, another travis build for `vX.Y.Z` is triggered.
* The travis build for `vX.Y.Z` in Release configuration publishes releases to GitHub and [NuGet.org](https://www.nuget.org/packages/Boogie/).
* Once the workflow pushes a new tag `vX.Y.Z`, another travis build for `vX.Y.Z`
is triggered.
* The travis build for `vX.Y.Z` in Release configuration publishes releases to
GitHub and [NuGet.org][nuget].

## License

Boogie is licensed under the MIT License (see [LICENSE.txt](LICENSE.txt)).

[license-badge]: https://img.shields.io/github/license/boogie-org/boogie?color=blue
[nuget]: https://www.nuget.org/packages/Boogie
[nuget-badge]: https://img.shields.io/nuget/v/Boogie
[travis]: https://travis-ci.com/boogie-org/boogie
[travis-badge]: https://travis-ci.com/boogie-org/boogie.svg?branch=master
[jenkins]: #FIXME
[jenkins-badge]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie

0 comments on commit 520eabc

Please sign in to comment.