Skip to content

Commit e0d50e0

Browse files
tchajedtchajed
committed
Merge branch 'module-aware'
Implement module-aware loading using golang.org/x/tools/go/packages to load source code, rather than using ParseFile directly. - Fixes #9 - Fixes #10 - Fixes #19 Also adds 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 disk or dist_ffi; "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 goose binary's command-line interface is now tested directly in CI using BATS, a bash testing framework.
2 parents e124991 + 37504cf commit e0d50e0

39 files changed

+660
-176
lines changed

‎.github/workflows/build.yml

+7-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ on:
44
push:
55
branches:
66
- master
7+
- "*"
78
pull_request:
89

910
jobs:
@@ -19,12 +20,17 @@ jobs:
1920
with:
2021
go-version: ${{ matrix.go-version }}
2122
- uses: actions/checkout@v2
23+
with:
24+
submodules: true
2225
- name: Check style
2326
run: |
2427
gofmt -w -s .
2528
go generate ./...
2629
git diff --exit-code
27-
- name: Test
30+
- name: Go tests
2831
run: |
2932
go vet -composites=false ./...
3033
go test -v ./...
34+
- name: End-to-end CLI tests
35+
run: |
36+
./test/bats/bin/bats ./test/goose.bats

‎.gitmodules

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
[submodule "test/bats"]
2+
path = test/bats
3+
url = https://github.com/bats-core/bats-core.git
4+
[submodule "test/test_helper/bats-support"]
5+
path = test/test_helper/bats-support
6+
url = https://github.com/bats-core/bats-support.git
7+
[submodule "test/test_helper/bats-assert"]
8+
path = test/test_helper/bats-assert
9+
url = https://github.com/bats-core/bats-assert.git

‎cmd/goose/main.go

+52-49
Original file line numberDiff line numberDiff line change
@@ -12,70 +12,73 @@ import (
1212
"github.com/tchajed/goose/internal/coq"
1313
)
1414

15+
func translate(pkgPatterns []string, outRootDir string, modDir string,
16+
ignoreErrors bool, tr goose.Translator) {
17+
red := color.New(color.FgRed).SprintFunc()
18+
fs, errs, patternError := tr.TranslatePackages(modDir, pkgPatterns...)
19+
if patternError != nil {
20+
fmt.Fprintln(os.Stderr, red(patternError.Error()))
21+
os.Exit(1)
22+
}
23+
24+
someError := false
25+
for i, f := range fs {
26+
err := errs[i]
27+
if err != nil {
28+
fmt.Fprintln(os.Stderr, red(err.Error()))
29+
someError = true
30+
if !ignoreErrors {
31+
continue
32+
}
33+
}
34+
outFile := path.Join(outRootDir,
35+
coq.ImportToPath(f.PkgPath, f.GoPackage))
36+
outDir := path.Dir(outFile)
37+
err = os.MkdirAll(outDir, 0777)
38+
if err != nil {
39+
fmt.Fprintln(os.Stderr, err.Error())
40+
fmt.Fprintln(os.Stderr, red("could not create output directory"))
41+
}
42+
out, err := os.Create(outFile)
43+
defer out.Close()
44+
f.Write(out)
45+
if err != nil {
46+
fmt.Fprintln(os.Stderr, err.Error())
47+
fmt.Fprintln(os.Stderr, red("could not write output"))
48+
os.Exit(1)
49+
}
50+
}
51+
if someError {
52+
os.Exit(1)
53+
}
54+
}
55+
1556
//noinspection GoUnhandledErrorResult
1657
func main() {
1758
flag.Usage = func() {
1859
fmt.Fprintln(flag.CommandLine.Output(), "Usage: goose [options] <path to go package>")
1960

2061
flag.PrintDefaults()
2162
}
22-
var config goose.Config = goose.MakeDefaultConfig()
23-
flag.BoolVar(&config.AddSourceFileComments, "source-comments", false,
63+
var tr goose.Translator
64+
65+
flag.BoolVar(&tr.AddSourceFileComments, "source-comments", false,
2466
"add comments indicating Go source code location for each top-level declaration")
25-
flag.BoolVar(&config.TypeCheck, "typecheck", false,
26-
"add type-checking theorems")
27-
flag.Var(&config.Excludes, "exclude-import", "go package that should not generate a coq import; can specify multiple packages to exclude")
28-
flag.StringVar(&config.Ffi, "ffi", config.Ffi,
29-
"FFI {disk|dist|none} (not specified defaults to disk)")
67+
flag.BoolVar(&tr.TypeCheck, "typecheck", false, "add type-checking theorems")
3068

31-
var outFile string
32-
flag.StringVar(&outFile, "out", "-",
33-
"file to output to (use '-' for stdout)")
69+
var outRootDir string
70+
flag.StringVar(&outRootDir, "out", ".",
71+
"root directory for output (default is current directory)")
3472

35-
var packagePath string
36-
flag.StringVar(&packagePath, "package", "",
37-
"output to a package path")
73+
var modDir string
74+
flag.StringVar(&modDir, "dir", ".",
75+
"directory containing necessary go.mod")
3876

3977
var ignoreErrors bool
4078
flag.BoolVar(&ignoreErrors, "ignore-errors", false,
4179
"output partial translation even if there are errors")
4280

4381
flag.Parse()
44-
if flag.NArg() != 1 {
45-
flag.Usage()
46-
os.Exit(1)
47-
}
48-
srcDir := flag.Arg(0)
4982

50-
red := color.New(color.FgRed).SprintFunc()
51-
f, err := config.TranslatePackage(packagePath, srcDir)
52-
if err != nil {
53-
fmt.Fprintln(os.Stderr, red(err.Error()))
54-
if !ignoreErrors {
55-
os.Exit(1)
56-
}
57-
}
58-
if outFile == "-" {
59-
f.Write(os.Stdout)
60-
} else {
61-
if packagePath != "" {
62-
outFile = path.Join(outFile, coq.ImportToPath(packagePath))
63-
outDir := path.Dir(outFile)
64-
_, err := os.Stat(outDir)
65-
if os.IsNotExist(err) {
66-
os.MkdirAll(outDir, 0777)
67-
}
68-
}
69-
out, err := os.Create(outFile)
70-
if err != nil {
71-
fmt.Fprintln(os.Stderr, err.Error())
72-
fmt.Fprintln(os.Stderr, red("could not write output"))
73-
os.Exit(1)
74-
}
75-
defer out.Close()
76-
f.Write(out)
77-
}
78-
if err != nil {
79-
os.Exit(1)
80-
}
83+
translate(flag.Args(), outRootDir, modDir, ignoreErrors, tr)
8184
}

‎examples_test.go

+25-25
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,8 @@ func (t positiveTest) DeleteActual() {
113113
_ = os.Remove(t.ActualFile())
114114
}
115115

116-
func testExample(testingT *testing.T, name string, conf goose.Config) {
116+
func testExample(testingT *testing.T, name string, tr goose.Translator) {
117+
testingT.Parallel()
117118
testingT.Helper()
118119
assert := assert.New(testingT)
119120
t := positiveTest{newTest("internal/examples", name)}
@@ -124,7 +125,16 @@ func testExample(testingT *testing.T, name string, conf goose.Config) {
124125
}
125126
// c.Logf("testing example %s/", t.Path)
126127

127-
f, terr := conf.TranslatePackage("", t.path)
128+
files, errs, patternError := tr.TranslatePackages(t.path, ".")
129+
if patternError != nil {
130+
// shouldn't be possible since "." is valid
131+
assert.FailNowf("loading failed", "load error: %v", patternError)
132+
}
133+
if !(len(files) == 1 && len(errs) == 1) {
134+
assert.FailNowf("pattern matched unexpected number of packages",
135+
"files: %v", files)
136+
}
137+
f, terr := files[0], errs[0]
128138
if terr != nil {
129139
fmt.Fprintln(os.Stderr, terr)
130140
assert.FailNow("translation failed")
@@ -162,46 +172,35 @@ func testExample(testingT *testing.T, name string, conf goose.Config) {
162172
}
163173

164174
func TestUnitTests(t *testing.T) {
165-
testExample(t, "unittest", goose.MakeDefaultConfig())
175+
testExample(t, "unittest", goose.Translator{})
166176
}
167177

168178
func TestSimpleDb(t *testing.T) {
169-
testExample(t, "simpledb", goose.MakeDefaultConfig())
179+
testExample(t, "simpledb", goose.Translator{})
170180
}
171181

172182
func TestWal(t *testing.T) {
173-
c := goose.MakeDefaultConfig()
174-
c.TypeCheck = true
175-
testExample(t, "wal", c)
183+
testExample(t, "wal", goose.Translator{TypeCheck: true})
176184
}
177185

178186
func TestLogging2(t *testing.T) {
179-
c := goose.MakeDefaultConfig()
180-
c.TypeCheck = true
181-
testExample(t, "logging2", c)
187+
testExample(t, "logging2", goose.Translator{TypeCheck: true})
182188
}
183189

184190
func TestAppendLog(t *testing.T) {
185-
c := goose.MakeDefaultConfig()
186-
c.TypeCheck = true
187-
testExample(t, "append_log", c)
191+
testExample(t, "append_log", goose.Translator{TypeCheck: true})
188192
}
189193

190194
func TestRfc1813(t *testing.T) {
191-
c := goose.MakeDefaultConfig()
192-
c.TypeCheck = true
193-
testExample(t, "rfc1813", c)
195+
testExample(t, "rfc1813", goose.Translator{TypeCheck: true})
194196
}
195197

196198
func TestSemantics(t *testing.T) {
197-
c := goose.MakeDefaultConfig()
198-
c.TypeCheck = true
199-
testExample(t, "semantics", c)
199+
testExample(t, "semantics", goose.Translator{TypeCheck: true})
200200
}
201201

202202
func TestComments(t *testing.T) {
203-
c := goose.MakeDefaultConfig()
204-
testExample(t, "comments", c)
203+
testExample(t, "comments", goose.Translator{})
205204
}
206205

207206
type errorExpectation struct {
@@ -239,17 +238,17 @@ func getExpectedError(fset *token.FileSet,
239238
}
240239

241240
func translateErrorFile(assert *assert.Assertions, filePath string) *errorTestResult {
242-
fset := token.NewFileSet()
243241
pkgName := "example"
244-
ctx := goose.NewCtx(pkgName, fset, goose.Config{})
242+
ctx := goose.NewCtx(pkgName, goose.Config{})
243+
fset := ctx.Fset
245244
f, err := parser.ParseFile(fset, filePath, nil, parser.ParseComments)
246245
if err != nil {
247246
fmt.Fprintln(os.Stderr, err)
248247
assert.FailNowf("test code for %s does not parse", filePath)
249248
return nil
250249
}
251250

252-
err = ctx.TypeCheck(pkgName, []*ast.File{f})
251+
err = ctx.TypeCheck([]*ast.File{f})
253252
if err != nil {
254253
fmt.Fprintln(os.Stderr, err)
255254
assert.FailNowf("test code for %s does not type check", filePath)
@@ -278,12 +277,13 @@ func translateErrorFile(assert *assert.Assertions, filePath string) *errorTestRe
278277
}
279278

280279
func TestNegativeExamples(testingT *testing.T) {
281-
tests := loadTests("./testdata")
280+
tests := loadTests("./testdata/negative-tests")
282281
for _, t := range tests {
283282
if t.isDir() {
284283
continue
285284
}
286285
testingT.Run(t.name, func(testingT *testing.T) {
286+
testingT.Parallel()
287287
assert := assert.New(testingT)
288288
tt := translateErrorFile(assert, t.path)
289289
if tt == nil {

‎go.mod

+3-1
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,16 @@ module github.com/tchajed/goose
33
go 1.12
44

55
require (
6+
github.com/davecgh/go-spew v1.1.1
67
github.com/fatih/color v1.9.0
78
github.com/kr/text v0.2.0 // indirect
89
github.com/mattn/go-colorable v0.1.7 // indirect
910
github.com/niemeyer/pretty v0.0.0-20200227124842-a10e7caefd8e // indirect
1011
github.com/pkg/errors v0.9.1
1112
github.com/stretchr/testify v1.6.1
1213
github.com/tchajed/marshal v0.0.0-20200707011626-0d2aa09818a9
13-
golang.org/x/sys v0.0.0-20200817155316-9781c653f443
14+
golang.org/x/sys v0.0.0-20210510120138-977fb7262007
15+
golang.org/x/tools v0.1.1
1416
gopkg.in/check.v1 v1.0.0-20200227125254-8fa46927fb4f // indirect
1517
gopkg.in/yaml.v3 v3.0.0-20200615113413-eeeca48fe776 // indirect
1618
)

‎go.sum

+27
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,19 @@ github.com/tchajed/mailboat v0.2.0 h1:RhSuuqrmYf+h9tk64yZf5CuuoQ/2Ux8vnnNgt5WqM4
5151
github.com/tchajed/mailboat v0.2.0/go.mod h1:aKa/T1YCMVZFM2xbXnMNyp9r4k0pPni4+sJ8GoY51Hw=
5252
github.com/tchajed/marshal v0.0.0-20200707011626-0d2aa09818a9 h1:OsIWWeXLwFAp5aBxEyqlsH7mglcWE3WnyZSFV7LYmCE=
5353
github.com/tchajed/marshal v0.0.0-20200707011626-0d2aa09818a9/go.mod h1:TPo3bTYJkH87/4rXlxe0bpVWLnN+b5kjJnoXHLBfdaA=
54+
github.com/yuin/goldmark v1.3.5/go.mod h1:mwnBkeHKe2W/ZEtQ+71ViKU8L12m81fl3OWwC1Zlc8k=
55+
golang.org/x/crypto v0.0.0-20190308221718-c2843e01d9a2/go.mod h1:djNgcEr1/C05ACkg1iLfiJU5Ep61QUkGW8qpdssI0+w=
56+
golang.org/x/crypto v0.0.0-20191011191535-87dc89f01550/go.mod h1:yigFU9vqHzYiE8UmvKecakEJjdnWj3jj499lnFckfCI=
57+
golang.org/x/mod v0.4.2 h1:Gz96sIWK3OalVv/I/qNygP42zyoKp3xptRVCWRFEBvo=
58+
golang.org/x/mod v0.4.2/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
59+
golang.org/x/net v0.0.0-20190404232315-eb5bcb51f2a3/go.mod h1:t9HGtf8HONx5eT2rtn7q6eTqICYqUVnKs3thJo3Qplg=
60+
golang.org/x/net v0.0.0-20190620200207-3b0461eec859/go.mod h1:z5CRVTTTmAJ677TzLLGU+0bjPO0LkuOLi4/5GtJWs/s=
61+
golang.org/x/net v0.0.0-20210405180319-a5a99cb37ef4/go.mod h1:p54w0d4576C0XHj96bSt6lcn1PtDYWL6XObtHCRCNQM=
62+
golang.org/x/sync v0.0.0-20190423024810-112230192c58/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
63+
golang.org/x/sync v0.0.0-20210220032951-036812b2e83c/go.mod h1:RxMgew5VJxzue5/jJTE5uejpjVlOe/izrB70Jof72aM=
64+
golang.org/x/sys v0.0.0-20190215142949-d0b11bdaac8a/go.mod h1:STP8DvDyc/dI5b8T5hshtkjS+E42TnysNCUPdjciGhY=
5465
golang.org/x/sys v0.0.0-20190222072716-a9d3bda3a223/go.mod h1:STP8DvDyc/dI5b8T5hshtkjS+E42TnysNCUPdjciGhY=
66+
golang.org/x/sys v0.0.0-20190412213103-97732733099d/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
5567
golang.org/x/sys v0.0.0-20191008105621-543471e840be h1:QAcqgptGM8IQBC9K/RC4o+O9YmqEm0diQn9QmZw/0mU=
5668
golang.org/x/sys v0.0.0-20191008105621-543471e840be/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
5769
golang.org/x/sys v0.0.0-20191026070338-33540a1f6037/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
@@ -64,6 +76,21 @@ golang.org/x/sys v0.0.0-20200223170610-d5e6a3e2c0ae h1:/WDfKMnPU+m5M4xB+6x4kaepx
6476
golang.org/x/sys v0.0.0-20200223170610-d5e6a3e2c0ae/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
6577
golang.org/x/sys v0.0.0-20200817155316-9781c653f443 h1:X18bCaipMcoJGm27Nv7zr4XYPKGUy92GtqboKC2Hxaw=
6678
golang.org/x/sys v0.0.0-20200817155316-9781c653f443/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
79+
golang.org/x/sys v0.0.0-20201119102817-f84b799fce68/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
80+
golang.org/x/sys v0.0.0-20210330210617-4fbd30eecc44/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
81+
golang.org/x/sys v0.0.0-20210510120138-977fb7262007 h1:gG67DSER+11cZvqIMb8S8bt0vZtiN6xWYARwirrOSfE=
82+
golang.org/x/sys v0.0.0-20210510120138-977fb7262007/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
83+
golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1/go.mod h1:bj7SfCRtBDWHUb9snDiAeCFNEtKQo2Wmx5Cou7ajbmo=
84+
golang.org/x/text v0.3.0/go.mod h1:NqM8EUOU14njkJ3fqMW+pc6Ldnwhi/IjpwHt7yyuwOQ=
85+
golang.org/x/text v0.3.3/go.mod h1:5Zoc/QRtKVWzQhOtBMvqHzDpF6irO9z98xDceosuGiQ=
86+
golang.org/x/tools v0.0.0-20180917221912-90fa682c2a6e/go.mod h1:n7NCudcB/nEzxVGmLbDWY5pfWTLqBcC2KZ6jyYvM4mQ=
87+
golang.org/x/tools v0.0.0-20191119224855-298f0cb1881e/go.mod h1:b+2E5dAYhXwXZwtnZ6UAqBI28+e2cm9otk0dWdXHAEo=
88+
golang.org/x/tools v0.1.1 h1:wGiQel/hW0NnEkJUk8lbzkX2gFJU6PFxf1v5OlCfuOs=
89+
golang.org/x/tools v0.1.1/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
90+
golang.org/x/xerrors v0.0.0-20190717185122-a985d3407aa7/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
91+
golang.org/x/xerrors v0.0.0-20191011141410-1b5146add898/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
92+
golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1 h1:go1bK/D/BFZV2I8cIQd1NKEZ+0owSTG1fDTci4IqFcE=
93+
golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
6794
gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
6895
gopkg.in/check.v1 v1.0.0-20190902080502-41f04d3bba15/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
6996
gopkg.in/check.v1 v1.0.0-20200227125254-8fa46927fb4f h1:BLraFXnmrev5lT+xlilqcH8XK9/i0At2xKjWk4p6zsU=

0 commit comments

Comments
 (0)