CakeML/cakeml

Lint theory names

开放

#602 创建于 2019年1月15日

 (1 条评论) (0 个反应) (0 位负责人)Standard ML (98 个派生)auto 404
dev experiencehelp wantedtooling

仓库指标

星标
 (1,169 个星标)
PR 合并指标
 (PR 指标待抓取)

描述

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

贡献者指南