Skip to content

Commit

Permalink
Provide a way to skip interface conversions
Browse files Browse the repository at this point in the history
There's a bug in how they're generated which I don't want to fix right
now (and the interface in question is disk.Disk).
  • Loading branch information
tchajed committed Jun 26, 2024
1 parent ae6ea11 commit d039f2d
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 2 deletions.
1 change: 1 addition & 0 deletions cmd/goose/main.go
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ func main() {
flag.BoolVar(&tr.AddSourceFileComments, "source-comments", false,
"add comments indicating Go source code location for each top-level declaration")
flag.BoolVar(&tr.TypeCheck, "typecheck", false, "add type-checking theorems")
flag.BoolVar(&tr.SkipInterfaces, "skip-interfaces", false, "skip creating interface conversions")

var outRootDir string
flag.StringVar(&outRootDir, "out", ".",
Expand Down
6 changes: 4 additions & 2 deletions goose.go
Original file line number Diff line number Diff line change
Expand Up @@ -2190,8 +2190,10 @@ func (ctx Ctx) maybeDecls(d ast.Decl) []coq.Decl {
switch d := d.(type) {
case *ast.FuncDecl:
var cvs []coq.Decl
for _, stmt := range d.Body.List {
cvs = ctx.stmtInterface(cvs, stmt)
if !ctx.SkipInterfaces {
for _, stmt := range d.Body.List {
cvs = ctx.stmtInterface(cvs, stmt)
}
}
fd := ctx.funcDecl(d)
var results []coq.Decl
Expand Down
1 change: 1 addition & 0 deletions interface.go
Original file line number Diff line number Diff line change
Expand Up @@ -176,6 +176,7 @@ func sortedFiles(fileNames []string, fileAsts []*ast.File) []NamedFile {
type TranslationConfig struct {
TypeCheck bool
AddSourceFileComments bool
SkipInterfaces bool
}

func pkgErrors(errors []packages.Error) error {
Expand Down

0 comments on commit d039f2d

Please sign in to comment.