Description Checklist lake build StrataPython StrataPythonTest succeeds locally New .lean files start with the standard copyright header No trailing whitespace and files end with a newline