refactor runlim settings

FStarLang · Jul 12, 2023 · 7343ac2 · 7343ac2
1 parent 83f4118
commit 7343ac2
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 22 deletions.
diff --git a/lib/steel/Makefile b/lib/steel/Makefile
@@ -13,17 +13,7 @@ FSTAR_OPTIONS=$(OTHERFLAGS) --cache_checked_modules --warn_error @241 --already_
 COMPAT_INDEXED_EFFECTS=--compat_pre_typed_indexed_effects
 MY_FSTAR=$(RUNLIM) $(FSTAR) $(SIL) $(FSTAR_OPTIONS)
 
-# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
-# information about the time and space taken by each F* invocation.
-ifneq ($(RESOURCEMONITOR),)
-	ifeq ($(shell which runlim),)
-		_ := $(error $(NO_RUNLIM_ERR)))
-	endif
-	ifneq ($(MONID),)
-		MONPREFIX=$(MONID).
-	endif
-	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
-endif
+include runlim.mk
 
 %.checked:
 	$(call msg, "CHECK", $(basename $(notdir $@)))

diff --git a/lib/steel/pulse/Makefile b/lib/steel/pulse/Makefile
@@ -10,17 +10,7 @@ FSTAR_FILES:=$(wildcard *.fst *.fsti)
 
 FSTAR_OPTIONS=$(OTHERFLAGS) --cache_checked_modules --warn_error @241 --already_cached '*,-Pulse' --include ..
 
-# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
-# information about the time and space taken by each F* invocation.
-ifneq ($(RESOURCEMONITOR),)
-	ifeq ($(shell which runlim),)
-		_ := $(error $(NO_RUNLIM_ERR)))
-	endif
-	ifneq ($(MONID),)
-		MONPREFIX=$(MONID).
-	endif
-	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
-endif
+include ../runlim.mk
 
 MY_FSTAR=$(RUNLIM) $(FSTAR) $(SIL) $(FSTAR_OPTIONS)
 

diff --git a/lib/steel/runlim.mk b/lib/steel/runlim.mk
@@ -0,0 +1,11 @@
+# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
+# information about the time and space taken by each F* invocation.
+ifneq ($(RESOURCEMONITOR),)
+	ifeq ($(shell which runlim),)
+		_ := $(error $(NO_RUNLIM_ERR)))
+	endif
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
+endif