dev experiencehelp wantedtooling
Repository-Metriken
- Stars
- (1.169 Sterne)
- PR-Merge-Metriken
- (PR-Metriken ausstehend)
Beschreibung
This issue is to add checks on theory name conventions to the linter (implemented as pat of readme_gen). In particular, the following conventions should be followed for theory names:
- lowercase letters and underscores only
- the following suffixes as exceptions to the rule above
- Proof [proofs about the corresponding suffix-less theory's definitions]
- Lang [definition of an intermediate language]
- Sem [semantics of an intermediate language]
- Props [auxiliary properties and proofs for an intermediate language or compiler pass]
- Prog [construction of a deeply embedded program and its verification]
- Compile [in-logic compilation of the corresponding
Progtheory's program] - CompileProof [machine-code level proof for the corresponding
Progtheory]
Optionally, we could also check that whenever a Proof exists, a corresponding suffix-less theory exists, and similar checks for other requirements for suffixed theories, including their location in the directory tree.
(In future, this linting could be used to enforce a CakeML-wide theory suffix/prefix (to avoid clashes with other developments).)