`copilot-theorem`: README mentions inexisting `Driver.hs`, `lightProver`

Description

copilot-theorem's README mentions a file Driver.hs that is not part of the library:

As an example, the following prover is used in Driver.hs:

and later

Some examples are in the examples folder. The Driver.hs contains the main function to run any example.

It also says that there are two provers: one based on Kind2, and one called lightProver. The latter no longer exists, but we do have a What4 module now.

These mentions should be adjusted or removed.

Type

Bug: incorrect documentation.

Additional context

None.

Requester

Max Fan (NASA)

Method to check presence of bug

Running a search through the tree brings up several mentions:

$ grep -nIHre 'Driver.hs'
copilot-theorem/README.md:205:As an example, the following prover is used in `Driver.hs`:
copilot-theorem/README.md:254:Some examples are in the *examples* folder. The `Driver.hs` contains the `main`
copilot-theorem/README.md:257:by changing one *import* directive in `Driver.hs`.

$ grep -nIHre 'lightProver'
copilot-theorem/README.md:79:prove (lightProver def) (check "gt0") spec
copilot-theorem/README.md:82:where `lightProver def` stands for the *light prover* with default
copilot-theorem/README.md:150:`lightProver :: Options -> Prover` function which builds a prover from a record
copilot-theorem/README.md:209:  lightProver def {onlyBmc = True, kTimeout = 5}

$ grep -nIHre '\<Light\>' | grep -ve 'XML'
copilot-theorem/README.md:71:  the `Copilot.Theorem.Light` and `Copilot.Theorem.Kind2` module.
copilot-theorem/README.md:123:Two provers are provided by default: `Light` and `Kind2`.
copilot-theorem/README.md:149:The *light prover* is defined in `Copilot.Theorem.Light`. This module exports the
copilot-theorem/README.md:399:#### The Light prover
copilot-theorem/README.md:402:basic *k-induction* algorithm [1]. The `Light` directory contains three files:

Expected result

The output of the above grep commands should be empty, indicating that that inexisting file/modules/functions are not mentioned.

Desired result

The output of the above grep commands should be empty, indicating that that inexisting file/modules/functions are not mentioned.

Proposed solution

The claims should be adjusted to match the existing file tree, modules and exports, either by updating the references to point to their current locations, or by removing the claims altogether.

Further notes

None.

Change Manager: Confirmed that the README is outdated and mentions in-existing functions, modules and files.

Technical Lead: Confirmed that the issue should be addressed.

I investigated these parts of copilot-theorem recently as well. I believe what the README refers to as lightProver has been superseded by the new kInduction prover, which is separate from the Kind2 and What4 provers. See also 976bc5f, which removes lightProver in favor of kInduction.

I have picked up fixing the README.

@RyanGlScott yes, it seems that lightProver has been superseded by kInduction (and the code has been refactored a bit since then). copilot-theorem is pretty much the only part of Copilot where I have nearly no knowledge about. What is the difference between kInduction:

copilot/copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs

Lines 110 to 116 in f823901

    
           kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal 
        
           kInduction opts backend = check P.Prover 
        
             { P.proverName  = "K-Induction" 
        
             , P.startProver = return . ProofState opts backend Map.empty . translateWithBounds 
        
             , P.askProver   = kInduction' (startK opts) (maxK opts) 
        
             , P.closeProver = const $ return () 
        
             }

and kind2Prover:

copilot/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs

Lines 44 to 49 in f823901

    
           kind2Prover :: Options -> Prover 
        
           kind2Prover opts = Prover 
        
             { proverName =  "Kind2" 
        
             , startProver  = return . ProverST opts . TS.translate 
        
             , askProver    = askKind2 
        
             , closeProver  = const $ return () }

Sounds like they solve the same problem with a different backend?

The README is rather outdated and incomplete, so maybe we just want to remove all parts mentioning lightProver and do a complete rewrite later on?

Sounds like they solve the same problem with a different backend?

Yes, that is my understanding as well.

Yeah, I think we may want to revisit and clean the library. @ivanperez-keera I propose we simply remove any obsolete information from the README, so that it is at least not plain incorrect about things. Later on we can investigate if kInduction and kind2Prover are actually equal, and deprecate one of them (in the end both are based on Yices). After this (and possibly other cleanup work) we can rewrite the README. What do you think?

@ivanperez-keera I have made a branch (master...fdedden:copilot:develop-fix-nonexisting-readme) that removes any mention to Driver.hs and the Light Prover. I have not tested the equivalence of the Light Prover with the k-induction prover yet, but it is a start. Let me know what you think.

BTW: I have seen numerous other typos and mistakes in the file, so it is in dire need of a cleanup.

Technical Lead: Issue scheduled for fixing in Copilot 3.20.

Fix assigned to: @fdedden .

Implementor: Solution implemented, review requested.

Change Manager: Verified that:

Solution is implemented:
- The code proposed compiles and passes all tests. Details:
  Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/270352630
- The solution proposed produces the expected result. Details:
  The change is to the README, so it's been evaluated by manual inspection. I checked some of the examples with kind2-0.7.2 to make sure they produce the expected results.
Implementation is documented. Details:
The change is to the documetnation.
Change history is clear.
Commit messages are clear.
Changelogs are updated.
Examples are updated. Details:
No updates needed.
Required version bumps are evaluated. Details:
Bump not needed. Changes affect README only.

Change Manager: Implementation ready to be merged.

	kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
	kInduction opts backend = check P.Prover
	{ P.proverName = "K-Induction"
	, P.startProver = return . ProofState opts backend Map.empty . translateWithBounds
	, P.askProver = kInduction' (startK opts) (maxK opts)
	, P.closeProver = const $ return ()
	}

	kind2Prover :: Options -> Prover
	kind2Prover opts = Prover
	{ proverName = "Kind2"
	, startProver = return . ProverST opts . TS.translate
	, askProver = askKind2
	, closeProver = const $ return () }