Skip to content

Manually regenerating regression tests with a custom built frontend

Jump to bottom
ana-pantilie edited this page Oct 25, 2021 · 1 revision

Overview of our test suite

This repository contains the following types of tests:

  1. tests written in Haskell, in kore/test, which we usually refer to as unit tests, even though many of them test multiple functionalities together
  2. K tests, in test, where the backend is tested against minimized K programs/specs
  3. kore tests, in test/regression-...; these are full semantics tests, imported from downstream projects

We usually refer to (2) and (3) as integration tests, since they also depend on the K frontend and on different projects which use K.

Sometimes, when talking about regression tests we refer to specifically (3).

Generating the kore for the regression tests

This is usually done automatically: there is a weekly update job which runs during the weekend and updates the files using the current deps/k_release.

There are scenarios where this update needs to be done manually: this most likely means the frontend has undergone a breaking change and we need to stop supporting the old frontend in the backend, but the frontend requires being built with a modified src/main/kore/prelude.kore, which lives in the backend's repository.

An example would be: the encoding of equations has changed, meaning that the frontend generates the kore for equations differently. The backend should support this new encoding, and remove support for the old one. The prelude.kore file contains equations which need to be manually rewritten in the new encoding. See PR 2890 which removes the support for the old equation encoding.

Steps for regenerating the regression tests with a custom-built frontend:

  1. Change prelude.kore accordingly, commit and push to a branch
  2. Clone https://github.com/kframework/k and switch to the branch associated to the release in use by the backend
  3. In K's submodule of the backend, checkout the branch with the modified prelude.kore
  4. Build K and add to path
  5. In the root of the backend repository, run scripts/generate-regression-tests.sh
  6. If the script succeeds, commit and push the changes to the regression tests
Clone this wiki locally