From a36459511109c7867ddf80d3170c2f005773d02f Mon Sep 17 00:00:00 2001 From: Garmelon Date: Sat, 28 Feb 2026 04:05:07 +0100 Subject: [PATCH] chore: fix ci after new linter was added (#12733) The linter was running in parallel with other tests, which were creating and deleting files. Since the linter was iterating over some files and directories at the time, it crashed. --- tests/CMakeLists.txt | 5 +++++ tests/misc/lint.sh | 1 - 2 files changed, 5 insertions(+), 1 deletion(-) delete mode 100644 tests/misc/lint.sh diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index cca99712d7..72538abebd 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -405,6 +405,11 @@ foreach(T ${LEANLAKETESTS}) endif() endforeach(T) +# Lint test suite and parts of the repository. +# Must not run in parallel with any other tests that may create or delete files. +add_test(NAME lint.py COMMAND python lint.py WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}") +set_tests_properties(lint.py PROPERTIES RUN_SERIAL TRUE) + add_test_pile(compile *.lean BENCH PART2) add_test_pile(compile_bench *.lean BENCH PART2) add_test_pile(elab *.lean) diff --git a/tests/misc/lint.sh b/tests/misc/lint.sh deleted file mode 100644 index 2b95731435..0000000000 --- a/tests/misc/lint.sh +++ /dev/null @@ -1 +0,0 @@ -python "$TEST_DIR/lint.py"