lean4-htt/tests
Sebastian Ullrich 1efd6657d4
test: unflakify test cases (#4940)
With the recent unification of server and cmdline processing,
`IO.Process` tests that previously broke the server because they
directly wrote to stdout are now flaky on the cmdline because
elaboration and reporting are happening in separate threads. By removing
direct writes to stdout, the race condition is removed and the file can
actually be edited in the language server as well again.
2024-08-07 09:34:29 +00:00
..
bench chore: reduce stack space usage at instantiate_mvars_fn (#4931) 2024-08-06 17:38:59 +00:00
compiler chore: fix tests 2024-06-19 20:21:34 +02:00
elabissues
ir
lean test: unflakify test cases (#4940) 2024-08-07 09:34:29 +00:00
pkg feat: accept user-defined options on the cmdline (#4741) 2024-08-02 12:24:56 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain