mk: removing extraneous .ml files after extracting

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

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/mk/fstar-12.mk b/mk/fstar-12.mk
@@ -79,4 +79,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.
+	rm -f $(filter-out $(ALL_ML_FILES), $(wildcard $(OUTPUT_DIR)/*.ml))
+
 all-checked: $(ALL_CHECKED_FILES)
diff --git a/mk/lib.mk b/mk/lib.mk
@@ -142,4 +142,9 @@ 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.
+	rm -f $(filter-out $(ALL_ML_FILES), $(wildcard $(OUTPUT_DIR)/*.ml))
+
 all-fs: all-checked $(ALL_FS_FILES)
+	rm -f $(filter-out $(ALL_FS_FILES), $(wildcard $(OUTPUT_DIR)/*.fs))
diff --git a/mk/plugins.mk b/mk/plugins.mk
@@ -123,3 +123,6 @@ 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.
+	rm -f $(filter-out $(ALL_ML_FILES), $(wildcard $(OUTPUT_DIR)/*.ml))