max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-16 18:03:57 -07:00
parent b01239b25b
commit 9d24f614fa
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Leanpkg.lean generated
View file

@ -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

8
stage0/src/util/name.h generated
View file

@ -40,8 +40,12 @@ inline bool is_id_rest(char const * begin, char const * end) {
reinterpret_cast<unsigned char const *>(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()); }