Add certifier tests for UPLC simplifier test inputs #7034
Conversation
ana-pantilie
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ana-pantilie
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ana-pantilie
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ana-pantilie
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ana-pantilie
changed the title
ana-pantilie
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ana-pantilie
added
the
No Changelog Required
| \f g -> (\a -> f (g 1 0) (a 2)) (\x y -> g y x) |
There was a problem hiding this comment.
Any chance we could make the simplifier handle open terms? Chances are, sooner or later we're gonna end up supporting smart contracts with free variables in them (not as a feature, just not to pay the cost of ensuring the script is closed).
There was a problem hiding this comment.
I think this would need a bigger change in the metatheory, and hence warrants a bigger discussion.
| ] | ||
| $ fmap (uncurry goldenVsSimplified) testSimplifyInputs | ||
| <> | ||
| [ goldenVsCse "cse1" cse1 |
There was a problem hiding this comment.
Why not test the certifier on CSE?
There was a problem hiding this comment.
Great catch, I forgot to add those! I'll add them as part of a separate PR/issue.
| import: lang | ||
| visibility: public | ||
| default-language: Haskell2010 | ||
| default-extensions: CPP |
There was a problem hiding this comment.
Is this needed? I don't think CPP should be a default extension regardless
There was a problem hiding this comment.
Yes, when I moved the modules to a cabal library they weren't compiling because of this. Maybe a cabal test-suite has this extension turned on by default?
| Just result -> | ||
| assertBool "The certifier returned false." result | ||
| Nothing -> | ||
| assertFailure "The certifier exited with an error." |
There was a problem hiding this comment.
is there no information of the error at all when the certifier fails?
There was a problem hiding this comment.
is there no information of the error at all when the certifier fails?
You need the counter examples from #6957 :) They are still too big to present in this message. We could at least parse enough of the response to see which phase failed? Currently I don't think we parse the response at all - it is all done in Agda and only returns a boolean value to Haskell.
There was a problem hiding this comment.
Good idea, I'll open an issue for this.
| ... | nothing = | ||
| putStrLn "The certifier was unable to check the compilation. Please open a bug report at https://www.github.com/IntersectMBO/plutus." | ||
| ... | just (cert (proof a)) = just true | ||
| ... | just (cert (ce ¬p t b a)) = just false |
There was a problem hiding this comment.
Could we pull out the phase tag (t here) and return that as part of the result somehow? It would be useful for Ziyang's question above. I appreciate that we would then need a more complicated type...
ana-pantilie
temporarily deployed
to
github-pages
GitHub Actions
Inactive
Fixes https://github.com/IntersectMBO/plutus-private/issues/1535