File tree Expand file tree Collapse file tree 1 file changed +12
-4
lines changed Expand file tree Collapse file tree 1 file changed +12
-4
lines changed Original file line number Diff line number Diff line change @@ -100,7 +100,7 @@ endef
100
100
export FINDLIBS
101
101
102
102
FSTAR_INCLUDE_DIRS_EXTRA ?=
103
- FINDLIBS_OUTPUT : = $(shell bash -c '${FINDLIBS}')
103
+ FINDLIBS_OUTPUT ? = $(shell bash -c '${FINDLIBS}')
104
104
FSTAR_INCLUDE_DIRS = $(FSTAR_INCLUDE_DIRS_EXTRA) $(FINDLIBS_OUTPUT)
105
105
106
106
# Make sure FSTAR_INCLUDE_DIRS has the `proof-libs`, print hints and
@@ -128,10 +128,16 @@ all-keep-going:
128
128
$(Q)rm -f .depend
129
129
$(Q)$(MAKE) --keep-going .depend hax.fst.config.json verify
130
130
131
- # If no any F* file is detected, we run hax
131
+ # Only run code extraction for build targets, not for 'clean'.
132
+ all all-keep-going:
132
133
ifeq "$(wildcard *.fst *fsti)" ""
133
- $(shell cargo hax into fstar)
134
+ $(shell cargo hax into fstar)
134
135
endif
136
+ $(Q)rm -f .depend
137
+ all:
138
+ $(Q)$(MAKE) .depend hax.fst.config.json verify
139
+ all-keep-going:
140
+ $(Q)$(MAKE) --keep-going .depend hax.fst.config.json verify
135
141
136
142
# By default, we process all the files in the current directory
137
143
ROOTS ?= $(wildcard *.fst *fsti)
@@ -257,9 +263,11 @@ vscode:
257
263
$(Q)rm -f .depend
258
264
$(Q)$(MAKE) hax.fst.config.json
259
265
266
+
267
+ .PHONY: clean
260
268
SHELL=bash
261
269
262
270
# Clean target
263
271
clean:
264
272
rm -rf $(CACHE_DIR)/*
265
- rm *.fst
273
+ rm -f *.fst *.fsti *.hints *.smt2
You can’t perform that action at this time.
0 commit comments