Irrefutable Lambda #702
GitHub Actions / junit-tests
failed
Jan 17, 2025 in 0s
49 tests run, 45 passed, 0 skipped, 4 failed.
Annotations
Check failure on line 94 in cli-impl/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.testInMemoryAndPrim()
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]Raw output
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.tyck.tycker.Problematic.fail(Problematic.java:31)
at org.aya.resolve.salt.PatternBinParser.makeArg(PatternBinParser.java:80)
at org.aya.resolve.salt.PatternBinParser.makeArg(PatternBinParser.java:27)
at org.aya.util.binop.BinOpParser.makeBinApp(BinOpParser.java:180)
at org.aya.util.binop.BinOpParser.foldTopBinary(BinOpParser.java:163)
at org.aya.util.binop.BinOpParser.foldTop(BinOpParser.java:144)
at org.aya.util.binop.BinOpParser.convertToPrefix(BinOpParser.java:102)
at org.aya.util.binop.BinOpParser.build(BinOpParser.java:53)
at org.aya.resolve.salt.Desalt$Pat.apply(Desalt.java:121)
at org.aya.resolve.salt.Desalt$Pat.apply(Desalt.java:118)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.Pattern$Clause.lambda$descent$0(Pattern.java:214)
at org.aya.util.Arg.descent(Arg.java:36)
at org.aya.syntax.concrete.Pattern$Clause.lambda$descent$1(Pattern.java:214)
at kala.collection.immutable.ImmutableVectors$Vector1.map(ImmutableVectors.java:390)
at kala.collection.immutable.ImmutableVectors$Vector1.map(ImmutableVectors.java:180)
at org.aya.syntax.concrete.Pattern$Clause.descent(Pattern.java:214)
at org.aya.resolve.salt.Desalt.lambda$apply$1(Desalt.java:55)
at kala.collection.immutable.ImmutableSeqs$Seq1.map(ImmutableSeqs.java:306)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:55)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.Expr$Lambda.descent(Expr.java:183)
at org.aya.syntax.concrete.Expr$Lambda.descent(Expr.java:173)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:66)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.resolve.salt.Desalt.desugar(Desalt.java:113)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:64)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.stmt.decl.FnBody$ExprBody.map(FnBody.java:24)
at org.aya.syntax.concrete.stmt.decl.FnBody$ExprBody.map(FnBody.java:22)
at org.aya.syntax.concrete.stmt.decl.FnDecl.descentInPlace(FnDecl.java:48)
at org.aya.resolve.StmtResolvers.lambda$desugar$1(StmtResolvers.java:32)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:459)
at org.aya.resolve.StmtResolvers.desugar(StmtResolvers.java:32)
at org.aya.resolve.module.ModuleLoader.resolveModule(ModuleLoader.java:84)
at org.aya.resolve.module.ModuleLoader.resolveModule(ModuleLoader.java:66)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:76)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:26)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:26)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:89)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:383)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:369)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:459)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:1049)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:269)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:238)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:217)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:28)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:153)
at org.aya.test.LibraryTest.compile(LibraryTest.java:159)
at org.aya.test.LibraryTest.testInMemoryAndPrim(LibraryTest.java:94)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1597)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1597)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at 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/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/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 worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Check failure on line 55 in cli-impl/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.[1] success
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]Raw output
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.tyck.tycker.Problematic.fail(Problematic.java:31)
at org.aya.resolve.salt.PatternBinParser.makeArg(PatternBinParser.java:80)
at org.aya.resolve.salt.PatternBinParser.makeArg(PatternBinParser.java:27)
at org.aya.util.binop.BinOpParser.makeBinApp(BinOpParser.java:180)
at org.aya.util.binop.BinOpParser.foldTopBinary(BinOpParser.java:163)
at org.aya.util.binop.BinOpParser.foldTop(BinOpParser.java:144)
at org.aya.util.binop.BinOpParser.convertToPrefix(BinOpParser.java:102)
at org.aya.util.binop.BinOpParser.build(BinOpParser.java:53)
at org.aya.resolve.salt.Desalt$Pat.apply(Desalt.java:121)
at org.aya.resolve.salt.Desalt$Pat.apply(Desalt.java:118)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.Pattern$Clause.lambda$descent$0(Pattern.java:214)
at org.aya.util.Arg.descent(Arg.java:36)
at org.aya.syntax.concrete.Pattern$Clause.lambda$descent$1(Pattern.java:214)
at kala.collection.immutable.ImmutableVectors$Vector1.map(ImmutableVectors.java:390)
at kala.collection.immutable.ImmutableVectors$Vector1.map(ImmutableVectors.java:180)
at org.aya.syntax.concrete.Pattern$Clause.descent(Pattern.java:214)
at org.aya.resolve.salt.Desalt.lambda$apply$1(Desalt.java:55)
at kala.collection.immutable.ImmutableSeqs$Seq1.map(ImmutableSeqs.java:306)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:55)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.Expr$Lambda.descent(Expr.java:183)
at org.aya.syntax.concrete.Expr$Lambda.descent(Expr.java:173)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:66)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.resolve.salt.Desalt.desugar(Desalt.java:113)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:64)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.stmt.decl.FnBody$ExprBody.map(FnBody.java:24)
at org.aya.syntax.concrete.stmt.decl.FnBody$ExprBody.map(FnBody.java:22)
at org.aya.syntax.concrete.stmt.decl.FnDecl.descentInPlace(FnDecl.java:48)
at org.aya.resolve.StmtResolvers.lambda$desugar$1(StmtResolvers.java:32)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:459)
at org.aya.resolve.StmtResolvers.desugar(StmtResolvers.java:32)
at org.aya.resolve.module.ModuleLoader.resolveModule(ModuleLoader.java:84)
at org.aya.resolve.module.ModuleLoader.resolveModule(ModuleLoader.java:66)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:76)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:26)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:26)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:89)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:383)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:369)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:459)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:1049)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:269)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:238)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:217)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:28)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:153)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:96)
at org.aya.test.LibraryTest.compile(LibraryTest.java:155)
at org.aya.test.LibraryTest.compile(LibraryTest.java:151)
at org.aya.test.LibraryTest.testOnDisk(LibraryTest.java:55)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestTemplateMethod(TimeoutExtension.java:94)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:231)
at org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:209)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.execute(TestTemplateTestDescriptor.java:141)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.lambda$execute$3(TestTemplateTestDescriptor.java:109)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:194)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.accept(ForEachOps.java:184)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:1024)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:556)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:546)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:265)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:611)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:291)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1709)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:556)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:546)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:265)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:611)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:291)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:212)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1709)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:556)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:546)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:265)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:611)
at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:291)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1709)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:556)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:546)
at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:265)
at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:611)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.execute(TestTemplateTestDescriptor.java:109)
at org.junit.jupiter.engine.descriptor.TestTemplateTestDescriptor.execute(TestTemplateTestDescriptor.java:43)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1597)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1597)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at 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/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/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 worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Check failure on line 72 in cli-impl/src/test/java/org/aya/test/LibraryTest.java
github-actions / junit-tests
LibraryTest.testLiterate()
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]Raw output
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]
at org.aya.util.reporter.ThrowingReporter.report(ThrowingReporter.java:15)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.util.reporter.CountingReporter$Delegated.report(CountingReporter.java:63)
at org.aya.tyck.tycker.Problematic.fail(Problematic.java:31)
at org.aya.resolve.salt.PatternBinParser.makeArg(PatternBinParser.java:80)
at org.aya.resolve.salt.PatternBinParser.makeArg(PatternBinParser.java:27)
at org.aya.util.binop.BinOpParser.makeBinApp(BinOpParser.java:180)
at org.aya.util.binop.BinOpParser.foldTopBinary(BinOpParser.java:163)
at org.aya.util.binop.BinOpParser.foldTop(BinOpParser.java:144)
at org.aya.util.binop.BinOpParser.convertToPrefix(BinOpParser.java:102)
at org.aya.util.binop.BinOpParser.build(BinOpParser.java:53)
at org.aya.resolve.salt.Desalt$Pat.apply(Desalt.java:121)
at org.aya.resolve.salt.Desalt$Pat.apply(Desalt.java:118)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.Pattern$Clause.lambda$descent$0(Pattern.java:214)
at org.aya.util.Arg.descent(Arg.java:36)
at org.aya.syntax.concrete.Pattern$Clause.lambda$descent$1(Pattern.java:214)
at kala.collection.immutable.ImmutableVectors$Vector1.map(ImmutableVectors.java:390)
at kala.collection.immutable.ImmutableVectors$Vector1.map(ImmutableVectors.java:180)
at org.aya.syntax.concrete.Pattern$Clause.descent(Pattern.java:214)
at org.aya.resolve.salt.Desalt.lambda$apply$1(Desalt.java:55)
at kala.collection.immutable.ImmutableSeqs$Seq1.map(ImmutableSeqs.java:306)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:55)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.Expr$Lambda.descent(Expr.java:183)
at org.aya.syntax.concrete.Expr$Lambda.descent(Expr.java:173)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:66)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.resolve.salt.Desalt.desugar(Desalt.java:113)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:64)
at org.aya.resolve.salt.Desalt.apply(Desalt.java:24)
at org.aya.util.error.PosedUnaryOperator.apply(PosedUnaryOperator.java:16)
at org.aya.util.error.WithPos.descent(WithPos.java:25)
at org.aya.syntax.concrete.stmt.decl.FnBody$ExprBody.map(FnBody.java:24)
at org.aya.syntax.concrete.stmt.decl.FnBody$ExprBody.map(FnBody.java:22)
at org.aya.syntax.concrete.stmt.decl.FnDecl.descentInPlace(FnDecl.java:48)
at org.aya.resolve.StmtResolvers.lambda$desugar$1(StmtResolvers.java:32)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:459)
at org.aya.resolve.StmtResolvers.desugar(StmtResolvers.java:32)
at org.aya.resolve.module.ModuleLoader.resolveModule(ModuleLoader.java:84)
at org.aya.resolve.module.ModuleLoader.resolveModule(ModuleLoader.java:66)
at org.aya.cli.library.LibraryModuleLoader.load(LibraryModuleLoader.java:76)
at org.aya.resolve.module.CachedModuleLoader.lambda$load$0(CachedModuleLoader.java:26)
at kala.collection.mutable.MutableTreeMap.getOrPut(MutableTreeMap.java:483)
at org.aya.resolve.module.CachedModuleLoader.load(CachedModuleLoader.java:26)
at org.aya.resolve.module.ModuleLoader.load(ModuleLoader.java:89)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckOne(LibraryCompiler.java:383)
at org.aya.cli.library.LibraryCompiler$LibrarySccTycker.tyckSCC(LibraryCompiler.java:369)
at org.aya.util.tyck.OrgaTycker.tyckSCC(OrgaTycker.java:25)
at kala.function.CheckedConsumer.accept(CheckedConsumer.java:36)
at kala.collection.immutable.ImmutableVectors$Vector1.forEach(ImmutableVectors.java:459)
at kala.collection.base.Traversable.forEachChecked(Traversable.java:1049)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:269)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:238)
at org.aya.cli.library.LibraryCompiler.make(LibraryCompiler.java:217)
at org.aya.cli.utils.CompilerUtil.catching(CompilerUtil.java:28)
at org.aya.cli.library.LibraryCompiler.start(LibraryCompiler.java:153)
at org.aya.cli.library.LibraryCompiler.compile(LibraryCompiler.java:96)
at org.aya.test.LibraryTest.compile(LibraryTest.java:155)
at org.aya.test.LibraryTest.testLiterate(LibraryTest.java:72)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:767)
at org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:156)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
at org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
at org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$8(TestMethodTestDescriptor.java:217)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
at org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:156)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1597)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at java.base/java.util.ArrayList.forEach(ArrayList.java:1597)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:160)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:146)
at org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:144)
at org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:143)
at org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:100)
at org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at 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/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/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 worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Check failure on line 59 in cli-impl/src/test/java/org/aya/test/TestRunner.java
github-actions / junit-tests
TestRunner.negative()
org.opentest4j.AssertionFailedError: diff --git a/cli-impl/src/test/resources/negative/ParseError.txt b/cli-impl/src/test/resources/negative/ParseError.txt
index 1e18b50..67586c5 100644
--- a/cli-impl/src/test/resources/negative/ParseError.txt
+++ b/cli-impl/src/test/resources/negative/ParseError.txt
@@ -109,7 +109,18 @@ In file $FILE:4:4 ->
Error: Implicit elements in a list pattern is disallowed
-1 error(s), 0 warning(s).
+In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/relation/binary/path.aya:11:61 ->
+
+ 9 │ def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
+ 10 │
+ 11 │ def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
+ │ ╰╯
+
+Error: Unknown constructor
+ i
+
+Resolving interrupted due to:
+2 error(s), 0 warning(s).
Let's learn from that.
IncorrectReturn:
==> expected: <true> but was: <false>Raw output
org.opentest4j.AssertionFailedError: diff --git a/cli-impl/src/test/resources/negative/ParseError.txt b/cli-impl/src/test/resources/negative/ParseError.txt
index 1e18b50..67586c5 100644
--- a/cli-impl/src/test/resources/negative/ParseError.txt
+++ b/cli-impl/src/test/resources/negative/ParseError.txt
@@ -109,7 +109,18 @@ In file $FILE:4:4 ->
Error: Implicit elements in a list pattern is disallowed
-1 error(s), 0 warning(s).
+In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/relation/binary/path.aya:11:61 ->
+
+ 9 │ def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
+ 10 │
+ 11 │ def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
+ │ ╰╯
+
+Error: Unknown constructor
+ i
+
+Resolving interrupted due to:
+2 error(s), 0 warning(s).
Let's learn from that.
IncorrectReturn:
==> expected: <true> but was: <false>
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.AssertTrue.failNotTrue(AssertTrue.java:63)
at app//org.junit.jupiter.api.AssertTrue.assertTrue(AssertTrue.java:36)
at app//org.junit.jupiter.api.Assertions.assertTrue(Assertions.java:214)
at app//org.aya.test.TestRunner.negative(TestRunner.java:59)
at [email protected]/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at [email protected]/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 [email protected]/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 [email protected]/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 [email protected]/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at [email protected]/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