max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix ci after new linter was added (#12733)

Browse source 
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.
This commit is contained in:
Garmelon 2026-02-28 04:05:07 +01:00 • committed by GitHub
parent 08ab8bf7c3
commit a364595111
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/CMakeLists.txt
View file

@ -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)

1
tests/misc/lint.sh
View file

@ -1 +0,0 @@
python "$TEST_DIR/lint.py"