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

Duplicated docstrings in instantiations with `where` #1723

Closed yav closed 3 months ago

yav commented 3 months ago

Consider the following example:

/**                                                                                 

"F"

*/                                                                               
submodule F where                                                                
  parameter n: [8]                                                               

/**                                                                              

"M"

*/                                                                               
submodule M = submodule F where n = 2    

Checking the docstrings results in:

Cryptol> :l Test.cry 
Loading module Cryptol
Loading module Main
Main> :check-docstrings 

Checking Main

Checking submodule Main::`where` argument of M::n

Checking submodule Main::M::`parameter` interface of F::n

Checking submodule Main::`where` argument of M

"M"
[0x4d]

Checking submodule Main::M

"M"
[0x4d]

Checking submodule Main::`parameter` interface of F

"F"
[0x46]

Successes: 3, No fences: 3, Failures: 0

It looks like the docstring on the instantiation is also put on the anyonmous module used for the instantiation, but we should probably not do that.