Installing vgo¶
Obtaining vgo¶
The source code of vgo is available via mercurial. Provided that you have mercurial installed, you can obtain vgo by doing:
% hg clone https://bitbucket.org/teythoon/vgo
destination directory: vgo
requesting all changes
adding changesets
adding manifests
adding file changes
[...]
Compiling vgo¶
In order to compile vgo you need the golang tool chain. On Debian systems you can install it using aptitude install golang.
Go to your vgo checkout and do:
% make
GOPATH=[...] go install vgo
[...]
Running the test suite¶
To make sure that your build of vgo works as expected, you can optionally run the test suite:
% make test
[...]
170 / 170 tests successful.
Installing vgo¶
You can optionally install vgo to a location of your choice by running:
% make install PREFIX=/usr/local/stow/vgo
[...]
Using vgo¶
All of vgos functionality can be invoked using the vgo binary. Running it without arguments to get a list of available commands:
vgo is a frontend for the verifiable go toolchain.
Usage:
vgo [vgo options] command [command options] [command args]
The commands are:
install verifies and installs the given vgo package
inspect vgo reports interactively
runtests runs the vgo test suite
config prints the vgo configuration
version prints the vgo version
help prints usage and flags of a given command
Use "vgo help [command]" for more information about a command.
Additional help topics:
options global vgo options
Use "vgo help [topic]" for more information about that topic.
vgo needs its source code to translate model checking stubs in the verification step. It uses the environment variable VGOROOT to locate it. If VGOROOT is not set, it defaults to /usr/lib/vgo. As a convenience if you run vgo directly from the source tree it uses this location automatically.
If you have installed vgo to ${PREFIX}, you must set VGOROOT to ${PREFIX}/lib/vgo. Make sure that the vgo frontend vgo is in your ${PATH}. With bourne shell like shells this can be done using:
% export VGOROOT="${PREFIX}/lib/vgo"
% export PATH="${PREFIX}/bin:${PATH}"
% vgo runtests
[...]
170 / 170 tests successful.