Reorganize StrataTest/Languages/Core/ into Examples/ and Tests/#522
Reorganize StrataTest/Languages/Core/ into Examples/ and Tests/#522
Conversation
Move all files from Core/ directly and behavior-focused files from Core/Examples/ into a new Core/Tests/ directory. Feature showcase files remain in Core/Examples/. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
joscoh
left a comment
There was a problem hiding this comment.
Arguably PolymorphicDatatypeTest.lean, PolymorphicFunctionTest.lean, and RecursiveFunctionTests.lean could go in the Examples/ directory since they demonstrate how to use polymorphic functions, datatypes, and recursive functions, respectively. But they consist of several examples (unlike most in the Examples/ directory) and some parts are unit-test-like, so it's probably fine.
Indeed -- I thought those were noisy and not showcase-y enough for Examples/. We should probably add good representative examples in the Examples/ directory, and I'm hoping this separation will help us exercise judgement there. |
MikaelMayer
left a comment
There was a problem hiding this comment.
The file path for unit tests now contains 3 times the word Test. Reminds me of Dafny which had Tests/LitTests/LitTest .
I don't have a better alternative as I do like to see in my IDE that a file ends with Test as the path is not visible.
Summary
StrataTest/Languages/Core/into a newCore/Tests/subdirectoryCore/Examples/intoCore/Tests/(e.g.DatatypeTypingTests,IfElsePrecedenceTest,PrecedenceCheck, etc.)Core/Examples/(e.g.Min,Map,SimpleProc,Loops,FreeRequireEnsure,UnreachableAssert, etc.)StrataTestusesglobs = ["StrataTest.+"]so all files are auto-discovered🤖 Generated with Claude Code