Skip to content

Update pyk testing harness#2438

Merged
rv-jenkins merged 13 commits intomasterfrom
update-pyk-tests
Feb 15, 2022
Merged

Update pyk testing harness#2438
rv-jenkins merged 13 commits intomasterfrom
update-pyk-tests

Conversation

@ehildenb
Copy link
Copy Markdown
Member

@ehildenb ehildenb commented Feb 14, 2022

Fixes: #2437

This PR overhauls the pyk testing harness completely. Concepts are drawn from here: #2437

In particular:

  • All definitions are kompiled in the same way, and in fact we find that one single Haskell-kompiled definition is enough for all our tests.
  • A new more generic way of running python unit tests is added, where you can specify which definitions or proofs you expect to be kompiled/emitted as json before that python unit test is run.
  • All of the defn-tests/ directory tests are now represented by defn_test.py, which makes use of the existing imp-verification/haskell build.
  • The file unit-test.py is renamed to unit_test.py, and listed in the generic python testing harness.
  • The two tests which exercise the command-line interface (kpyk ... graphviz ... and kpyk ... prove ...) are made to use imp-verification/haskell testing harness.
  • The test for converting coverage hashes from one semantics to another is removed, as that is only used perhaps in Polkadot semantics, and that project is not active anymore. That functionality probably needs a full rewrite anyway, so this is us officially "dropping" support for that feature (no longer maintaining it).

@rv-jenkins rv-jenkins merged commit db0a821 into master Feb 15, 2022
@rv-jenkins rv-jenkins deleted the update-pyk-tests branch February 15, 2022 14:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

pyk testing strategy

3 participants