Merge pull request #114 from lean-dojo/peiyang

Fix string UTF-8 misformatting PANIC
lean-dojo · Aug 14, 2024 · 88e50cb · 88e50cb
2 parents d7ad9f5 + 7e4910c
commit 88e50cb
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/LeanCopilot/Models/ByT5.lean b/LeanCopilot/Models/ByT5.lean
@@ -281,7 +281,9 @@ def tokenize (text : String) : Array String :=
 
 
 def detokenize (tokens : Array String) : String :=
-  String.fromUTF8! ⟨tokens.map tokenToByte!⟩
+  match (String.fromUTF8? ⟨tokens.map tokenToByte!⟩) with
+  | some s => s
+  | none => ""
 
 
 def eosToken := "</s>"