dhess
commented
3 months ago Another one:
two interp agree: FAIL (5.57s)
--
| ✗ two interp agree failed at test/Tests/EvalFullInterp.hs:458:60
| after 752 tests, 3 shrinks and 580 discards.
| shrink path: 752/580:qA2
| both terminated 100% ███████████████████▉
| one failed to terminate 0% ····················
|
| ┏━━ test/Tests/Eval/Utils.hs ━━━
| 51 ┃ genDirTm :: PropertyT WT (Dir, Expr, Type' () ())
| 52 ┃ genDirTm = do
| 53 ┃ dir <- forAllT $ Gen.element @[] [Chk, Syn]
| ┃ │ Syn
| 54 ┃ (t', ty) <- case dir of
| 55 ┃ Chk -> do
| 56 ┃ ty' <- forAllT $ genWTType $ KType ()
| 57 ┃ t' <- forAllT $ genChk ty'
| 58 ┃ pure (t', ty')
| 59 ┃ Syn -> forAllT genSyn
| ┃ │ ( App
| ┃ │ ()
| ┃ │ (Let
| ┃ │ ()
| ┃ │ LocalName { unLocalName = "x" }
| ┃ │ (EmptyHole ())
| ┃ │ (App
| ┃ │ ()
| ┃ │ (Var
| ┃ │ ()
| ┃ │ (GlobalVarRef
| ┃ │ GlobalName
| ┃ │ { qualifiedModule =
| ┃ │ ModuleName { unModuleName = "Primitives" :\| [] }
| ┃ │ , baseName = "const"
| ┃ │ }))
| ┃ │ (EmptyHole ())))
| ┃ │ (EmptyHole ())
| ┃ │ , TCon
| ┃ │ ()
| ┃ │ GlobalName
| ┃ │ { qualifiedModule = ModuleName { unModuleName = "Builtins" :\| [] }
| ┃ │ , baseName = "Bool"
| ┃ │ }
| ┃ │ )
| 60 ┃ t <- generateIDs t'
| 61 ┃ pure (dir, t, ty)
|
| ┏━━ test/Tests/EvalFullInterp.hs ━━━
| 445 ┃ tasty_two_interp_agree :: Property
| 446 ┃ tasty_two_interp_agree = withTests 1000
| 447 ┃ $ withDiscards 2000
| 448 ┃ $ propertyWT testModules
| 449 ┃ $ do
| 450 ┃ let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
| 451 ┃ tds <- asks typeDefs
| 452 ┃ (dir, t, _ty) <- genDirTm
| 453 ┃ let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
| 454 ┃ let optsR = RunRedexOptions{pushAndElide = True}
| 455 ┃ (_, ss) <- failWhenSevereLogs $ evalFullStepCount @EvalLog UnderBinders optsV optsR tds globs 100 dir t
| 456 ┃ si <- liftIO (evalFullTest' (MicroSec 10_000) tds globs dir $ forgetMetadata t)
| 457 ┃ case (ss, si) of
| 458 ┃ (Right ss', Right si') -> label "both terminated" >> Hedgehog.diff (forgetMetadata ss') alphaEq si'
| ┃ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| ┃ │ ━━━ Failed (- lhs) (+ rhs) ━━━
| ┃ │ - Ann
| ┃ │ - ()
| ┃ │ - (EmptyHole ())
| ┃ │ - (TCon
| ┃ │ - ()
| ┃ │ - GlobalName
| ┃ │ - { qualifiedModule = ModuleName { unModuleName = "Builtins" :\| [] }
| ┃ │ - , baseName = "Bool"
| ┃ │ - })
| ┃ │ + App
| ┃ │ + ()
| ┃ │ + (App
| ┃ │ + ()
| ┃ │ + (Var
| ┃ │ + ()
| ┃ │ + (GlobalVarRef
| ┃ │ + GlobalName
| ┃ │ + { qualifiedModule =
| ┃ │ + ModuleName { unModuleName = "Primitives" :\| [] }
| ┃ │ + , baseName = "const"
| ┃ │ + }))
| ┃ │ + (EmptyHole ()))
| ┃ │ + (EmptyHole ())
| 459 ┃ _ -> label "one failed to terminate"
|
| This failure can be reproduced by running:
| > recheckAt (Seed 8128149785453899409 10689373616275667251) "752/580:qA2" two interp agree
|
| Use "--pattern '$NF ~ /two interp agree/' --hedgehog-replay '752/580:qA2 Seed 8128149785453899409 10689373616275667251'" to reproduce from the command-line.
|
| Use -p '/two interp agree/' to rerun this test only.
|
| 1 out of 854 tests failed (88.19s)Ref:
Raw logs:
Ref:
Raw logs: