mk: removing extraneous .ml files after extracting

Helps when renaming modules.
FStarLang · Jan 9, 2025 · 3e1a783 · 3e1a783
1 parent c72e8b7
commit 3e1a783
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 0 deletions.
diff --git a/mk/fstar-12.mk b/mk/fstar-12.mk
@@ -79,4 +79,10 @@ depend: $(CACHE_DIR)/.depend$(TAG)
 include $(CACHE_DIR)/.depend$(TAG)
 
 all-ml: $(ALL_ML_FILES)
+	@# Remove extraneous .ml files, which can linger after
+	@# module renamings. The realpath is necessary to prevent
+	@# discrepancies between absolute and relative paths, double
+	@# slashes, etc.
+	rm -vf $(filter-out $(realpath $(ALL_ML_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.ml)))
+
 all-checked: $(ALL_CHECKED_FILES)
diff --git a/mk/lib.mk b/mk/lib.mk
@@ -142,4 +142,11 @@ all-checked: $(ALL_CHECKED_FILES)
 # These targets imply verification of every file too, regardless
 # of extraction.
 all-ml: all-checked $(ALL_ML_FILES)
+	@# Remove extraneous .ml files, which can linger after
+	@# module renamings. The realpath is necessary to prevent
+	@# discrepancies between absolute and relative paths, double
+	@# slashes, etc.
+	rm -vf $(filter-out $(realpath $(ALL_ML_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.ml)))
+
 all-fs: all-checked $(ALL_FS_FILES)
+	rm -vf $(filter-out $(realpath $(ALL_FS_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.fs)))
diff --git a/mk/plugins.mk b/mk/plugins.mk
@@ -123,3 +123,8 @@ depend: $(CACHE_DIR)/.depend$(TAG)
 include $(CACHE_DIR)/.depend$(TAG)
 
 all-ml: $(ALL_ML_FILES)
+	@# Remove extraneous .ml files, which can linger after
+	@# module renamings. The realpath is necessary to prevent
+	@# discrepancies between absolute and relative paths, double
+	@# slashes, etc.
+	rm -vf $(filter-out $(realpath $(ALL_ML_FILES)), $(realpath $(wildcard $(OUTPUT_DIR)/*.ml)))