From 9d24f614fa7b9f74bd70364d141ade12091b590d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Aug 2021 18:03:57 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Leanpkg.lean | 1 + stage0/src/util/name.h | 8 ++++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/stage0/src/Leanpkg.lean b/stage0/src/Leanpkg.lean index c43ba47313..3be55008de 100644 --- a/stage0/src/Leanpkg.lean +++ b/stage0/src/Leanpkg.lean @@ -219,6 +219,7 @@ end Leanpkg def main (args : List String) : IO UInt32 := do try + Lean.enableInitializersExecution Lean.initSearchPath none -- HACK let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args Leanpkg.main cmd outerArgs innerArgs diff --git a/stage0/src/util/name.h b/stage0/src/util/name.h index 16cebab50e..1689455fd5 100644 --- a/stage0/src/util/name.h +++ b/stage0/src/util/name.h @@ -40,8 +40,12 @@ inline bool is_id_rest(char const * begin, char const * end) { reinterpret_cast(end)); } -extern "C" uint64_t lean_name_hash_exported(b_lean_obj_arg n); +extern "C" uint64_t lean_name_hash_exported(lean_obj_arg n); +inline uint64_t lean_name_hash_exported_b(b_lean_obj_arg n) { + lean_inc(n); + return lean_name_hash_exported(n); +} enum class name_kind { ANONYMOUS, STRING, NUMERAL }; /** \brief Hierarchical names. */ @@ -95,7 +99,7 @@ public: name & operator=(name const & other) { object_ref::operator=(other); return *this; } name & operator=(name && other) { object_ref::operator=(other); return *this; } static uint64_t hash(b_obj_arg n) { - lean_assert(lean_name_hash(n) == lean_name_hash_exported(n)); + lean_assert(lean_name_hash(n) == lean_name_hash_exported_b(n)); return lean_name_hash(n); } uint64_t hash() const { return hash(raw()); }