2.2 Running the compiler
Vortex includes a typechecker for Cecil. (Programs in languages other than Cecil are typechecked by their corresponding front-ends.) The typechecker has to be invoked explicitly by the typecheck or fulltypecheck commands; it isn't run when a make command is issued. fulltypecheck rechecks the whole program for type errors, while typecheck only rechecks code in modified files. typecheck is faster for small program changes, but it can miss errors that arise in files that were not touched.
The current typechecker implementation does not perform any "implementation-side" typechecking (checking whether signatures are fully and unambiguously implemented), but does perform most other, "client-side" typechecking. It also includes a few known bugs and weaknesses, where it may report some type errors unnecessarily.