ucsd-progsys/liquidhaskell

Collect bfq files in CI

Open

#2,020 opened on Jun 29, 2022

View on GitHub
 (4 comments) (0 reactions) (0 assignees)Haskell (1,306 stars) (157 forks)batch import
good first issue

Description

We found recently a failing job in CI which isn't reproducible if the job is retried. If we could collect the .bfq files of tests which fail in CI, we might have a better chance to reproduce them either locally or in CI.

.bfq files aren't the most portable but are the fastest to write, and at the moment are the only files guaranteed to be accepted as inputs to LF. We would have to see how much of an impact in test time they produce.

There are at least two possible solutions:

  1. I think the ideal would be to dump the .bfq files only when there is a verification error, and only if some flag (to be implemented) is enabled. When tests are expected to fail, we would need to provide a reversed flag, that only produces .bfq files if verification succeeds.
  2. The next best would be to produce only .bfq files on all tests, no matter if they failed or not. LH has a --save flag, but it produces a few other files besides .bfq. One task here would be to add a new flag to LH and LF to only produce .bfqs.

https://github.com/ucsd-progsys/liquidhaskell/issues/2020: Implements --save-bfq-on-error in liquid-fixpoint

Other pieces necessary for this issue are:

  • similar flag for liquid haskell.
  • simliar flag for liquid fixpoint and liquid haskell that produces bfq files on success (to use for negative tests).
  • using the flags in CI in the liquid haskell repo.

Contributor guide

Tech stack
None
Domain
ci cdtesting
Issue type
feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
4
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
3-5 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
stale
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
clear
Prerequisites
Basic Haskell knowledgeFamiliarity with liquidhaskellFamiliarity with liquid fixpointCI/CD concepts
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
25
Research direction
To implement this feature, start by reviewing the linked issue #2020 in liquid fixpoint to understand the proposed save bfq on error flag. In liquidhaskell, add a similar flag to dump .bfq files on verification errors or successes. Then, update the CI configuration (likely in .circleci/config.yml) to use these flags. The goal is to collect .bfq files only when needed to aid debugging. Engage with maintainers if the scope or approach needs clarification.