From 4b7fbb037133ddeaf187c1ba95dc891b406c6950 Mon Sep 17 00:00:00 2001 From: Niklas Larsson Date: Fri, 12 Jun 2020 12:46:19 +0200 Subject: [PATCH] Fix overly nitpicky reflection test See #287 --- tests/idris2/reflection003/expected | 10 +++++----- tests/idris2/reflection003/refprims.idr | 8 +++++++- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 34042f6d7..0004f2e74 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -5,11 +5,11 @@ LOG 0: Name: Prelude.Strings.++ LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String)) LOG 0: Resolved name: Prelude.Nat LOG 0: Constructors: [Prelude.Z, Prelude.S] -refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1: +refprims.idr:43:10--45:1:While processing right hand side of dummy1 at refprims.idr:43:1--45:1: Error during reflection: Not really trying -refprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1: +refprims.idr:46:10--48:1:While processing right hand side of dummy2 at refprims.idr:46:1--48:1: Error during reflection: Still not trying -refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1: +refprims.idr:49:10--51:1:While processing right hand side of dummy3 at refprims.idr:49:1--51:1: Error during reflection: Undefined name -refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1: -Error during reflection: failed after generating Main.{plus:6078} +refprims.idr:52:10--54:1:While processing right hand side of dummy4 at refprims.idr:52:1--54:1: +Error during reflection: failed after generating Main.{plus:XXXX} diff --git a/tests/idris2/reflection003/refprims.idr b/tests/idris2/reflection003/refprims.idr index 952258575..9fedc07b9 100644 --- a/tests/idris2/reflection003/refprims.idr +++ b/tests/idris2/reflection003/refprims.idr @@ -27,11 +27,17 @@ logBad logMsg 0 ("Constructors: " ++ show !(getCons n)) fail "Still not trying" +-- because the exact sequence number in a gensym depends on +-- the library and compiler internals we need to censor it so the +-- output won't be overly dependent on the exact versions used. +censorDigits : String -> String +censorDigits str = pack $ map (\c => if isDigit c then 'X' else c) (unpack str) + tryGenSym : Elab a tryGenSym = do n <- genSym "plus" ns <- inCurrentNS n - fail $ "failed after generating " ++ show ns + fail $ "failed after generating " ++ censorDigits (show ns) dummy1 : a dummy1 = %runElab logPrims