Skip to content

Commit

Permalink
tweak makefile
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Nov 7, 2024
1 parent 19afac2 commit 919d21c
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions examples/native_tactics/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
# 'include test.mk'.

FSTAR_HOME=../..
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)
FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS)

# Tests for which the native tactics used in module named Sample.Test.fst are
# declared in a corresponding module named Sample.fst
Expand Down Expand Up @@ -48,33 +48,33 @@ OTHERFLAGS +=
all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL))

# .depend:
# $(FSTAR) --dep full $(addsuffix .Test.fst, $(ALL)) --output_deps_to .depend
# $(FSTAR_EXE) --dep full $(addsuffix .Test.fst, $(ALL)) --output_deps_to .depend

# include .depend

.PHONY: %.test
.PRECIOUS: %.ml

%.test: %.fst %.ml
$(FSTAR) $*.fst --load $*
$(FSTAR_EXE) $*.fst --load $*
touch $@

%.sep.test: %.fst %.ml
$(FSTAR) $*.Test.fst --load $*
$(FSTAR_EXE) $*.Test.fst --load $*
touch $@

%.ml: %.fst
$(FSTAR) $*.fst --cache_checked_modules --codegen Plugin --extract $*
$(FSTAR_EXE) $*.fst --cache_checked_modules --codegen Plugin --extract $*
touch $@

%.clean:
rm -f Registers_List.ml Registers.List.ml Registers_List.cmxs

%.native: %.fst Registers.List.ml
$(FSTAR) $*.fst --load Registers.List --warn_error -266
$(FSTAR_EXE) $*.fst --load Registers.List --warn_error -266

%.interp: %.fst Registers.List.fst
$(FSTAR) $*.fst
$(FSTAR_EXE) $*.fst


clean:
Expand Down

0 comments on commit 919d21c

Please sign in to comment.