goose

Goose is now located at https://github.com/goose-lang/goose. Primitives with trusted models and specs that are intended for verified code to use are now at https://github.com/goose-lang/primitive.

Bump dependencies

This release adds support for the async_disk FFI and uses the new ptrT type for opaque pointers.

This version includes improvements and bug fixes from @RalfJung, especially around control flow.

Many translations now include an extra unit value at the end like e; #(), hence the move from v0.3 to v0.4.

Goose is now module-aware

Implement module-aware loading using golang.org/x/tools/go/packages to load source code (issue #9), rather than using ParseFile directly. This feature was implemented with @upamanyus, who helped figure out how Goose used to work and implemented the initial version of this feature.

It is no longer necessary to use GO111MODULE=auto or download the translated package's dependencies to $GOPATH to make Goose work. Dependencies are fetched from the module cache as in a normal module build.

In addition, this design allowed us to add the following features

• It is no longer necessary to specify an FFI manually. The correct FFI
  will be determined by the presence of an import of the disk or dist_ffi
  packages; "none" is chosen if neither is imported.
• Multiple packages under a single directory can be translated
  simultaneously, automatically using their package paths to determine the
  output directory. Loading multiple packages simultaneously is much
  faster.
• (somewhat experimental) Translation works even on upstream
  dependencies not in the source tree, though they need to be in go.mod.
• Goose now translates with the build flag "goose" set. Files can be
  skipped in the translation by simply adding // +build !goose with an
  empty line after to the top of the file, addressing issue #10.
• The examples in the Goose repo automatically use the correct FFI based on
  imports, so we automatically have some tests using the generic FFI, addressing
  issue #19.
• The goose binary's command-line interface is now tested directly in
  CI using BATS, a bash testing framework.