merge: Do not explicitly set encoding in build (#1116)

aya-prover · Jun 19, 2024 · 3482274 · 3482274
2 parents c18e5df + 8bc6de4
commit 3482274
Show file tree

Hide file tree

Showing 10 changed files with 67 additions and 69 deletions.
diff --git 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
@@ -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.");
   }
 }
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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.