Collect bfq files in CI · ucsd-progsys/liquidhaskell#2020

2022-06-29T12:32:00.000Z

We found recently a [failing job](https://app.circleci.com/pipelines/github/ucsd-progsys/liquidhaskell/1353/workflows/69ecdfe8-de27-48ec-b5cc-63e79bc198f6/jobs/7954) 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 `.bfq`s. ------------ 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.

(4 评论) (0 反应) (0 负责人)Haskell (1,306 star) (157 fork)batch import

good first issue

描述

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:

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.
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.

贡献者指南

技术栈: 无
领域: ci cdtesting
议题类型: feature
难度: 4
预计时间: 3-5 days
活动状态: stale
清晰度: clear
前置要求: Basic Haskell knowledgeFamiliarity with liquidhaskellFamiliarity with liquid fixpointCI/CD concepts
新手友好度: 25
研究方向: 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.