As well as passing a one-look review, code in PhyslibAlpha has to pass a number of linters which we describe in this file.
lake exe runPhyslibAlphaLinters
This picks up things like lack of doc-strings on definitions, or incompatible @[simp] attributes.
./scripts/PhyslibAlpha/alphaFileImports.py
This checks that all PhyslibAlpha files are included in the file PhyslibAlpha.lean,
even if commented out based out with info of the commit where they broke.
./scripts/PhyslibAlpha/noAlphaImports.py
This checks that no file in ./Physlib or ./QuantumInfo imports a file from ./PhyslibAlpha.
./scripts/PhyslibAlpha/alphaPythonLinters.sh
Checks things like line length, simps which are not simp only or final tactics.