Skip to content

Commit

Permalink
Use new CLI for Go translation
Browse files Browse the repository at this point in the history
  • Loading branch information
tchajed committed Jan 12, 2024
1 parent 6f0c12a commit 7889de0
Showing 1 changed file with 1 addition and 5 deletions.
6 changes: 1 addition & 5 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,7 @@ DFY_FILES := $(shell find src -name "*.dfy")
OK_FILES := $(DFY_FILES:.dfy=.dfy.ok)

DAFNY_CORES := "50%"

# these arguments don't affect verification outcomes
DAFNY_BASIC_ARGS := --verification-time-limit 20 --cores $(DAFNY_CORES)

DAFNY_ARGS := --disable-nonlinear-arithmetic
DAFNY = ./etc/dafnyq verify $(DAFNY_BASIC_ARGS) $(DAFNY_ARGS)

Expand Down Expand Up @@ -44,8 +41,7 @@ src/nonlin/%.dfy.ok: DAFNY_ARGS =
# up unused imports emitted by Dafny.
dafnygen/dafnygen.go: src/compile.dfy $(DFY_FILES)
@echo "DAFNY COMPILE $<"
# TODO: use dafny translate (new CLI)
$(Q)./etc/dafnyq /compileTarget:go /noVerify /spillTargetCode:2 /out dafnygen $<
$(Q)./etc/dafnyq translate go --no-verify --include-runtime --output dafnygen $<
$(Q)rm -rf dafnygen
$(Q)cd dafnygen-go/src && ../../etc/dafnygen-imports.py ../../dafnygen
$(Q)rm -r dafnygen-go
Expand Down

0 comments on commit 7889de0

Please sign in to comment.