Skip to content

Commit

Permalink
Update goose path to goose-lang
Browse files Browse the repository at this point in the history
  • Loading branch information
tchajed committed Jul 20, 2024
1 parent bcc3a4d commit 926bda7
Show file tree
Hide file tree
Showing 49 changed files with 134 additions and 354 deletions.
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# Goose: a subset of Go with a semantics in Coq

[![CI](https://github.com/tchajed/goose/workflows/CI/badge.svg)](https://github.com/tchajed/goose/actions/workflows/build.yml)
[![](https://godoc.org/github.com/tchajed/goose?status.svg)](https://godoc.org/github.com/tchajed/goose)
[![CI](https://github.com/goose-lang/goose/workflows/CI/badge.svg)](https://github.com/goose-lang/goose/actions/workflows/build.yml)
[![](https://godoc.org/github.com/goose-lang/goose?status.svg)](https://godoc.org/github.com/goose-lang/goose)

Goose is a subset of Go equipped with a semantics in Coq, as well as translator to automatically convert Go programs written in Go to a model in Coq. The model plugs into [Perennial](https://github.com/mit-pdos/perennial) for carrying out verification of concurrent storage systems.

Expand All @@ -26,7 +26,7 @@ import (

"github.com/tchajed/marshal"

"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)

type Log struct {
Expand Down Expand Up @@ -128,7 +128,7 @@ Directly modeling a low-level, imperative language (and especially writing in it

Goose requires Go 1.12+.

You can install goose with either `go get github.com/tchajed/goose/cmd/goose` or from a clone of this repo with `go install ./cmd/goose`. These install
You can install goose with either `go get github.com/goose-lang/goose/cmd/goose` or from a clone of this repo with `go install ./cmd/goose`. These install
the `goose` binary to `$GOPATH/bin` (or `~/go/bin` if you don't have GOPATH
set).

Expand Down
4 changes: 2 additions & 2 deletions cmd/goose/main.go
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ import (

"github.com/fatih/color"

"github.com/tchajed/goose"
"github.com/tchajed/goose/glang"
"github.com/goose-lang/goose"
"github.com/goose-lang/goose/glang"
)

// write data to file name, first checking if it already has those contents
Expand Down
4 changes: 2 additions & 2 deletions cmd/test_gen/main.go
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ From Perennial.goose_lang Require Import ffi.disk_prelude.
From Perennial.goose_lang.interpreter Require Import test_config.
(* test functions *)
From Goose.github_dot_com.tchajed.goose.internal.examples Require Import semantics.
From Goose.github_dot_com.goose_lang.goose.internal.examples Require Import semantics.
`

Expand All @@ -28,7 +28,7 @@ import (
"testing"
"github.com/stretchr/testify/suite"
"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)
type GoTestSuite struct {
Expand Down
2 changes: 1 addition & 1 deletion docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

[Motivation](motivation.md) documents why we use the approach of converting from Go at all in the context of our verification work.

[Implementation](implementation.md) walks through the design decisions in the Goose implementation. This includes details on the subset of Go supported, measure to make the translation more trustworthy, and goose works together with a Go support library (the `github.com/tchajed/goose/machine` and `github.com/tchjaed/goose/machine/filesys` packages) and the Perennial Goose support code in Coq.
[Implementation](implementation.md) walks through the design decisions in the Goose implementation. This includes details on the subset of Go supported, measure to make the translation more trustworthy, and goose works together with a Go support library (the `github.com/goose-lang/goose/machine` and `github.com/tchjaed/goose/machine/filesys` packages) and the Perennial Goose support code in Coq.

[Writing Goose](writing-goose.md) explains how to write code in Goose, the
subset of Go that the Goose translator and Goose model accept.
Expand Down
2 changes: 1 addition & 1 deletion docs/implementation.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,4 @@ A few Go features are implemented as libraries in GooseLang on top of simpler pr

## Go support library

Goose supplies `github.com/tchajed/goose/machine` for a handful of additional base operations (eg, for encoding integers as bytes), which have a corresponding semantics in GooseLang (via an implementation).
Goose supplies `github.com/goose-lang/goose/machine` for a handful of additional base operations (eg, for encoding integers as bytes), which have a corresponding semantics in GooseLang (via an implementation).
2 changes: 1 addition & 1 deletion examples_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ import (
"strings"
"testing"

"github.com/goose-lang/goose"
"github.com/stretchr/testify/assert"
"github.com/tchajed/goose"
)

var updateGold = flag.Bool("update-gold",
Expand Down
15 changes: 8 additions & 7 deletions go.mod
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
module github.com/tchajed/goose
module github.com/goose-lang/goose

go 1.22

require (
github.com/fatih/color v1.16.0
github.com/fatih/color v1.17.0
github.com/pkg/errors v0.9.1
github.com/stretchr/testify v1.7.0
github.com/stretchr/testify v1.9.0
github.com/tchajed/marshal v0.4.3
golang.org/x/sys v0.14.0
golang.org/x/tools v0.15.0
golang.org/x/sys v0.22.0
golang.org/x/tools v0.23.0
)

require (
Expand All @@ -17,6 +17,7 @@ require (
github.com/mattn/go-colorable v0.1.13 // indirect
github.com/mattn/go-isatty v0.0.20 // indirect
github.com/pmezard/go-difflib v1.0.0 // indirect
golang.org/x/mod v0.14.0 // indirect
gopkg.in/yaml.v3 v3.0.0-20200615113413-eeeca48fe776 // indirect
golang.org/x/mod v0.19.0 // indirect
golang.org/x/sync v0.7.0 // indirect
gopkg.in/yaml.v3 v3.0.1 // indirect
)
19 changes: 19 additions & 0 deletions go.sum
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,13 @@ github.com/fatih/color v1.9.0/go.mod h1:eQcE1qtQxscV5RaZvpXrrb8Drkc3/DdQ+uUYCNjL
github.com/fatih/color v1.13.0/go.mod h1:kLAiJbzzSOZDVNGyDpeOxJ47H46qBXwg5ILebYFFOfk=
github.com/fatih/color v1.16.0 h1:zmkK9Ngbjj+K0yRhTVONQh1p/HknKYSlNT+vZCzyokM=
github.com/fatih/color v1.16.0/go.mod h1:fL2Sau1YI5c0pdGEVCbKQbLXB6edEj1ZgiY4NijnWvE=
github.com/fatih/color v1.17.0 h1:GlRw1BRJxkpqUCBKzKOw098ed57fEsKeNjpTe3cSjK4=
github.com/fatih/color v1.17.0/go.mod h1:YZ7TlrGPkiz6ku9fK3TLD/pl3CpsiFyu8N92HLgmosI=
github.com/goose-lang/goose v0.0.0-20191114201541-ebbf1d75c8ca/go.mod h1:2c33VcNcIHG8vQhprFmBlZxpC62+TfmnGjB+jVaKhXo=
github.com/goose-lang/goose v0.0.0-20200128225509-92a5cfe01fc4/go.mod h1:rhep/Jc/mYPoMIYG8dPtnc71UHAPHNYRx1qvpB245Ss=
github.com/goose-lang/goose v0.2.0/go.mod h1:Y2zBxxd3wa0lrYRDyebxZgbgV4LLsPUtsBiLe1wnS9c=
github.com/goose-lang/goose v0.3.1/go.mod h1:s6D4ibH0SaPtDcp0krx05XkZLlqipgRyRH8X6JP+hcc=
github.com/goose-lang/goose v0.4.4/go.mod h1:w5NCIqICRsj0OJfTuft7HO2H51u629Qn0d+wxZsu6Eo=
github.com/goose-lang/std v0.0.0-20210910024443-21c4593d3dec/go.mod h1:eBTA88cbxhdegtDJayt+ns0Y9jjXsAwxv3CbH+62cKE=
github.com/goose-lang/std v0.0.0-20220414201102-c41554454045 h1:2djI+j4CTlxbg4FcWT2n4rvnBqccNVCOvLm6oaHaUDc=
github.com/goose-lang/std v0.0.0-20220414201102-c41554454045/go.mod h1:eBTA88cbxhdegtDJayt+ns0Y9jjXsAwxv3CbH+62cKE=
Expand Down Expand Up @@ -42,6 +49,8 @@ github.com/stretchr/testify v1.4.0/go.mod h1:j7eGeouHqKxXV5pUuKE4zz7dFj8WfuZ+81P
github.com/stretchr/testify v1.6.1/go.mod h1:6Fq8oRcR53rry900zMqJjRRixrwX3KX962/h/Wwjteg=
github.com/stretchr/testify v1.7.0 h1:nwc3DEeHmmLAfoZucVR881uASk0Mfjw8xYJ99tb5CcY=
github.com/stretchr/testify v1.7.0/go.mod h1:6Fq8oRcR53rry900zMqJjRRixrwX3KX962/h/Wwjteg=
github.com/stretchr/testify v1.9.0 h1:HtqpIVDClZ4nwg75+f6Lvsy/wHu+3BoSGCbBAcpTsTg=
github.com/stretchr/testify v1.9.0/go.mod h1:r2ic/lqez/lEtzL7wO/rwa5dbSLXVDPFyf8C91i36aY=
github.com/tchajed/goose v0.0.0-20191114201541-ebbf1d75c8ca/go.mod h1:2c33VcNcIHG8vQhprFmBlZxpC62+TfmnGjB+jVaKhXo=
github.com/tchajed/goose v0.0.0-20200128225509-92a5cfe01fc4/go.mod h1:rhep/Jc/mYPoMIYG8dPtnc71UHAPHNYRx1qvpB245Ss=
github.com/tchajed/goose v0.2.0/go.mod h1:Y2zBxxd3wa0lrYRDyebxZgbgV4LLsPUtsBiLe1wnS9c=
Expand All @@ -62,6 +71,8 @@ golang.org/x/mod v0.4.2/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
golang.org/x/mod v0.6.0-dev.0.20220106191415-9b9b3d81d5e3/go.mod h1:3p9vT2HGsQu2K1YbXdKPJLVgG5VJdoTa1poYQBtP1AY=
golang.org/x/mod v0.14.0 h1:dGoOF9QVLYng8IHTm7BAyWqCqSheQ5pYWGhzW00YJr0=
golang.org/x/mod v0.14.0/go.mod h1:hTbmBsO62+eylJbnUtE2MGJUyE7QWk4xUqPFrRgJ+7c=
golang.org/x/mod v0.19.0 h1:fEdghXQSo20giMthA7cd28ZC+jts4amQ3YMXiP5oMQ8=
golang.org/x/mod v0.19.0/go.mod h1:hTbmBsO62+eylJbnUtE2MGJUyE7QWk4xUqPFrRgJ+7c=
golang.org/x/net v0.0.0-20190404232315-eb5bcb51f2a3/go.mod h1:t9HGtf8HONx5eT2rtn7q6eTqICYqUVnKs3thJo3Qplg=
golang.org/x/net v0.0.0-20190620200207-3b0461eec859/go.mod h1:z5CRVTTTmAJ677TzLLGU+0bjPO0LkuOLi4/5GtJWs/s=
golang.org/x/net v0.0.0-20210226172049-e18ecbb05110/go.mod h1:m0MpNAwzfU5UDzcl9v0D8zg8gWTRqZa9RBIspLL5mdg=
Expand All @@ -70,6 +81,8 @@ golang.org/x/net v0.0.0-20211015210444-4f30a5c0130f/go.mod h1:9nx3DQGgdP8bBQD5qx
golang.org/x/sync v0.0.0-20190423024810-112230192c58/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
golang.org/x/sync v0.0.0-20210220032951-036812b2e83c/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
golang.org/x/sync v0.5.0 h1:60k92dhOjHxJkrqnwsfl8KuaHbn/5dl0lUPUklKo3qE=
golang.org/x/sync v0.7.0 h1:YsImfSBoP9QPYL0xyKJPq0gcaJdG3rInoqxTWbfQu9M=
golang.org/x/sync v0.7.0/go.mod h1:Czt+wKu1gCyEFDUtn0jG5QVvpJ6rzVqr5aXyt9drQfk=
golang.org/x/sys v0.0.0-20190215142949-d0b11bdaac8a/go.mod h1:STP8DvDyc/dI5b8T5hshtkjS+E42TnysNCUPdjciGhY=
golang.org/x/sys v0.0.0-20190222072716-a9d3bda3a223/go.mod h1:STP8DvDyc/dI5b8T5hshtkjS+E42TnysNCUPdjciGhY=
golang.org/x/sys v0.0.0-20190412213103-97732733099d/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
Expand All @@ -93,6 +106,8 @@ golang.org/x/sys v0.0.0-20220811171246-fbc7d0a398ab/go.mod h1:oPkhp1MJrh7nUepCBc
golang.org/x/sys v0.6.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/sys v0.14.0 h1:Vz7Qs629MkJkGyHxUlRHizWJRG2j8fbQKjELVSNhy7Q=
golang.org/x/sys v0.14.0/go.mod h1:/VUhepiaJMQUp4+oa/7Zr1D23ma6VTLIYjOOTFZPUcA=
golang.org/x/sys v0.22.0 h1:RI27ohtqKCnwULzJLqkv897zojh5/DwS/ENaMzUOaWI=
golang.org/x/sys v0.22.0/go.mod h1:/VUhepiaJMQUp4+oa/7Zr1D23ma6VTLIYjOOTFZPUcA=
golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1/go.mod h1:bj7SfCRtBDWHUb9snDiAeCFNEtKQo2Wmx5Cou7ajbmo=
golang.org/x/text v0.3.0/go.mod h1:NqM8EUOU14njkJ3fqMW+pc6Ldnwhi/IjpwHt7yyuwOQ=
golang.org/x/text v0.3.3/go.mod h1:5Zoc/QRtKVWzQhOtBMvqHzDpF6irO9z98xDceosuGiQ=
Expand All @@ -104,6 +119,8 @@ golang.org/x/tools v0.1.1/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
golang.org/x/tools v0.1.10/go.mod h1:Uh6Zz+xoGYZom868N8YTex3t7RhtHDBrE8Gzo9bV56E=
golang.org/x/tools v0.15.0 h1:zdAyfUGbYmuVokhzVmghFl2ZJh5QhcfebBgmVPFYA+8=
golang.org/x/tools v0.15.0/go.mod h1:hpksKq4dtpQWS1uQ61JkdqWM3LscIS6Slf+VVkm+wQk=
golang.org/x/tools v0.23.0 h1:SGsXPZ+2l4JsgaCKkx+FQ9YZ5XEtA1GZYuoDjenLjvg=
golang.org/x/tools v0.23.0/go.mod h1:pnu6ufv6vQkll6szChhK3C3L/ruaIv5eBeztNG8wtsI=
golang.org/x/xerrors v0.0.0-20190717185122-a985d3407aa7/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
golang.org/x/xerrors v0.0.0-20191011141410-1b5146add898/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
Expand All @@ -117,3 +134,5 @@ gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI=
gopkg.in/yaml.v3 v3.0.0-20200313102051-9f266ea9e77c/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM=
gopkg.in/yaml.v3 v3.0.0-20200615113413-eeeca48fe776 h1:tQIYjPdBoyREyB9XMu+nnTclpTYkz2zFM+lzLJFO4gQ=
gopkg.in/yaml.v3 v3.0.0-20200615113413-eeeca48fe776/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM=
gopkg.in/yaml.v3 v3.0.1 h1:fxVm/GzAzEWqLHuvctI91KS9hhNmmWOoWu0XTYJS7CA=
gopkg.in/yaml.v3 v3.0.1/go.mod h1:K4uyk7z7BCEPqu6E+C64Yfv1cQ7kz7rIZviUmN+EgEM=
12 changes: 6 additions & 6 deletions goose.go
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@
// include user-defined structs in Go as Coq records and a Perennial procedure
// for each Go function.
//
// See the Goose README at https://github.com/tchajed/goose for a high-level
// See the Goose README at https://github.com/goose-lang/goose for a high-level
// overview. The source also has some design documentation at
// https://github.com/tchajed/goose/tree/master/docs.
// https://github.com/goose-lang/goose/tree/master/docs.
package goose

import (
Expand All @@ -23,7 +23,7 @@ import (
"strings"
"unicode"

"github.com/tchajed/goose/glang"
"github.com/goose-lang/goose/glang"
"golang.org/x/tools/go/packages"
)

Expand Down Expand Up @@ -1509,9 +1509,9 @@ func stringLitValue(lit *ast.BasicLit) string {
}

var ffiMapping = map[string]string{
"github.com/mit-pdos/gokv/grove_ffi": "grove",
"github.com/tchajed/goose/machine/disk": "disk",
"github.com/tchajed/goose/machine/async_disk": "async_disk",
"github.com/mit-pdos/gokv/grove_ffi": "grove",
"github.com/goose-lang/goose/machine/disk": "disk",
"github.com/goose-lang/goose/machine/async_disk": "async_disk",
}

func (ctx Ctx) imports(d []ast.Spec) []glang.Decl {
Expand Down
2 changes: 1 addition & 1 deletion interface.go
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import (

"github.com/pkg/errors"

"github.com/tchajed/goose/glang"
"github.com/goose-lang/goose/glang"
"golang.org/x/tools/go/packages"
)

Expand Down
2 changes: 1 addition & 1 deletion machine/async_disk/async_disk.go
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package async_disk

import (
"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)

// Essentially a copy + paste of the disk interface. We do this so that we can
Expand Down
2 changes: 1 addition & 1 deletion machine/async_disk/file.go
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package async_disk

import (
"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)

type FileDisk = disk.FileDisk
Expand Down
2 changes: 1 addition & 1 deletion machine/async_disk/mem.go
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package async_disk

import (
"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)

type MemDisk = disk.MemDisk
Expand Down
2 changes: 1 addition & 1 deletion machine/disk/disk_bench_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import (
"os"
"testing"

"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)

var diskFile = flag.String("disk", "", "path to file to use for disk-based benchmark")
Expand Down
2 changes: 1 addition & 1 deletion machine/filesys/filesys_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ import (
"sort"
"testing"

"github.com/goose-lang/goose/machine/filesys"
"github.com/stretchr/testify/suite"
"github.com/tchajed/goose/machine/filesys"
)

// FilesysSuite implements a filesystem test suite generic over fs.
Expand Down
2 changes: 1 addition & 1 deletion testdata/examples/append_log/append_log.go
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import (

"github.com/tchajed/marshal"

"github.com/tchajed/goose/machine/disk"
"github.com/goose-lang/goose/machine/disk"
)

type Log struct {
Expand Down
4 changes: 2 additions & 2 deletions testdata/examples/append_log/append_log.gold.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(* autogenerated from github.com/tchajed/goose/testdata/examples/append_log *)
(* autogenerated from github.com/goose-lang/goose/testdata/examples/append_log *)
From New.golang Require Import defn.
From New.code Require github_com.tchajed.goose.machine.disk.
From New.code Require github_com.goose_lang.goose.machine.disk.
From New.code Require github_com.tchajed.marshal.
From New.code Require sync.

Expand Down
2 changes: 1 addition & 1 deletion testdata/examples/async/async.go
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// async just uses the async disk FFI
package async

import "github.com/tchajed/goose/machine/async_disk"
import "github.com/goose-lang/goose/machine/async_disk"

func TakesDisk(d async_disk.Disk) {}

Expand Down
4 changes: 2 additions & 2 deletions testdata/examples/async/async.gold.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(* autogenerated from github.com/tchajed/goose/testdata/examples/async *)
(* autogenerated from github.com/goose-lang/goose/testdata/examples/async *)
From New.golang Require Import defn.
From New.code Require github_com.tchajed.goose.machine.async_disk.
From New.code Require github_com.goose_lang.goose.machine.async_disk.

From New Require Import async_disk_prelude.

Expand Down
2 changes: 1 addition & 1 deletion testdata/examples/comments/comments.gold.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(* autogenerated from github.com/tchajed/goose/testdata/examples/comments *)
(* autogenerated from github.com/goose-lang/goose/testdata/examples/comments *)
From New.golang Require Import defn.

Section code.
Expand Down
10 changes: 5 additions & 5 deletions testdata/examples/go.mod
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
module github.com/tchajed/goose/testdata/examples
module github.com/goose-lang/goose/testdata/examples

go 1.22

require (
github.com/goose-lang/goose v0.6.1
github.com/stretchr/testify v1.9.0
github.com/tchajed/goose v0.5.3
github.com/tchajed/marshal v0.6.0
github.com/tchajed/marshal v0.6.1
)

require (
github.com/davecgh/go-spew v1.1.1 // indirect
github.com/goose-lang/std v0.0.0-20240314130527-d1c85b72c3f7 // indirect
github.com/goose-lang/std v0.3.2 // indirect
github.com/pkg/errors v0.9.1 // indirect
github.com/pmezard/go-difflib v1.0.0 // indirect
golang.org/x/sys v0.6.0 // indirect
golang.org/x/sys v0.22.0 // indirect
gopkg.in/yaml.v3 v3.0.1 // indirect
)
Loading

0 comments on commit 926bda7

Please sign in to comment.