Skip to content

Commit

Permalink
update machine names for tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@andrevidela
andrevidela committed Jan 17, 2025
1 parent d1801f3 commit 26db84c
Show file tree
Hide file tree
Showing 7 changed files with 100 additions and 98 deletions.
14 changes: 7 additions & 7 deletions tests/idris2/basic/basic044/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,33 +117,33 @@ Target type : ({arg:1} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:3:
$resolved6
$resolved7
Target type : ?Vec.{a:4569}_[]
Target type : ?Vec.{a:4574}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4:
(($resolved3 ((:: (fromInteger 0)) Nil)) Nil)
(($resolved4 ((:: (fromInteger 0)) Nil)) Nil)
(($resolved5 ((:: (fromInteger 0)) Nil)) Nil)
Target type : (Vec.Vec ?Vec.{a:4569}_[] ?Vec.{n:4568}_[])
Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:5:
(($resolved3 (fromInteger 0)) Nil)
(($resolved4 (fromInteger 0)) Nil)
(($resolved5 (fromInteger 0)) Nil)
Target type : ?Vec.{a:4572}_[]
Target type : ?Vec.{a:4577}_[]
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
With default. Target type : ?Vec.{a:4574}_[]
With default. Target type : ?Vec.{a:4579}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7:
$resolved6
$resolved7
Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
Target type : (Vec.Vec ?Vec.{a:4579}_[] ?Vec.{n:4578}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
With default. Target type : ?Vec.{a:4573}_[]
With default. Target type : ?Vec.{a:4578}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8:
$resolved6
$resolved7
Target type : (Vec.Vec ?Vec.{a:4572}_[] ?Vec.{n:4571}_[])
Target type : (Vec.Vec ?Vec.{a:4577}_[] ?Vec.{n:4576}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:5:
(($resolved4 (fromInteger 0)) Nil)
Target type : (Prelude.Basics.List Prelude.Types.Nat)
Expand Down
2 changes: 2 additions & 0 deletions tests/idris2/data/record021/RecordParam.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@ record Ok (ty : Type) where
f : (x : ty) -> Type
record Fail (ty : Type) where
f : {x : ty} -> Type
record Fail2 (ty : Type) where
f : {x : ty} -> ty -> {y : ty} -> Type
2 changes: 1 addition & 1 deletion tests/idris2/error/error018/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7

1/1: Building Issue1031-4 (Issue1031-4.idr)
Error: While processing left hand side of nice. Unsolved holes:
Main.{dotTm:815} introduced at:
Main.{dotTm:820} introduced at:
Issue1031-4:4:6--4:10
1 | %default total
2 |
Expand Down
150 changes: 75 additions & 75 deletions tests/idris2/evaluator/evaluator002/expected
View file
Original file line number Diff line number Diff line change
@@ -1,89 +1,89 @@
1/2: Building Lib (Lib.idr)
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2554}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551}
LOG eval.stuck.outofscope:5: Stuck function: {_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2559}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556}
LOG eval.stuck.outofscope:5: Stuck function: {_:2561}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559}
LOG eval.stuck.outofscope:5: Stuck function: {_:2565}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2566}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564}
LOG eval.stuck.outofscope:5: Stuck function: {_:2570}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2571}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575}
LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2585}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586}
LOG eval.stuck.outofscope:5: Stuck function: {_:2589}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2590}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2590}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591}
LOG eval.stuck.outofscope:5: Stuck function: {_:2594}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598}
LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598}
LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux
2/2: Building Main (Main.idr)
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2612}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621}
LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601}
LOG eval.stuck.outofscope:5: Stuck function: Lib.accMap
Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux
LOG eval.stuck:5: Stuck function: Lib.accMapAux
Expand Down
6 changes: 3 additions & 3 deletions tests/idris2/evaluator/interpreter008/expected
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
1/1: Building Issue2041 (Issue2041.idr)
Error: Unsolved holes:
Main.{n:820} introduced at:
Main.{n:825} introduced at:
Issue2041:5:17--5:19
1 | ex : {n : Nat} -> String
2 | ex {n} = "hello" ++ show n
Expand All @@ -9,8 +9,8 @@ Issue2041:5:17--5:19
5 | main = putStrLn ex
^^

Main> Encountered unimplemented hole Main.{n:820}
Warning: compiling hole Main.{n:820}
Main> Encountered unimplemented hole Main.{n:825}
Warning: compiling hole Main.{n:825}
Main> Encountered unimplemented hole Main.{n:4}
Warning: compiling hole Main.{n:4}
Main>
Expand Down
18 changes: 9 additions & 9 deletions tests/idris2/interactive/interactive042/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,17 @@ Main> 0 m : Nat
------------------------------
help : Vect (S (plus n m)) a
Main> Main> a : Nat
eq : {a:822} = a
eq : {a:827} = a
------------------------------
a : Nat
Main> 0 m : Nat
0 a : Type
x : a
xs : Vect {n:871} a
xs : Vect {n:876} a
ys : Vect m a
0 n : Nat
------------------------------
help : Vect (S (plus {n:871} m)) a
help : Vect (S (plus {n:876} m)) a
Main>
Bye for now!
1/1: Building Issue35-2 (Issue35-2.idr)
Expand All @@ -39,10 +39,10 @@ Issue35-2:2:13--2:14

1/1: Building Issue35-2 (Issue35-2.idr)
Error: While processing right hand side of f. When unifying:
Either b {b:821}
Either b {b:826}
and:
Either {b:821} b
Mismatch between: {b:821} (implicitly bound at Issue35-2:2:1--2:2) and b.
Either {b:826} b
Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:2) and b.

Issue35-2:2:13--2:14
1 | f : { a, b : Type } -> Either a b -> Either b a
Expand All @@ -51,10 +51,10 @@ Issue35-2:2:13--2:14

1/1: Building Issue35-2 (Issue35-2.idr)
Error: While processing right hand side of f. When unifying:
Prelude.Either b {b:821}
Prelude.Either b {b:826}
and:
Prelude.Either {b:821} b
Mismatch between: {b:821} (implicitly bound at Issue35-2:2:1--2:2) and b.
Prelude.Either {b:826} b
Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:2) and b.

Issue35-2:2:13--2:14
1 | f : { a, b : Type } -> Either a b -> Either b a
Expand Down
6 changes: 3 additions & 3 deletions tests/idris2/misc/lazy003/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ Refers to: Builtin.Unit
Flags: covering
Main> Main.f6
Arguments []
Compile time tree: Delay (\u1, {u2:834} => u1)
Compiled: Delay Lazy (\u1=> \{u2:834}=> u1)
Compile time tree: Delay (\u1, {u2:839} => u1)
Compiled: Delay Lazy (\u1=> \{u2:839}=> u1)
Refers to: Builtin.Unit
Flags: covering
Main> Main.switch3
Expand All @@ -19,7 +19,7 @@ Compiled: \ {arg:0} => let f = Force Lazy (Main.switch {arg:0}) in
\{lamc:0}=> case {lamc:0} of
{ Builtin.MkPair {tag = 0} [cons] {e:2} {e:3} => case {e:3} of { Builtin.MkPair {tag = 0} [cons] {e:6} {e:7} => Builtin.MkPair {tag = 0} [cons] (f {e:2}) (Builtin.MkPair {tag = 0} [cons] (f {e:6}) (f {e:7}))}
}
Refers to: Main.case block in switch3, Main.{_:980}, Main.switch, Builtin.Pair, Prelude.Types.Nat
Refers to: Main.case block in switch3, Main.{_:985}, Main.switch, Builtin.Pair, Prelude.Types.Nat
Refers to (runtime): Main.switch, Builtin.MkPair
Flags: covering
Size change:
Expand Down

0 comments on commit 26db84c

Please sign in to comment.