search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 126 forks source link

check-docstrings and imports #1724

Open yav opened 3 months ago

yav commented 3 months ago

At the moment we don't run doc-strings on imported modules, but perhaps we should? Here's an example:


/**

"B"

*/
module B  where
  /* empty */

module A where
  import B

Running check-docstrings after loading A doesn't do anything.

Cryptol> :l A.cry 
Loading module Cryptol
Loading module B
Loading module A
A> :check-docstrings 

Checking A

Successes: 0, No fences: 1, Failures: 0
glguy commented 3 months ago

I think it only makes sense to recurse the import tree in the trivial examples. Often we'd have modules being defined because they are being used in multiple places. We could avoid rechecking this modules multiple times with caching, but that seems like working around bad design with a speed-hack. For a project with multiple top-level leaf modules you'd already need to manually enumerate what those top-level modules are. It seems more principled to have a list of the modules you that want to check which includes those that might be imported by other modules.