Initial implementation of check docstrings from python

[glguy]

Check-point: docstrings can be checked from python

At a minimum work remains to update the documentation strings for this feature.

[weaversa]

Do you envision the timeout being for the entire check, or a timeout for each individual check in scope? If you're undecided, let me suggest the timeout should apply to each individual check. By this I mean that if a module has 10 checks, and we run check_docstrings with a timeout of 1 second, each check that takes less than 1 second should succeed, and the rest fail, but all checks should be attempted.

[glguy]

Do you envision the timeout being for the entire check, or a timeout for each individual check in scope? If you're undecided, let me suggest the timeout should apply to each individual check. By this I mean that if a module has 10 checks, and we run check_docstrings with a timeout of 1 second, each check that takes less than 1 second should succeed, and the rest fail, but all checks should be attempted.

Your idea makes sense. I'll take a look. I need to see how timeouts would interact with external solvers and their state but it seems like something we should be able to account for.

[WeeknightMVP]

Do you envision the timeout being for the entire check, or a timeout for each individual check in scope? If you're undecided, let me suggest the timeout should apply to each individual check. By this I mean that if a module has 10 checks, and we run check_docstrings with a timeout of 1 second, each check that takes less than 1 second should succeed, and the rest fail, but all checks should be attempted.

Because different verification commands take different times for different configurations, automated testing and other use cases for :check-docstrings would benefit from configuring a timeout for a given verification command or group thereof. This could be specified as a (not currently supported) REPL configuration setting...

module TimeoutExample where

import Primitive::Symmetric::Cipher::Block::DES (DES)

/**
 * DES correctly recovers plaintext encrypted with the same shared key.
 * 
 * ```
 * :set timeout=5.0  // takes about 2.0s in my workspace
 * :set prover=abc
 * :prove DESCorrect
 * ```
 */
property DESCorrect key msg = DES.decrypt key (DES.encrypt key msg) == msg

...or perhaps stored in a database of verification results and adapted based on completion time.