Where are copilot tests located?

[yaitskov]

Hi,

cabal package in ./copilot doesn't have a test folder nonetheless there is a runtest shell script.
Is it a legacy package?
If ./copilot-verifier has enough tests then why not merge ./copilot into the verifier or vice-versa?
How to use runtest?

[ivanperez-keera]

Copilot is divided into multiple packages, as you can see both at the top level of the repo in the multiple folders named copilot*, and in the package list on hackage.

The copilot package is a package that depends on several (but not all) libraries, which most users will depend on. The thinking is that, if your application or package depends on copilot, then you immediately have access to most of the constructs you'll need to create specifications and compile them to C99.

The copilot package itself does not have tests. Instead, the tests are in the packages that copilot depends on.

At this stage, we don't yet want to make the copilot package depend on copilot-verifier, because the latter has many dependencies, and many users won't need all of that machinery, but in principle, it could.

As for the runtest script, it's a vestige of an older version of Copilot. It could be removed, or renamed to copilot (as an executable). We've talked about creating a copilotc and copiloti wrappers around GHC to compile to a target language (C99, Bluespec) and to interpret a spec, respectively, but we are holding back on that because creating a GHC wrapper that exposes everything we might need might be a non-trivial task and create a sizeable burden that we may not have the resources to maintain well.