Skip to content

add --save-bfq-on-error flag for liquidhaskell and include it in CI#2648

Open
kaf-lamed-beyt wants to merge 5 commits intoucsd-progsys:developfrom
kaf-lamed-beyt:collect-bfq
Open

add --save-bfq-on-error flag for liquidhaskell and include it in CI#2648
kaf-lamed-beyt wants to merge 5 commits intoucsd-progsys:developfrom
kaf-lamed-beyt:collect-bfq

Conversation

@kaf-lamed-beyt
Copy link
Copy Markdown

i'm not sure how to pass the --save-bfq-on-error through the LH plugin test pipeline like you (@facundominguez) did in the previous PR. the extraOpts in Build.hs goes to cabal build, not to individual test executables.

i'm not sure how to pass the `--save-bfq-on-error` through the LH plugin test pipeline like you (@
facundominguez) did in the previous PR. the `extraOpts` in `Build.hs` goes to cabal build, not to individual test executables.
@kaf-lamed-beyt
Copy link
Copy Markdown
Author

kaf-lamed-beyt commented Apr 1, 2026

@facundominguez, can you take a look at this?

i'll follow up with the other PRs addressing points 2 and 3 in #2020 once this is clear.

@facundominguez
Copy link
Copy Markdown
Collaborator

Hello @kaf-lamed-beyt. Thanks for the PR!
Passing options to the Liquid Haskell plugin requires special GHC flags [link].

Probably, it should go in tests/tests.cabal.

@kaf-lamed-beyt
Copy link
Copy Markdown
Author

oh alright, i'll check this out.

thank you, @facundominguez!

@kaf-lamed-beyt
Copy link
Copy Markdown
Author

@facundominguez, let me know how it looks now.

-fkeep-going
-O0
-no-link
-fplugin-opt=LiquidHaskell:--save-bfq-on-error
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @kaf-lamed-beyt.

I guess we don't want to pass this flag to tests that are expected to fail. They are in testsuite with names containing the neg infix, and there is the errors testsuite.

Perhaps we could use a common stanza for negative tests:

common ghc-options-for-negated-tests
    ghc-options: -fplugin-opt=LiquidHaskell:--save-bfq-on-error
...
executable errors
    import:           common-ghc-options, ghc-options-for-negated-tests
    ...
...

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah, i see. that's much better. lemme find the neg infixes.

@kaf-lamed-beyt
Copy link
Copy Markdown
Author

@facundominguez, i've just updated it now. let me know how it looks. thank you.

@facundominguez
Copy link
Copy Markdown
Collaborator

Thanks @kaf-lamed-beyt! Something is amiss with the CI jobs. Otherwise, the changes look good to me.

@kaf-lamed-beyt
Copy link
Copy Markdown
Author

hmmm... i think there's a merge conflict in liquid-fixpoint. i'll try attending to that and see if it resolves it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants