search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

print SMT preamble to the logfile when constructing context + fix CircleCI #681

Closed clayrat closed 6 months ago

clayrat commented 6 months ago

While investigating https://github.com/ucsd-progsys/liquidhaskell/issues/2272 we've discovered that since https://github.com/ucsd-progsys/liquid-fixpoint/pull/641 the SMT preamble is no longer printed to the .smt2 logfile. This PR fixes that.

facundominguez commented 6 months ago

~Thanks @clayrat, could we have a test that fails without this fix as well?~

facundominguez commented 6 months ago

Ah, please, ignore my previous comment. This looks good as is.

ranjitjhala commented 6 months ago

@facundominguez should we remove the circleci thing? Not sure why its failing but seems to be subsumed by the rest?

facundominguez commented 6 months ago

I think we can drop the circleci job.

This job, however, was running liquid-fixpoint with the PLE interpreter on. If we are to continue testing the interpreter, we will need to run it elsewhere (maybe another github job).

clayrat commented 6 months ago

I think the error just means that we have to update the image version in .circleci/config.yml

facundominguez commented 6 months ago

I think the error just means that we have to update the image version in .circleci/config.yml

Yes. I don't feel strong about fixing the job vs dropping it.

ranjitjhala commented 6 months ago

@facundominguez do you recall why those interpreter tests are not just part of the regular stack/cabal test suite? @clayrat can you try to change this line https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/.circleci/config.yml#L7C14-L7C35

to say image: default ? Maybe that will work?

facundominguez commented 6 months ago

do you recall why those interpreter tests are not just part of the regular stack/cabal test suite?

I don't remember, but it is rerunning all tests with a different flag. If I had to guess, I'd say running a separate job was done to earn some parallelism. But the tests take only 30 seconds to run, so perhaps the parallelism is unjustified.

clayrat commented 6 months ago

@clayrat can you try to change this line develop/.circleci/config.yml#L7C14-L7C35 to say image: default ? Maybe that will work?

Yep, works now