lean4-htt/tests
Kim Morrison 3a457e6ad6
chore: use #guard_msgs in run tests (#4175)
Many of our tests in `tests/lean/run/` produce output from `#eval` (or
`#check`) statements, that is then ignored.

This PR tries to capture all the useful output using `#guard_msgs`. I've
only done a cursory check that the output is still sane --- there is a
chance that some "unchecked" tests have already accumulated regressions
and this just cements them!

In the other direction, I did identify two rotten tests:
* a minor one in `setStructInstNotation.lean`, where a comment says `Set
Nat`, but `#check` actually prints `?_`. Weird?
* `CompilerProbe.lean` is generating empty output, apparently indicating
that something is broken, but I don't know the signficance of this file.

In any case, I'll ask about these elsewhere.

(This started by noticing that a recent `grind` test file had an
untested `trace_state`, and then got carried away.)
2024-05-16 00:38:31 +00:00
..
bench chore: Nat.repr microbenchmark (#3888) 2024-04-17 18:10:32 +00:00
compiler fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
elabissues feat: add bitwise operations to reduceNat? and kernel (#3134) 2024-01-11 18:12:45 +00:00
ir feat: lake: GNU/BSD OS detection in test scripts (#3180) 2024-01-14 02:49:38 +00:00
lean chore: use #guard_msgs in run tests (#4175) 2024-05-16 00:38:31 +00:00
pkg feat: validate reducibility attribute setting (#4052) 2024-05-03 13:44:42 +00:00
playground chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508) 2024-03-04 23:56:30 +00:00
plugin fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
simpperf
.gitignore
common.sh fix: use -O3 for LLVM tests in common.sh 2023-11-02 23:21:47 +01:00
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00