Skip to content

Instantly share code, notes, and snippets.

@brprice

brprice/gist:13058384f13291b6ce31bbfe3e8d17cd Secret

Created September 16, 2021 15:29
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save brprice/13058384f13291b6ce31bbfe3e8d17cd to your computer and use it in GitHub Desktop.
Save brprice/13058384f13291b6ce31bbfe3e8d17cd to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
On 15dbbd3112bf8b0d954a152d5807521d22bb2fe4 I got this failure
test/Test.hs
Tests
EvalFull
resume: FAIL (15.46s)
✗ resume failed at test/Tests/EvalFull.hs:371:5
after 96 tests, 20 shrinks and 771 discards.
┏━━ test/Tests/EvalFull.hs ━━━
352 ┃ hprop_resume :: Property
353 ┃ hprop_resume = withDiscards 1000 $
354 ┃ propertyWT (buildTypingContext defaultTypeDefs mempty NoSmartHoles) $ do
355 ┃ tds <- asks typeDefs
356 ┃ (dir, t, _, globs) <- genDirTmGlobs
357 ┃ n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here
┃ │ 6
358 ┃ (stepsFinal', sFinal) <- evalFullStepCount tds globs n dir t
359 ┃ when (stepsFinal' < 2) discard
360 ┃ let stepsFinal = case sFinal of Left _ -> stepsFinal'; Right _ -> 1 + stepsFinal'
361 ┃ m <- forAllT $ Gen.integral $ Range.constant 1 (stepsFinal - 1)
┃ │ 1
362 ┃ (stepsMid, sMid') <- evalFullStepCount tds globs m dir t
363 ┃ stepsMid === m
364 ┃ sMid <- case sMid' of
365 ┃ Left (TimedOut e) -> pure e
366 ┃ -- This should never happen: we know we are not taking enough steps to
367 ┃ -- hit a normal form (as m < stepsFinal)
368 ┃ Right e -> assert False >> pure e
369 ┃ (stepsTotal, sTotal) <- evalFullStepCount tds globs (stepsFinal - m) dir sMid
370 ┃ stepsMid + stepsTotal === stepsFinal'
371 ┃ set _ids' 0 sFinal === set _ids' 0 sTotal
┃ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
┃ │ ━━━ Failed (- lhs) (+ rhs) ━━━
┃ │ Left
┃ │ TimedOut
┃ │ Ann
┃ │ Meta 0 Nothing Nothing
┃ │ LAM
┃ │ Meta 0 Nothing Nothing
┃ │ "a2"
┃ │ App
┃ │ Meta 0 Nothing Nothing
┃ │ EmptyHole (Meta 0 Nothing Nothing)
┃ │ Letrec
┃ │ Meta 0 Nothing Nothing
┃ │ "a1"
┃ │ Lam
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a3"
┃ │ (Let
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a5"
┃ │ (Letrec
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a6"
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (TVar (Meta 0 Nothing Nothing) "a2")
┃ │ (EmptyHole (Meta 0 Nothing Nothing)))
┃ │ (EmptyHole (Meta 0 Nothing Nothing)))
┃ │ TEmptyHole (Meta 0 Nothing Nothing)
┃ │ Hole
┃ │ Meta 0 Nothing Nothing
┃ │ Letrec
┃ │ Meta 0 Nothing Nothing
┃ │ "a"
┃ │ LAM
┃ │ Meta 0 Nothing Nothing
┃ │ - "a72"
┃ │ + "a147"
┃ │ Let
┃ │ Meta 0 Nothing Nothing
┃ │ "a2"
┃ │ - Var (Meta 0 Nothing Nothing) "a72"
┃ │ + Var (Meta 0 Nothing Nothing) "a147"
┃ │ Let
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a4"
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (App
┃ │ (Meta 0 Nothing Nothing)
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (Letrec
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a1"
┃ │ (Lam
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a3"
┃ │ (Let
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a5"
┃ │ (Letrec
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a6"
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (TVar (Meta 0 Nothing Nothing) "a2")
┃ │ (EmptyHole (Meta 0 Nothing Nothing)))
┃ │ (EmptyHole (Meta 0 Nothing Nothing))))
┃ │ (TEmptyHole (Meta 0 Nothing Nothing))
┃ │ (Hole
┃ │ (Meta 0 Nothing Nothing) (Var (Meta 0 Nothing Nothing) "a"))))
┃ │ TEmptyHole (Meta 0 Nothing Nothing)
┃ │ Ann
┃ │ (Meta 0 Nothing Nothing)
┃ │ (LAM
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a2"
┃ │ (Let
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a4"
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (App
┃ │ (Meta 0 Nothing Nothing)
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (Letrec
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a1"
┃ │ (Lam
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a3"
┃ │ (Let
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a5"
┃ │ (Letrec
┃ │ (Meta 0 Nothing Nothing)
┃ │ "a6"
┃ │ (EmptyHole (Meta 0 Nothing Nothing))
┃ │ (TVar (Meta 0 Nothing Nothing) "a2")
┃ │ (EmptyHole (Meta 0 Nothing Nothing)))
┃ │ (EmptyHole (Meta 0 Nothing Nothing))))
┃ │ (TEmptyHole (Meta 0 Nothing Nothing))
┃ │ (Hole
┃ │ (Meta 0 Nothing Nothing) (Var (Meta 0 Nothing Nothing) "a"))))))
┃ │ (TEmptyHole (Meta 0 Nothing Nothing))
┃ │ TEmptyHole (Meta 0 Nothing Nothing)
┏━━ test/Tests/EvalFull.hs ━━━
423 ┃ genDirTmGlobs :: PropertyT WT (Dir, Expr, Type' (), M.Map ID Def)
424 ┃ genDirTmGlobs = do
425 ┃ dir <- forAllT $ Gen.element [Chk, Syn]
┃ │ Chk
426 ┃ (t', ty) <- case dir of
427 ┃ Chk -> do
428 ┃ ty' <- forAllT $ genWTType KType
┃ │ TFun
┃ │ ()
┃ │ (TEmptyHole ())
┃ │ (TFun
┃ │ ()
┃ │ (TEmptyHole ())
┃ │ (TApp
┃ │ () (TApp () (TEmptyHole ()) (TEmptyHole ())) (TEmptyHole ())))
429 ┃ t' <- forAllT $ genChk ty'
┃ │ Letrec
┃ │ ()
┃ │ "a"
┃ │ (LAM
┃ │ ()
┃ │ "a2"
┃ │ (Let
┃ │ ()
┃ │ "a4"
┃ │ (EmptyHole ())
┃ │ (App
┃ │ ()
┃ │ (EmptyHole ())
┃ │ (Letrec
┃ │ ()
┃ │ "a1"
┃ │ (Lam
┃ │ ()
┃ │ "a3"
┃ │ (Let
┃ │ ()
┃ │ "a5"
┃ │ (Letrec () "a6" (EmptyHole ()) (TVar () "a2") (EmptyHole ()))
┃ │ (EmptyHole ())))
┃ │ (TEmptyHole ())
┃ │ (Hole () (Var () "a"))))))
┃ │ (TEmptyHole ())
┃ │ (Var () "a")
430 ┃ pure (t', ty')
431 ┃ Syn -> forAllT genSyn
432 ┃ t <- generateIDs t'
433 ┃ globTypes <- asks globalCxt
434 ┃ let genDef i (n, defTy) =
435 ┃ (\ty' e -> Def {defID = i, defName = n, defType = ty', defExpr = e})
436 ┃ <$> generateTypeIDs defTy <*> (generateIDs =<< genChk defTy)
437 ┃ globs <- forAllT $ M.traverseWithKey genDef globTypes
┃ │ fromList []
438 ┃ pure (dir, t, ty, globs)
439 ┃
440 ┃ -- | Like '===' but specifically for expressions.
441 ┃ -- Ignores IDs, but remembers metadata (like cached types)
442 ┃ (~==) :: Expr -> Expr -> Assertion
This failure can be reproduced by running:
> recheck (Size 66) (Seed 3667079855370498646 17075026488463551245) resume
Use '--hedgehog-replay "Size 66 Seed 3667079855370498646 17075026488463551245"' to reproduce.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment