Kwxm/metatheory/fix test2 #6414
Conversation
kwxm
added
Test
Metatheory
No Changelog Required
| deps = cmp.executableToolDepends; | ||
| in | ||
| ''PATH=${lib.makeBinPath deps}:$PATH''; | ||
|
|
||
| # FIXME: Somehow this is broken even with setting the path up as above |
There was a problem hiding this comment.
@zeme-wana I think this is what I have to remove to re-enable these tests in CI, but that's a guess. I'm also not sure what the stuff above about preCheck is for or whether we still need it.
There was a problem hiding this comment.
Yes, the test2->test-detailed came back and is passing.
As for the preCheck, I removed it and ci still passes, so it was probably obsolete.
|
This is issue #6406. |
…lutus into kwxm/metatheory/fix-test2
zeme-wana
force-pushed
the
kwxm/metatheory/fix-test2
branch
from
5411479
to
fda7740
Compare
…lutus into kwxm/metatheory/fix-test2
plutus-core/executables/plc/Main.hs
Outdated
| if printModeDeBruijn | ||
| then | ||
| let w = toDeBruijnTypePLC ty | ||
| in print (getPrintMethod printMode w) >> exitSuccess | ||
| else print (getPrintMethod printMode ty) >> exitSuccess |
There was a problem hiding this comment.
Does something like this make sense? Makes it a bit cleaner imo, but feel free to ignore if you don't agree/it doesn't work.
| if printModeDeBruijn | |
| then | |
| let w = toDeBruijnTypePLC ty | |
| in print (getPrintMethod printMode w) >> exitSuccess | |
| else print (getPrintMethod printMode ty) >> exitSuccess | |
| let transformNames = if printModeDeBruijn then toDeBruijnTypePLC else id | |
| in print (getPrintMethod printMode (transformNames ty)) >> exitSuccess |
There was a problem hiding this comment.
Unfortunately that doesn't work because ty and toDeBruijnTy ty have different types (the type of PLC types is parametric over the type of names, and toDebruijnType changes that). I think we'd have to introduce a new type class to get round that.
There was a problem hiding this comment.
I have tried to tidy it up a bit though.
There was a problem hiding this comment.
Looks great, thank you!
| @@ -104,7 +104,7 @@ printmode = option auto | |||
| <> showDefault | |||
| <> help | |||
| ("Print mode for textual output (ignored elsewhere): Classic -> plcPrettyClassicDef, " | |||
| <> "Debug -> plcPrettyClassicDebug, " | |||
| <> "Simple -> plcPrettyClassicSimple, " | |||
There was a problem hiding this comment.
The names changed in the prettyprinting code a while ago and plcPrettyClassicDebug no longer exists but the help message didn't get updated.
plutus-core/executables/uplc/Main.hs
Outdated
| @@ -67,6 +68,7 @@ data EvalOptions = | |||
| Input | |||
| Format | |||
| PrintMode | |||
| Bool -- Use de Bruijn indices in the output? | |||
There was a problem hiding this comment.
I personally think it's better to write a new datatype with 2 constructors something like ShowNames = UseDeBruijn | UseNames to avoid "boolean blindness"; it makes it possible to figure out from just the type/constructors what semantics they have, if you use booleans you have to add comments to maintain readability.
There was a problem hiding this comment.
You caught me! I did feel guilty about not doing that but I was too lazy to change it, partly because I would have had to go and look up the right way to deal with the command-line options. I'll change it.
plutus-metatheory:test2was disabled in CI and would fail if you ran it locally. This should fix the tests, after a fashion. Those tests (now renamed totest-detailed) run various Agda and Haskell evaluators on some examples and check that the evaluators agree. The problem was that the test was attempting to re-parse the output and compare ASTs, but the Agda evaluators can only output textual PLC/UPLC with names (often justAor something similar) annotated with de Bruijn indices, and the parsers can't handle those. To work around this I've modified theplcanduplcevaluators to be able to output textual code with de Bruijn indices as well and modified the tests to compare canonicalised versions of the textual output (squashing up all the whitespace and replacing variables with just their de Bruijn indices). This is kind of horrible, but it does work and saves us from having to worry about alpha equivalence.To fix it properly I think we'd either have to make the Haskell parser accept de Bruijn indices or get the Agda code to output unique names, and neither of these seem especially easy.I've also rewritten the tests to use Tasty.HUnit, which we use quite a lot elsewhere: previously they were using something called
detailed-0.9, which seems to be an obscure type of test suite that cabal knows about. I don't really know what that is, but I've been able to replace it withexitcode-stdio-1.0, which we use everywhere else.I messed about with
project.nixto try to re-enable the tests in CI, but I'm not sure if I've done that correctly.I also deleted some files in the top level of
plutus-metatheory/testthat appear to be unused.