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

貢獻者指南