From 6e71cbe32b9b46b1e6554384ffcaae757ded412e Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Wed, 19 Jun 2024 02:15:23 -0400
Subject: [PATCH 1/2] build: do not explicitly set encoding

---
 build.gradle.kts                                             | 2 --
 cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java | 4 ++--
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/build.gradle.kts b/build.gradle.kts
index b8f87db0bb..b73f6a9836 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -97,7 +97,6 @@ subprojects {
     modularity.inferModulePath.set(true)
 
     options.apply {
-      encoding = "UTF-8"
       isDeprecation = true
       release.set(javaVersion)
       compilerArgs.addAll(listOf("-Xlint:unchecked", "--enable-preview"))
@@ -126,7 +125,6 @@ subprojects {
     options.addBooleanOption("-enable-preview", true)
     options.addStringOption("-source", javaVersion.toString())
     options.addStringOption("Xdoclint:none", "-quiet")
-    options.encoding("UTF-8")
     options.tags(
       "apiNote:a:API Note:",
       "implSpec:a:Implementation Requirements:",
diff --git a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java
index 616220dab0..1aa21ed522 100644
--- a/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java
+++ b/cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java
@@ -57,7 +57,7 @@ public record Message(
     @NotNull String successNotion,
     @NotNull String failNotion
   ) {
-    public static final Message EMOJI = new Message("\uD83D\uDC02\uD83C\uDF7A", "\uD83D\uDD28");
-    public static final Message ASCII = new Message("That looks right!", "What are you doing?");
+    public static final Message EMOJI = new Message("🎉", "🥲");
+    public static final Message ASCII = new Message("That looks right!", "Let's learn from that.");
   }
 }

From 8bc6de4a3f5771a4ee1615528d1b8c2b8ef76b1d Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Wed, 19 Jun 2024 02:46:33 -0400
Subject: [PATCH 2/2] test: update golden values

---
 .../test/resources/negative/ExprTyckError.txt | 22 +++++++-------
 .../test/resources/negative/GoalAndMeta.txt   | 12 ++++----
 .../test/resources/negative/OperatorError.txt | 10 +++----
 .../test/resources/negative/ParseError.txt    |  4 +--
 .../test/resources/negative/PatCohError.txt   | 20 ++++++-------
 .../test/resources/negative/PatTyckError.txt  | 28 ++++++++---------
 .../test/resources/negative/ScopeError.txt    | 30 +++++++++----------
 .../test/resources/negative/TerckError.txt    |  4 +--
 8 files changed, 65 insertions(+), 65 deletions(-)

diff --git a/cli-impl/src/test/resources/negative/ExprTyckError.txt b/cli-impl/src/test/resources/negative/ExprTyckError.txt
index 877a74c5e7..e145ed9633 100644
--- a/cli-impl/src/test/resources/negative/ExprTyckError.txt
+++ b/cli-impl/src/test/resources/negative/ExprTyckError.txt
@@ -13,7 +13,7 @@ Error: Cannot check the expression
          Nat
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 IllTypedApp:
 In file $FILE:2:22 ->
@@ -36,7 +36,7 @@ In file $FILE:2:4 ->
 Error: Unsolved meta _
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 WantButNo:
 In file $FILE:2:19 ->
@@ -51,7 +51,7 @@ Error: Unable to accept the expression
          Type 0
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 CringeReturnType:
 In file $FILE:2:11 ->
@@ -80,7 +80,7 @@ Error: Cannot check the expression
          (Normalized: \ p0 ⇒ p0)
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 BadInterval:
 In file $FILE:2:16 ->
@@ -93,7 +93,7 @@ Error: The point `2` does not live in interval
 note: Did you mean:  `0` or `1`
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 BadPrim:
 In file $FILE:1:0 ->
@@ -116,7 +116,7 @@ Error: The prim declaration
          Type 0
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 PrimNoResult:
 In file $FILE:2:5 ->
@@ -136,7 +136,7 @@ In file $FILE:2:5 ->
 Error: `prim Path` is expected to have a return type
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 PiDom:
 In file $FILE:2:28 ->
@@ -151,7 +151,7 @@ Error: The type
          Type 0
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 PiDomMeta:
 In file $FILE:4:19 ->
@@ -181,7 +181,7 @@ Error: The meta (denoted ? below) is supposed to satisfy:
          X
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ConReturn:
 In file $FILE:2:14 ->
@@ -198,7 +198,7 @@ Error: Cannot make sense of the return type of the constructor
          X
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NoRule:
 In file $FILE:1:9 ->
@@ -216,5 +216,5 @@ In file $FILE:1:4 ->
 Error: Unsolved meta _
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt
index fbd4e1deea..a2c8326d28 100644
--- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt
+++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt
@@ -8,7 +8,7 @@ In file $FILE:2:18 ->
 Error: Unsolved meta _
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Goal:
 In file $FILE:2:28 ->
@@ -32,7 +32,7 @@ In file $FILE:2:28 ->
 Error: Unsolved meta _
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 UnsolvedMetaLit:
 In file $FILE:5:17 ->
@@ -92,7 +92,7 @@ Error: Unable to solve the type of this literal:
          `Nat`, `Nat2`
 
 5 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Daylily:
 In file $FILE:5:12 ->
@@ -163,7 +163,7 @@ Error: Unsolved meta _
        in `^0 (?_ ^0) → ^1 (Neg <X>)`
 
 4 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ScopeCheck:
 In file $FILE:5:14 ->
@@ -198,7 +198,7 @@ In file $FILE:5:14 ->
 Error: Unsolved meta _
 
 3 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 LiteralAmbiguous3:
 In file $FILE:6:11 ->
@@ -214,7 +214,7 @@ Error: Unable to solve the type of this literal:
          `List`, `List2`
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NonPattern:
 In file $FILE:9:3 ->
diff --git a/cli-impl/src/test/resources/negative/OperatorError.txt b/cli-impl/src/test/resources/negative/OperatorError.txt
index 11ea43f163..c460934950 100644
--- a/cli-impl/src/test/resources/negative/OperatorError.txt
+++ b/cli-impl/src/test/resources/negative/OperatorError.txt
@@ -10,7 +10,7 @@ Error: Ambiguous operator precedence detected between `==` and `+`
 note: Use `tighter/looser` clause or insert parentheses to make it clear.
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Cyclic:
 In file $FILE:3:28 ->
@@ -24,7 +24,7 @@ Error: Circular precedence found between b, c, d
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Issue677:
 In file $FILE:3:27 ->
@@ -46,7 +46,7 @@ In file $FILE:3:4 ->
 Error: Unsolved meta _
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NoAssoc:
 In file $FILE:9:21 ->
@@ -61,7 +61,7 @@ Error: Cannot figure out computation order because `=` (Infix) and `=` (Infix)
 note: Make them both left/right-associative to resolve this problem.
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 SelfBind:
 In file $FILE:2:9 ->
@@ -74,7 +74,7 @@ Error: Self bind is not allowed
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ModuleImportRename:
 That looks right!
diff --git a/cli-impl/src/test/resources/negative/ParseError.txt b/cli-impl/src/test/resources/negative/ParseError.txt
index b3db6d9cb4..aaf92003d6 100644
--- a/cli-impl/src/test/resources/negative/ParseError.txt
+++ b/cli-impl/src/test/resources/negative/ParseError.txt
@@ -7,7 +7,7 @@ In file $FILE:1:0 ->
 Error: Expect a name
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Modifier:
 In file $FILE:1:0 ->
@@ -18,7 +18,7 @@ In file $FILE:1:0 ->
 Error: The modifier overlap is not suitable here.
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 IgnoredModifier:
 In file $FILE:1:0 ->
diff --git a/cli-impl/src/test/resources/negative/PatCohError.txt b/cli-impl/src/test/resources/negative/PatCohError.txt
index 2d835e1604..5de67a76d7 100644
--- a/cli-impl/src/test/resources/negative/PatCohError.txt
+++ b/cli-impl/src/test/resources/negative/PatCohError.txt
@@ -14,7 +14,7 @@ Error: I'm unsure if there should be a case for constructor
          Fin+1 m
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Confl:
 In file $FILE:2:12 ->
@@ -34,7 +34,7 @@ Error: The 2nd and the 1st clauses are not confluent because we failed to unify
          suc zero
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ConflLiteral:
 In file $FILE:2:12 ->
@@ -225,7 +225,7 @@ Warning: The 2nd clause dominates the 6th clause. The 6th clause will be
          unreachable
 
 6 error(s), 7 warning(s).
-What are you doing?
+Let's learn from that.
 
 ConflLiteral2:
 In file $FILE:2:12 ->
@@ -529,7 +529,7 @@ Warning: The 5th clause dominates the 4th clause. The 4th clause will be
          unreachable
 
 11 error(s), 12 warning(s).
-What are you doing?
+Let's learn from that.
 
 FirstMatchDomination:
 In file $FILE:6:2 ->
@@ -619,7 +619,7 @@ Warning: The 5th clause dominates the 4th clause. The 4th clause will be
          unreachable
 
 2 error(s), 4 warning(s).
-What are you doing?
+Let's learn from that.
 
 NestedMissing:
 In file $FILE:2:0 ->
@@ -651,7 +651,7 @@ In file $FILE:7:2 ->
 Warning: The 5th clause is dominated by the other clauses, hence unreachable
 
 1 error(s), 1 warning(s).
-What are you doing?
+Let's learn from that.
 
 IApplyConfluence:
 In file $FILE:4:4 ->
@@ -675,7 +675,7 @@ Error: The 3rd clause matches on a path constructor. We failed to unify
          signed false 0
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Coverage:
 In file $FILE:2:0 ->
@@ -694,7 +694,7 @@ Error: Unhandled case:
          suc _, suc _, suc _, x'''
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 CoverageLiteral:
 In file $FILE:2:0 ->
@@ -713,7 +713,7 @@ Error: Unhandled case:
          1, 1, 1, x'''
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 IApplyConflReduce:
 In file $FILE:8:4 ->
@@ -739,5 +739,5 @@ Error: The 4th clause matches on a path constructor. We failed to unify
          pos n
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt
index 24f46172ba..b0f9a99683 100644
--- a/cli-impl/src/test/resources/negative/PatTyckError.txt
+++ b/cli-impl/src/test/resources/negative/PatTyckError.txt
@@ -10,7 +10,7 @@ Error: Unknown constructor
          test2
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 SelectionFailed:
 In file $FILE:4:2 ->
@@ -38,7 +38,7 @@ Error: I'm unsure if there should be a case for
          Vec (<n> + <n>) A
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 SelectionBlocked:
 In file $FILE:4:2 ->
@@ -53,7 +53,7 @@ Error: Unsure if this pattern is actually impossible, as constructor selection
          Vec (<n> + <n>) A
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 SplitOnNonData:
 In file $FILE:3:3 ->
@@ -69,7 +69,7 @@ Error: Cannot split on a non-inductive type
          unit y
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 BadLiteral:
 In file $FILE:3:2 ->
@@ -85,7 +85,7 @@ Error: The literal
          Test
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NotEnoughPattern:
 In file $FILE:3:8 ->
@@ -99,7 +99,7 @@ Error: There is no pattern for the parameter
          ^2
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 TooManyPattern:
 In file $FILE:3:11 ->
@@ -115,7 +115,7 @@ Error: There are too many implicit patterns:
          ^2
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 TooManyPattern2:
 In file $FILE:3:14 ->
@@ -132,7 +132,7 @@ Error: There is no parameter for the pattern
        before the `:` in the signature)
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 InvalidEmptyBody:
 In file $FILE:3:2 ->
@@ -156,7 +156,7 @@ Error: This match arm does not contain any absurd pattern but it has an empty
        body
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 InvalidAbsurdPattern:
 In file $FILE:2:23 ->
@@ -168,7 +168,7 @@ In file $FILE:2:23 ->
 Error: Absurd pattern does not fit here because `true` is still available
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NoPattern:
 In file $FILE:4:0 ->
@@ -182,7 +182,7 @@ Error: Unhandled case:
          A, B, f, g, p
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NewRepoIssue597:
 In file $FILE:2:22 ->
@@ -207,7 +207,7 @@ Error: There is no parameter for the pattern
        before the `:` in the signature)
 
 2 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NewRepoIssue746:
 In file $FILE:4:2 ->
@@ -221,7 +221,7 @@ Error: Unknown constructor
          test2
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 NewRepoIssue384:
 In file $FILE:1:4 ->
@@ -232,5 +232,5 @@ In file $FILE:1:4 ->
 Error: The empty pattern-matching function test does not have a telescope
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
diff --git a/cli-impl/src/test/resources/negative/ScopeError.txt b/cli-impl/src/test/resources/negative/ScopeError.txt
index cf096f90d6..d6f4d5d7fb 100644
--- a/cli-impl/src/test/resources/negative/ScopeError.txt
+++ b/cli-impl/src/test/resources/negative/ScopeError.txt
@@ -32,7 +32,7 @@ Error: The unqualified name `zero` is ambiguous
 
 Resolving interrupted due to:
 1 error(s), 2 warning(s).
-What are you doing?
+Let's learn from that.
 
 DidYouMean:
 In file $FILE:2:11 ->
@@ -46,7 +46,7 @@ Error: The name `suc` is not defined in the current scope
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ImportDefineShadow:
 In file $FILE:4:4 ->
@@ -73,7 +73,7 @@ Error: The qualified name `A::bar` is not defined in the current scope
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ImportHiding:
 In file $FILE:4:15 ->
@@ -87,7 +87,7 @@ Error: The qualified name `A::bar` is not defined in the current scope
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ImportDefineShadow2:
 In file $FILE:4:5 ->
@@ -111,7 +111,7 @@ In file $FILE:1:4 ->
 Error: The recursive definition `undefined` is not structurally recursive
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 Issue247:
 In file $FILE:3:2 ->
@@ -125,7 +125,7 @@ Error: The name zero (`zero`) is already defined elsewhere
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 RedefPrim:
 In file $FILE:1:12 ->
@@ -137,7 +137,7 @@ Error: Redefinition of primitive `I`
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 PrimDeps:
 In file $FILE:1:5 ->
@@ -149,7 +149,7 @@ Error: The primitive `Path` depends on undeclared primitive(s): `I`
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 UnknownPrim:
 In file $FILE:1:5 ->
@@ -161,7 +161,7 @@ Error: Unknown primitive `senpaiSuki`
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 UnknownVar:
 In file $FILE:2:9 ->
@@ -174,7 +174,7 @@ Error: The qualified name `Nat::suc` is not defined in the current scope
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 LetOpen:
 That looks right!
@@ -191,7 +191,7 @@ Error: The name `b` is not defined in the current scope
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 GeneralizedDisallowed:
 In file $FILE:3:7 ->
@@ -205,7 +205,7 @@ Error: The generalized variable `A` is not available here
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 DuplicateModName:
 In file $FILE:2:7 ->
@@ -218,7 +218,7 @@ Error: The module name `A` is already defined elsewhere
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 ImportNoneExistMod:
 In file $FILE:1:7 ->
@@ -230,7 +230,7 @@ Error: The module name `hopefullyThisModuleWillNeverExist` is not found
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 OpenNoneExistMod:
 In file $FILE:1:5 ->
@@ -243,5 +243,5 @@ Error: The module name `hopefullyThisModuleWillNeverExist` is not defined in the
 
 Resolving interrupted due to:
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
diff --git a/cli-impl/src/test/resources/negative/TerckError.txt b/cli-impl/src/test/resources/negative/TerckError.txt
index 0654a9958b..f20c1dee0e 100644
--- a/cli-impl/src/test/resources/negative/TerckError.txt
+++ b/cli-impl/src/test/resources/negative/TerckError.txt
@@ -13,7 +13,7 @@ note: In particular, the problematic call is:
         =
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 UnfoldNonTermination:
 In file $FILE:3:4 ->
@@ -30,7 +30,7 @@ note: In particular, the problematic call is:
         =
 
 1 error(s), 0 warning(s).
-What are you doing?
+Let's learn from that.
 
 SwapAddition:
 That looks right!