Merge pull request #131 from bkragl/build

Switch to .NET Core only and use Boogie NuGet package

.travis.yml

@@ -6,7 +6,7 @@ git:
   depth: false
 env:
   global:
-    - SOLUTION=cba-NetCore.sln
+    - SOLUTION=source/Corral.sln
     - Z3URL=https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip
     # Workaround for GitVersionTask bug in combination with .NET Core SDK 3.1.200
     # (see, e.g., https://github.com/dotnet/sdk/issues/10878 and https://github.com/GitTools/GitVersion/issues/2063)
@@ -22,11 +22,6 @@ install:
   - export PATH="$(find $PWD/z3* -name bin -type d):$PATH"
 
 script:
-  - git submodule update --init
-
-  # Attach HEADs in submodules to appease GitVersion
-  - git submodule foreach 'git branch -d master && git checkout -b master'
-
   # Build one configuration
   - dotnet build -c ${CONFIGURATION} ${SOLUTION}
 
@@ -37,7 +32,7 @@ deploy:
 
   # Publish dotnet global tool on nuget.org
   - provider: script
-    script: dotnet nuget push bin/${CONFIGURATION}/Corral*.nupkg -k ${NUGET_API_KEY} -s https://api.nuget.org/v3/index.json
+    script: dotnet nuget push source/Corral/bin/${CONFIGURATION}/Corral*.nupkg -k ${NUGET_API_KEY} -s https://api.nuget.org/v3/index.json
     skip_cleanup: true
     on:
       all_branches: true
@@ -49,7 +44,7 @@ deploy:
     token:
       secure: QDinEx1hu7AkjXNnut767Q6g9us91dVQAzxBoI5o+VGfvsLDV/G0VcVXTSWw1oLskxfEdnDuALFORwAvZxAVvRpQVTF1p/fVwsz1WgdjdfV0sm+0KlhTWekIBBMoZ7l7u3bjCFUYw6/7qqD732bUG24iSz7YG2WB6qB1AgS1RhyK9PaHLSfi5jtAAB179Pt00TcXhdT3Vr2v3f6CcSa3z2qOdtwUMLLz6ZSkobnWXE7DIDNXnntCQDCVFTF2JiCGfZpscKw70ufa4Vqr5pd4XJ+LDQGmB+y7ZAG9EIMcG0/c8/c8xac6K6URWmrDUSmTSFEhryM7wqzCpWDtzN9oJic86Lwv5TTHypfIdcM3LpoUoV02mmomyCJ4gL429Ts0FSC9rvIxxYqbIpDihE3yCJwtp5URZ0ZqRdMvc+GtWUqEPuJIkAvw2zP36+BAM3WS4z1ZytuB9RE01g27hg3yyjEBzJc/jkb4V1JW1UZyllCDp/IKv2tcKKv3nx/nuf72MJsixTTS1BgJitVgcO0dT37kP6xQFg2uTvzWUZUssb6PslDAyjaaQr9Fgyh+f87O5p73iMCUe9hivFsYI+ppgmRkx7Bp0aUKK8lBNsvRxPXNodAK1G6PDflmFXRonoRPueG2QHY5xX2zefdXmy2KXp/f2Xsi/Muwy3/h3iDaBHk=
     file_glob: true
-    file: bin/${CONFIGURATION}/Corral*.nupkg
+    file: source/Corral/bin/${CONFIGURATION}/Corral*.nupkg
     skip_cleanup: true
     on:
       all_branches: true

README.md

@@ -5,78 +5,76 @@
 [![Travis build status][travis-badge]][travis]
 
 
-Corral is a solver for the reachability modulo theories problem. Learn more here: http://research.microsoft.com/en-us/projects/verifierq
+Corral is a solver for the reachability modulo theories problem. Learn more
+here: http://research.microsoft.com/en-us/projects/verifierq
 
-## Dependency on Boogie
+## Building and Running Corral
 
-Corral has a dependency on [Boogie](https://github.com/boogie-org/boogie), which is provided as a git submodule. To download the specific revision of Boogie that Corral depends on:
-
-```
-cd ${CORRAL_DIR}
-git submodule init
-git submodule update
-```
-
-## Building and running Corral on Windows
-
-Here is how you set up Corral.
-
-1. Build `cba.sln`. This solution includes the necessary Boogie projects; there is no longer a separate step to build Boogie.
-2. Running Corral requires z3. We have tested Corral against z3 version 4.1; download and copy z3.exe in `bin\debug` folder, alongside the `corral.exe` executable.
-3. Corral takes a Boogie program as input. There are regressions provided in `test\regressions` folder. Go to this folder and run `perl check.pl` to run all the regressions. You can run an individual test, for instance, as follows: go to `test\regressions` and do: `..\..\bin\debug\corral.exe 001\001.bpl /flags:001\config`. The flag `/flags:filename` instructs corral to read its flags from the file `filename`.
-
-## Building and Running Corral on Linux using Mono
-
-The following worked for Matt McCutchen on Fedora 23. You may need to change the `TargetFrameworkVersion` to match what your Mono version provides.
-```
-cd ${CORRAL_DIR}
-xbuild /p:TargetFrameworkVersion=v4.5 /p:Configuration=Debug cba.sln
-ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe
-mono bin/Debug/corral.exe ...
-```
-
-## Building and Running Corral using .NET Core
-
-Currently there are separate project and solution files (`*-NetCore.*`) to build Corral with .NET Core, which use GitVersion to attach version numbers to the assemblies and package(s) generated by builds.
+Corral is built using [.NET Core](https://dotnet.microsoft.com) and use
+GitVersion to attach version numbers to the assemblies and package(s) generated
+by builds.
 
 ```console
-# Attach HEADs in submodules to appease GitVersion
-$ git submodule foreach 'git branch -D master && git checkout -b master'
-
 # Build the solution
-$ dotnet build cba-NetCore.sln
+$ dotnet build source/Corral.sln
 
 # Run the generated executable
-$ bin/Debug/netcoreapp3.1/corral ...
+$ source/Corral/bin/Debug/netcoreapp3.1/corral ...
 ```
 
 > :warning: There is currently a know build problem with .NET Core and
 > GitVersionTask. The workaround is to set the environment variable
 > `MSBUILDSINGLELOADCONTEXT=1` and run `dotnet build-server shutdown`.
 
 Alternatively, Corral can be installed as a [.NET Core Global Tool](https://docs.microsoft.com/en-us/dotnet/core/tools/global-tools):
+
 ```console
 $ dotnet tool install --global Corral
 ```
 
+### SMT Solver
+
+Running Corral requires [Z3](https://github.com/Z3Prover/z3). We have tested
+Corral against Z3 version 4.8.8.
+
+### Regressions
+
+Corral takes a Boogie program as input. There are regressions provided in
+`test\regressions` folder. Go to this folder and run `perl check.pl` to run all
+the regressions. You can run an individual test, for instance, as follows: go to
+`test\regressions` and do: `${CORRAL_EXE} 001\001.bpl
+/flags:001\config`. The flag `/flags:filename` instructs corral to read its
+flags from the file `filename`.
+
 ## Versioning and Release Automation
 
-The [main.yml](https://github.com/boogie-org/corral/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` anywhere in
+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/Corral/).
+* 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-badge]: https://img.shields.io/github/license/boogie-org/corral?color=blue
 [nuget]:         https://www.nuget.org/packages/Corral
 [nuget-badge]:   https://img.shields.io/nuget/v/Corral
 [travis]:        https://travis-ci.com/boogie-org/corral
 [travis-badge]:  https://travis-ci.com/boogie-org/corral.svg?branch=master
-