Skip to content

Commit 0471319

Browse files
nomeatanomeata
authored
chore: tests: use filenames as test names (#11302)
This PR renames the CTests tests to use filenames as test names. So instead of ``` 2080 - leanruntest_issue5767.lean (Failed) ``` we get ``` 2080 - tests/lean/run/issue5767.lean (Failed) ``` which allows Ctrl-Click’ing on them in the VSCode terminal.
1 parent 2e22c85 commit 0471319

File tree

1 file changed

+28
-14
lines changed

1 file changed

+28
-14
lines changed

‎src/shell/CMakeLists.txt‎

Lines changed: 28 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,8 @@ file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
6464
FOREACH(T ${LEANTESTS})
6565
if(NOT T MATCHES "\\.#")
6666
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
67-
add_test(NAME "leantest_${T_NAME}"
67+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
68+
add_test(NAME "${T_PATH}"
6869
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
6970
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
7071
endif()
@@ -75,7 +76,8 @@ file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean")
7576
FOREACH(T ${LEANRUNTESTS})
7677
if(NOT T MATCHES "\\.#")
7778
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
78-
add_test(NAME "leanruntest_${T_NAME}"
79+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
80+
add_test(NAME "${T_PATH}"
7981
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
8082
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
8183
endif()
@@ -86,7 +88,8 @@ file(GLOB LEANDOCEXS "${LEAN_SOURCE_DIR}/../doc/examples/*.lean")
8688
FOREACH(T ${LEANDOCEXS})
8789
if(NOT T MATCHES "\\.#")
8890
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
89-
add_test(NAME "leandocex_${T_NAME}"
91+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
92+
add_test(NAME "${T_PATH}"
9093
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples"
9194
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
9295
endif()
@@ -96,7 +99,8 @@ ENDFOREACH(T)
9699
file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
97100
FOREACH(T ${LEANCOMPTESTS})
98101
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
99-
add_test(NAME "leancomptest_${T_NAME}"
102+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
103+
add_test(NAME "${T_PATH}"
100104
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
101105
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
102106
ENDFOREACH(T)
@@ -113,7 +117,8 @@ file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
113117
FOREACH(T ${LEANINTERPTESTS})
114118
if(NOT EXISTS "${T}.no_interpreter")
115119
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
116-
add_test(NAME "leaninterptest_${T_NAME}"
120+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
121+
add_test(NAME "${T_PATH} (interpreted)"
117122
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
118123
COMMAND bash -c "${TEST_VARS} ./test_single_interpret.sh ${T_NAME}")
119124
endif()
@@ -125,15 +130,17 @@ file(GLOB LEANBENCHTESTS "${LEAN_SOURCE_DIR}/../tests/bench/*.lean.expected.out"
125130
FOREACH(T_OUT ${LEANBENCHTESTS})
126131
string(REPLACE ".expected.out" "" T ${T_OUT})
127132
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
128-
add_test(NAME "leanbenchtest_${T_NAME}"
133+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
134+
add_test(NAME "${T_PATH}"
129135
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
130136
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
131137
ENDFOREACH(T_OUT)
132138

133139
file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean")
134140
FOREACH(T ${LEANINTERPTESTS})
135141
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
136-
add_test(NAME "leanplugintest_${T_NAME}"
142+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
143+
add_test(NAME "${T_PATH}"
137144
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin"
138145
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
139146
ENDFOREACH(T)
@@ -142,7 +149,8 @@ ENDFOREACH(T)
142149
file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean")
143150
FOREACH(T ${LEANT0TESTS})
144151
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
145-
add_test(NAME "leant0test_${T_NAME}"
152+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
153+
add_test(NAME "${T_PATH}"
146154
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
147155
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
148156
ENDFOREACH(T)
@@ -152,7 +160,8 @@ file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
152160
FOREACH(T ${LEANPKGTESTS})
153161
if(EXISTS ${T}/test.sh)
154162
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
155-
add_test(NAME "leanpkgtest_${T_NAME}"
163+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
164+
add_test(NAME "${T_PATH}"
156165
WORKING_DIRECTORY "${T}"
157166
COMMAND bash -c "${TEST_VARS} ./test.sh")
158167
endif()
@@ -163,7 +172,8 @@ file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/server/*.lean")
163172
FOREACH(T ${LEANTESTS})
164173
if(NOT T MATCHES "\\.#")
165174
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
166-
add_test(NAME "leanservertest_${T_NAME}"
175+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
176+
add_test(NAME "${T_PATH}"
167177
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/server"
168178
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
169179
endif()
@@ -174,7 +184,8 @@ file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
174184
FOREACH(T ${LEANTESTS})
175185
if(NOT T MATCHES "\\.#" AND NOT T MATCHES "run.lean")
176186
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
177-
add_test(NAME "leaninteractivetest_${T_NAME}"
187+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
188+
add_test(NAME "${T_PATH}"
178189
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
179190
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
180191
endif()
@@ -185,7 +196,8 @@ file(GLOB_RECURSE LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/projec
185196
FOREACH(T ${LEANTESTS})
186197
if(NOT T MATCHES "\\.#")
187198
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
188-
add_test(NAME "leaninteractiveprojecttest_${T_NAME}"
199+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
200+
add_test(NAME "${T_PATH}"
189201
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive/projects"
190202
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T}")
191203
endif()
@@ -196,7 +208,8 @@ file(GLOB_RECURSE LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/docparse/*_[0-9][0
196208
FOREACH(T ${LEANTESTS})
197209
if(NOT T MATCHES "\\.#" AND NOT T MATCHES "run.lean")
198210
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
199-
add_test(NAME "leandocparsetest_${T_NAME}"
211+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
212+
add_test(NAME "${T_PATH}"
200213
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/docparse"
201214
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
202215
endif()
@@ -214,7 +227,8 @@ FOREACH(T ${LEANLAKETESTS})
214227
if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")
215228
GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
216229
GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)
217-
add_test(NAME "leanlaketest_${DIR_NAME}"
230+
CMAKE_PATH(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
231+
add_test(NAME "${T_PATH}"
218232
WORKING_DIRECTORY "${T_DIR}"
219233
COMMAND bash -c "
220234
set -eu

0 commit comments

Comments
 (0)