From 2324c0939d6407a567b32ecce883528f2cb35da0 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 26 Aug 2025 18:54:02 +0200 Subject: [PATCH] chore: add private `getUtf8Byte'` to `Init.Meta` (#10140) This PR adds a private `Lean.Name.getUtf8Byte'` to `Init.Meta` for a future PR that optimizes `Lean.Name.escapePart`. `Lean.Name.getUtf8Byte'` should be replaced with `String.getUtf8Byte` once the string refactor is through. --- src/Init/Meta.lean | 6 ++++++ stage0/src/stdlib_flags.h | 2 ++ 2 files changed, 8 insertions(+) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 88acee7b66..fa42a35901 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -131,6 +131,12 @@ def isInaccessibleUserName : Name → Bool | Name.num p _ => isInaccessibleUserName p | _ => false +-- FIXME: `getUtf8Byte` is in `Init.Data.String.Extra`, which causes an import cycle with +-- `Init.Meta`. Moving `getUtf8Byte` up to `Init.Data.String.Basic` creates another import cycle. +-- Please replace this definition with `getUtf8Byte` when the string refactor is through. +@[extern "lean_string_get_byte_fast"] +private opaque getUtf8Byte' (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8 + /-- Creates a round-trippable string name component if possible, otherwise returns `none`. Names that are valid identifiers are not escaped, and otherwise, if they do not contain `»`, they are escaped. diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..910e30f4fa 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// Please update stage0, dear CI + namespace lean { options get_default_options() { options opts;