Skip to content

Commit 0d18a08

Browse files
mtzguidomtzguido
authored
Merge pull request #3664 from mtzguido/mkrm
mk: removing extraneous .ml files after extracting
2 parents c72e8b7 + 9766228 commit 0d18a08

3 files changed

Lines changed: 68 additions & 14 deletions

File tree

‎mk/fstar-12.mk‎

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -70,13 +70,31 @@ EXTRACT += --extract +FStar.Seq.Properties
7070
ROOTS :=
7171
ROOTS += $(SRC)/fstar/FStarC.Main.fst
7272

73-
$(CACHE_DIR)/.depend$(TAG):
73+
DEPSTEM := $(CACHE_DIR)/.depend$(TAG)
74+
# We always run this to compute a full list of fst/fsti files in the
75+
# $(SRC) (ignoring the roots, it's a bit conservative). The list is
76+
# saved in $(DEPSTEM).touch.chk, and compared to the one we generated
77+
# before in $(DEPSTEM).touch. If there's a change (or the 'previous')
78+
# does not exist, the timestamp of $(DEPSTEM0.touch will be updated
79+
# triggering an actual dependency run.
80+
.PHONY: .force
81+
$(DEPSTEM).touch: .force
82+
mkdir -p $(dir $@)
83+
find $(SRC) -name '*.fst*' > $@.chk
84+
diff -q $@ $@.chk 2>/dev/null || cp $@.chk $@
85+
86+
$(DEPSTEM): $(DEPSTEM).touch
7487
$(call msg, "DEPEND", $(SRC))
7588
$(FSTAR) --dep full $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $@
76-
mkdir -p $(CACHE_DIR)
7789

78-
depend: $(CACHE_DIR)/.depend$(TAG)
79-
include $(CACHE_DIR)/.depend$(TAG)
90+
depend: $(DEPSTEM)
91+
include $(DEPSTEM)
8092

8193
all-ml: $(ALL_ML_FILES)
94+
@# Remove extraneous .ml files, which can linger after
95+
@# module renamings. The realpath is necessary to prevent
96+
@# discrepancies between absolute and relative paths, double
97+
@# slashes, etc.
98+
rm -vf $(filter-out $(realpath $(ALL_ML_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.ml)))
99+
82100
all-checked: $(ALL_CHECKED_FILES)

‎mk/lib.mk‎

Lines changed: 23 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -130,16 +130,35 @@ EXTRACT := --extract '* $(EXTRACT_NS)'
130130
# file in the cwd named like a file in ulib/, F* may prefer the former.
131131
ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
132132

133-
$(CACHE_DIR)/.depend$(TAG):
133+
DEPSTEM := $(CACHE_DIR)/.depend$(TAG)
134+
# We always run this to compute a full list of fst/fsti files in the
135+
# $(SRC) (ignoring the roots, it's a bit conservative). The list is
136+
# saved in $(DEPSTEM).touch.chk, and compared to the one we generated
137+
# before in $(DEPSTEM).touch. If there's a change (or the 'previous')
138+
# does not exist, the timestamp of $(DEPSTEM0.touch will be updated
139+
# triggering an actual dependency run.
140+
.PHONY: .force
141+
$(DEPSTEM).touch: .force
142+
mkdir -p $(dir $@)
143+
find $(SRC) -name '*.fst*' > $@.chk
144+
diff -q $@ $@.chk 2>/dev/null || cp $@.chk $@
145+
146+
$(DEPSTEM): $(DEPSTEM).touch
134147
$(call msg, "DEPEND", $(SRC))
135148
$(FSTAR) --dep full $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $@
136-
mkdir -p $(CACHE_DIR)
137149

138-
depend: $(CACHE_DIR)/.depend$(TAG)
139-
include $(CACHE_DIR)/.depend$(TAG)
150+
depend: $(DEPSTEM)
151+
include $(DEPSTEM)
140152

141153
all-checked: $(ALL_CHECKED_FILES)
142154
# These targets imply verification of every file too, regardless
143155
# of extraction.
144156
all-ml: all-checked $(ALL_ML_FILES)
157+
@# Remove extraneous .ml files, which can linger after
158+
@# module renamings. The realpath is necessary to prevent
159+
@# discrepancies between absolute and relative paths, double
160+
@# slashes, etc.
161+
rm -vf $(filter-out $(realpath $(ALL_ML_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.ml)))
162+
145163
all-fs: all-checked $(ALL_FS_FILES)
164+
rm -vf $(filter-out $(realpath $(ALL_FS_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.fs)))

‎mk/plugins.mk‎

Lines changed: 23 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -114,12 +114,29 @@ ROOTS += ../ulib/FStar.Tactics.V2.Logic.fsti
114114
ROOTS += ../ulib/FStar.Tactics.V2.SyntaxHelpers.fst
115115
ROOTS += ../ulib/FStar.Tactics.Visit.fst
116116

117-
$(CACHE_DIR)/.depend$(TAG):
118-
$(call msg, "DEPEND")
119-
$(FSTAR) --dep full $(ROOTS) $(EXTRACT) --output_deps_to $@
120-
mkdir -p $(CACHE_DIR)
117+
DEPSTEM := $(CACHE_DIR)/.depend$(TAG)
118+
# We always run this to compute a full list of fst/fsti files in the
119+
# $(SRC) (ignoring the roots, it's a bit conservative). The list is
120+
# saved in $(DEPSTEM).touch.chk, and compared to the one we generated
121+
# before in $(DEPSTEM).touch. If there's a change (or the 'previous')
122+
# does not exist, the timestamp of $(DEPSTEM0.touch will be updated
123+
# triggering an actual dependency run.
124+
.PHONY: .force
125+
$(DEPSTEM).touch: .force
126+
mkdir -p $(dir $@)
127+
find $(SRC) -name '*.fst*' > $@.chk
128+
diff -q $@ $@.chk 2>/dev/null || cp $@.chk $@
121129

122-
depend: $(CACHE_DIR)/.depend$(TAG)
123-
include $(CACHE_DIR)/.depend$(TAG)
130+
$(DEPSTEM): $(DEPSTEM).touch
131+
$(call msg, "DEPEND", $(SRC))
132+
$(FSTAR) --dep full $(ROOTS) $(EXTRACT) $(DEPFLAGS) --output_deps_to $@
133+
134+
depend: $(DEPSTEM)
135+
include $(DEPSTEM)
124136

125137
all-ml: $(ALL_ML_FILES)
138+
@# Remove extraneous .ml files, which can linger after
139+
@# module renamings. The realpath is necessary to prevent
140+
@# discrepancies between absolute and relative paths, double
141+
@# slashes, etc.
142+
rm -vf $(filter-out $(realpath $(ALL_ML_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.ml)))

0 commit comments

Comments
 (0)