diff --git a/src/Init/Data/Ord/String.lean b/src/Init/Data/Ord/String.lean
index d928196ab5..37c46be239 100644
--- a/src/Init/Data/Ord/String.lean
+++ b/src/Init/Data/Ord/String.lean
@@ -25,8 +25,14 @@ open Std
 
 namespace String
 
+/--
+Lexicographic comparison of strings
+-/
+def compare (s₁ s₂ : @& String) : Ordering :=
+  compareOfLessAndEq s₁ s₂
+
 instance : Ord String where
-  compare x y := compareOfLessAndEq x y
+  compare := String.compare
 
 instance : TransOrd String :=
   TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index fe7d099e94..fa126b6ef5 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -1252,6 +1252,7 @@ static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) {
 }
 static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); }
 LEAN_EXPORT bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
+LEAN_EXPORT uint8_t lean_string_compare(b_lean_obj_arg s1, b_lean_obj_arg s2);
 static inline uint8_t lean_string_dec_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_eq(s1, s2); }
 static inline uint8_t lean_string_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_lt(s1, s2); }
 LEAN_EXPORT uint64_t lean_string_hash(b_lean_obj_arg);
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 97794a7f09..426357b607 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -2108,6 +2108,18 @@ extern "C" LEAN_EXPORT bool lean_string_lt(object * s1, object * s2) {
     return r < 0 || (r == 0 && sz1 < sz2);
 }
 
+// Constructor indices of `Ordering`: lt = 0, eq = 1, gt = 2.
+extern "C" LEAN_EXPORT uint8_t lean_string_compare(b_obj_arg s1, b_obj_arg s2) {
+    size_t sz1 = lean_string_size(s1) - 1; // ignore null char in the end
+    size_t sz2 = lean_string_size(s2) - 1; // ignore null char in the end
+    int r      = std::memcmp(lean_string_cstr(s1), lean_string_cstr(s2), std::min(sz1, sz2));
+    if (r < 0) return 0;
+    if (r > 0) return 2;
+    if (sz1 < sz2) return 0;
+    if (sz1 > sz2) return 2;
+    return 1;
+}
+
 static obj_res string_to_list_core(std::string const & s, bool reverse = false) {
     std::vector<unsigned> tmp;
     utf8_decode(s, tmp);
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index e444447049..4682959a61 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update thy
+
 namespace lean {
 options get_default_options() {
     options opts;