Skip to content

Commit 69eb286

Browse files
fix check-profile (#1576)
#1500 broke the profiling CI, this fixes it I think
1 parent db4cc9d commit 69eb286

File tree

1 file changed

+7
-8
lines changed

1 file changed

+7
-8
lines changed

Makefile

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ MDBOOK_SRC := $(MDBOOK_DIR)/src
1515
# Base directory where Agda interface files are stored
1616
AGDA_BUILD := _build
1717
# Agda profiling directory
18-
AGDA_PROFILING_TEMP := temp
19-
AGDA_PROFILING_OUTPUT := $(AGDA_PROFILING_TEMP)/typecheck_output.txt
18+
TEMP_DIR := temp
19+
AGDA_PROFILING_OUTPUT := $(TEMP_DIR)/typecheck_output.txt
2020
# Docs
2121
DOCS_DIR := docs
2222
TABLES_DIR := $(DOCS_DIR)/tables
@@ -100,10 +100,9 @@ check: ./$(SOURCE_DIR)/everything.lagda.md
100100
${TIME} ${AGDA} $?
101101

102102
.PHONY: check-profile
103-
# `clean` is specified second so that the $< variable stores the everything file.
104-
# We don't mind, because the `clean` target busts the typechecking and website cache,
105-
# but doesn't touch the everything file.
106-
check-profile: ./$(SOURCE_DIR)/everything.lagda.md clean
103+
check-profile: $(SOURCE_DIR)/everything.lagda.md
104+
@# Remove cached build data
105+
@rm -Rf ./$(AGDA_BUILD)/
107106
${AGDA} ${AGDAPROFILEFLAGS} $<
108107

109108
# Convert module path to directory path (replace dots with slashes)
@@ -125,7 +124,7 @@ profile-module:
125124
@find ./$(AGDA_BUILD) -type f -path "*/agda/$(SOURCE_DIR)/$(MODULE_DIR).agdai" -exec rm -f {} \+ 2>/dev/null || \
126125
echo "\033[0;31m$(AGDA_BUILD) directory does not exist, skipping deletion of interface files.\033[0m"
127126
@# Ensure the temporary directory exists
128-
@mkdir -p ./$(AGDA_PROFILING_TEMP)
127+
@mkdir -p ./$(TEMP_DIR)
129128
@# Profile typechecking the module and capture the output in the temp directory, also display on terminal
130129
@echo "\033[0;32mProfiling typechecking of $(MODULE)\033[0m"
131130
@$(AGDA) $(PROFILE_MODULE_AGDA_ARGS) $(SOURCE_DIR)/$(MODULE_DIR).lagda.md 2>&1 | tee ./$(AGDA_PROFILING_OUTPUT)
@@ -204,7 +203,7 @@ clean-website:
204203

205204
.PHONY: clean
206205
clean: clean-website
207-
@rm -Rf ./$(AGDA_BUILD)/ ./$(AGDA_PROFILING_TEMP)/ ./$(SOURCE_DIR)/everything.lagda.md ./$(SCRIPTS_DIR)/__pycache__
206+
@rm -Rf ./$(AGDA_BUILD)/ ./$(TEMP_DIR)/ ./$(SOURCE_DIR)/everything.lagda.md ./$(SCRIPTS_DIR)/__pycache__
208207

209208
.PHONY: pre-commit
210209
pre-commit:

0 commit comments

Comments
 (0)