CakeML/cakeml

Lint theory names

Open

#602 opened on Jan 15, 2019

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Standard ML (98 forks)auto 404
dev experiencehelp wantedtooling

Repository metrics

Stars
 (1,169 stars)
PR merge metrics
 (PR metrics pending)

Description

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 Prog theory's program]
    • CompileProof [machine-code level proof for the corresponding Prog theory]

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).)

Contributor guide