Support dependent types in variable
#815
GitHub Actions / junit-tests
failed
Dec 27, 2024 in 0s
56 tests run, 55 passed, 0 skipped, 1 failed.
Annotations
Check failure on line 48 in cli-impl/src/test/java/org/aya/test/TestRunner.java
github-actions / junit-tests
TestRunner.negative()
org.opentest4j.AssertionFailedError: ScopeError.txt ==> expected: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
3 │ def one => zero
│ ╰──╯
Error: The unqualified name `zero` is ambiguous
Did you mean:
`Nat1::zero`
`Nat2::zero`
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Error: The name `zero` being exported clashes with another exported definition
with the same name
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->
1 │ inductive Nat | zero | suc Nat
2 │ def one => suc zero
│ ╰─╯
Error: The name `suc` is not defined in the current scope
Did you mean: `Nat::suc`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->
2 │ module A { def foo => true }
3 │ open A
4 │ def foo => false
│ ╰─╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->
2 │ module A { def foo => true }
3 │ open A using (foo as bruh)
4 │ open A using (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->
2 │ module A { def foo => true }
3 │ open A hiding (foo)
4 │ open A hiding (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->
2 │ module A { def foo => true }
3 │ def foo => false
4 │ open A
│ ╰╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->
1 │ inductive Z : Type
2 │ | zero
3 │ | zero
│ ╰──╯
Error: The name zero (`zero`) is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ prim I prim I
│ ╰╯
Error: Redefinition of primitive `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim Path
│ ╰──╯
Error: The primitive `Path` depends on undeclared primitive(s): `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim senpaiSuki
│ ╰────────╯
Error: Unknown primitive `senpaiSuki`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->
1 │ open inductive Nat : Type | zero
2 │ def p => Nat::suc Nat::zero
│ ╰──────╯
Error: The qualified name `Nat::suc` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
LetOpen:
That looks right!
UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->
1 │ open import arith::bool::base
2 │ def b => true
3 │ def p (a : Bool) : Bool elim b
│ ╰╯
Error: The name `b` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
GeneralizedDisallowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:7 ->
1 │ variable A : Type
2 │ def test Type : Type
3 │ | _ => A
│ ╰╯
Error: The generalized variable `A` is not available here
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->
1 │ module A {}
2 │ module A {}
│ ╰╯
Error: The module name `A` is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->
1 │ import hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not found
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ open hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Warning: The name `t` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Error: The name `t` being exported clashes with another exported definition with
the same name
Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.
UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->
1 │ open class Cls | A : Type
2 │ def test (c : Cls) => c.B
│ ╰╯
Error: Unknown member `B` projected
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
> but was: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
3 │ def one => zero
│ ╰──╯
Error: The unqualified name `zero` is ambiguous
Did you mean:
`Nat1::zero`
`Nat2::zero`
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Error: The name `zero` being exported clashes with another exported definition
with the same name
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->
1 │ inductive Nat | zero | suc Nat
2 │ def one => suc zero
│ ╰─╯
Error: The name `suc` is not defined in the current scope
Did you mean: `Nat::suc`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->
2 │ module A { def foo => true }
3 │ open A
4 │ def foo => false
│ ╰─╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->
2 │ module A { def foo => true }
3 │ open A using (foo as bruh)
4 │ open A using (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->
2 │ module A { def foo => true }
3 │ open A hiding (foo)
4 │ open A hiding (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->
2 │ module A { def foo => true }
3 │ def foo => false
4 │ open A
│ ╰╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->
1 │ inductive Z : Type
2 │ | zero
3 │ | zero
│ ╰──╯
Error: The name zero (`zero`) is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ prim I prim I
│ ╰╯
Error: Redefinition of primitive `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim Path
│ ╰──╯
Error: The primitive `Path` depends on undeclared primitive(s): `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim senpaiSuki
│ ╰────────╯
Error: Unknown primitive `senpaiSuki`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->
1 │ open inductive Nat : Type | zero
2 │ def p => Nat::suc Nat::zero
│ ╰──────╯
Error: The qualified name `Nat::suc` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
LetOpen:
That looks right!
UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->
1 │ open import arith::bool::base
2 │ def b => true
3 │ def p (a : Bool) : Bool elim b
│ ╰╯
Error: The name `b` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
GeneralizedDisallowed:
Internal error
DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->
1 │ module A {}
2 │ module A {}
│ ╰╯
Error: The module name `A` is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->
1 │ import hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not found
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ open hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Warning: The name `t` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Error: The name `t` being exported clashes with another exported definition with
the same name
Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.
UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->
1 │ open class Cls | A : Type
2 │ def test (c : Cls) => c.B
│ ╰╯
Error: Unknown member `B` projected
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
>
Raw output
org.opentest4j.AssertionFailedError: ScopeError.txt ==> expected: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
3 │ def one => zero
│ ╰──╯
Error: The unqualified name `zero` is ambiguous
Did you mean:
`Nat1::zero`
`Nat2::zero`
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Error: The name `zero` being exported clashes with another exported definition
with the same name
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->
1 │ inductive Nat | zero | suc Nat
2 │ def one => suc zero
│ ╰─╯
Error: The name `suc` is not defined in the current scope
Did you mean: `Nat::suc`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->
2 │ module A { def foo => true }
3 │ open A
4 │ def foo => false
│ ╰─╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->
2 │ module A { def foo => true }
3 │ open A using (foo as bruh)
4 │ open A using (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->
2 │ module A { def foo => true }
3 │ open A hiding (foo)
4 │ open A hiding (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->
2 │ module A { def foo => true }
3 │ def foo => false
4 │ open A
│ ╰╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->
1 │ inductive Z : Type
2 │ | zero
3 │ | zero
│ ╰──╯
Error: The name zero (`zero`) is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ prim I prim I
│ ╰╯
Error: Redefinition of primitive `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim Path
│ ╰──╯
Error: The primitive `Path` depends on undeclared primitive(s): `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim senpaiSuki
│ ╰────────╯
Error: Unknown primitive `senpaiSuki`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->
1 │ open inductive Nat : Type | zero
2 │ def p => Nat::suc Nat::zero
│ ╰──────╯
Error: The qualified name `Nat::suc` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
LetOpen:
That looks right!
UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->
1 │ open import arith::bool::base
2 │ def b => true
3 │ def p (a : Bool) : Bool elim b
│ ╰╯
Error: The name `b` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
GeneralizedDisallowed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:7 ->
1 │ variable A : Type
2 │ def test Type : Type
3 │ | _ => A
│ ╰╯
Error: The generalized variable `A` is not available here
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->
1 │ module A {}
2 │ module A {}
│ ╰╯
Error: The module name `A` is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->
1 │ import hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not found
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ open hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Warning: The name `t` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Error: The name `t` being exported clashes with another exported definition with
the same name
Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.
UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->
1 │ open class Cls | A : Type
2 │ def test (c : Cls) => c.B
│ ╰╯
Error: Unknown member `B` projected
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
> but was: <DidYouMeanDisamb:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:30 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:8 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
│ ╰──╯
3 │ def one => zero
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:11 ->
1 │ private open inductive Nat1 | zero
2 │ private open inductive Nat2 | zero
3 │ def one => zero
│ ╰──╯
Error: The unqualified name `zero` is ambiguous
Did you mean:
`Nat1::zero`
`Nat2::zero`
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
ExportClashes:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:22 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` shadows a previous local definition from outer scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Warning: The name `zero` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:0 ->
1 │ open inductive Nat1 | zero
2 │ open inductive Nat2 | zero
│ ╰──╯
Error: The name `zero` being exported clashes with another exported definition
with the same name
Resolving interrupted due to:
1 error(s), 2 warning(s).
Let's learn from that.
DidYouMean:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:11 ->
1 │ inductive Nat | zero | suc Nat
2 │ def one => suc zero
│ ╰─╯
Error: The name `suc` is not defined in the current scope
Did you mean: `Nat::suc`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:4 ->
2 │ module A { def foo => true }
3 │ open A
4 │ def foo => false
│ ╰─╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
ImportUsing:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:14 ->
2 │ module A { def foo => true }
3 │ open A using (foo as bruh)
4 │ open A using (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportHiding:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:15 ->
2 │ module A { def foo => true }
3 │ open A hiding (foo)
4 │ open A hiding (bar)
│ ╰─╯
Error: The qualified name `A::bar` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportDefineShadow2:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:5 ->
2 │ module A { def foo => true }
3 │ def foo => false
4 │ open A
│ ╰╯
Warning: The name `foo` introduces ambiguity and can only be accessed through a
qualified name
That looks right!
Issue247:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:2 ->
1 │ inductive Z : Type
2 │ | zero
3 │ | zero
│ ╰──╯
Error: The name zero (`zero`) is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
RedefPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ prim I prim I
│ ╰╯
Error: Redefinition of primitive `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
PrimDeps:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim Path
│ ╰──╯
Error: The primitive `Path` depends on undeclared primitive(s): `I`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownPrim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ prim senpaiSuki
│ ╰────────╯
Error: Unknown primitive `senpaiSuki`
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
UnknownVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:9 ->
1 │ open inductive Nat : Type | zero
2 │ def p => Nat::suc Nat::zero
│ ╰──────╯
Error: The qualified name `Nat::suc` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
LetOpen:
That looks right!
UnknownElimVar:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:3:29 ->
1 │ open import arith::bool::base
2 │ def b => true
3 │ def p (a : Bool) : Bool elim b
│ ╰╯
Error: The name `b` is not defined in the current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
GeneralizedDisallowed:
Internal error
DuplicateModName:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:7 ->
1 │ module A {}
2 │ module A {}
│ ╰╯
Error: The module name `A` is already defined elsewhere
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImportNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:7 ->
1 │ import hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not found
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
OpenNoneExistMod:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:5 ->
1 │ open hopefullyThisModuleWillNeverExist
│ ╰───────────────────────────────╯
Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
current scope
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
DuplicateExport:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Warning: The name `t` introduces ambiguity and can only be accessed through a
qualified name
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:12 ->
2 │ module B { def t => Type }
3 │ public open A
4 │ public open B
│ ╰╯
Error: The name `t` being exported clashes with another exported definition with
the same name
Resolving interrupted due to:
1 error(s), 1 warning(s).
Let's learn from that.
UnknownProjMem:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:24 ->
1 │ open class Cls | A : Type
2 │ def test (c : Cls) => c.B
│ ╰╯
Error: Unknown member `B` projected
Resolving interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
>
at app//org.junit.jupiter.api.AssertionFailureBuilder.build(AssertionFailureBuilder.java:151)
at app//org.junit.jupiter.api.AssertionFailureBuilder.buildAndThrow(AssertionFailureBuilder.java:132)
at app//org.junit.jupiter.api.AssertEquals.failNotEqual(AssertEquals.java:197)
at app//org.junit.jupiter.api.AssertEquals.assertEquals(AssertEquals.java:182)
at app//org.junit.jupiter.api.Assertions.assertEquals(Assertions.java:1156)
at app//org.aya.test.TestRunner.checkOutput(TestRunner.java:76)
at app//org.aya.test.TestRunner.expectFixture(TestRunner.java:88)
at app//kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at app//kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:460)
at app//kala.collection.base.Traversable.forEachChecked(Traversable.java:976)
at app//org.aya.test.TestRunner.negative(TestRunner.java:48)
at java.base@22.0.2/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base@22.0.2/java.lang.reflect.Method.invoke(Method.java:580)
at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at app//org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base@22.0.2/java.util.ArrayList.forEach(ArrayList.java:1597)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base@22.0.2/java.util.ArrayList.forEach(ArrayList.java:1597)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at app//org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:124)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:99)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:94)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:63)
at java.base@22.0.2/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base@22.0.2/java.lang.reflect.Method.invoke(Method.java:580)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:92)
at jdk.proxy2/jdk.proxy2.$Proxy6.stop(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:200)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:132)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:103)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:63)
at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:121)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:71)
at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Loading