diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 207e33b8c4..47c99e9b6c 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -506,7 +506,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_ar /* monoMsNow : BaseIO Nat */ extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) { - static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64)); + static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64"); auto now = std::chrono::steady_clock::now(); auto tm = std::chrono::duration_cast(now.time_since_epoch()); return io_result_mk_ok(uint64_to_nat(tm.count())); @@ -514,7 +514,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) { /* monoNanosNow : BaseIO Nat */ extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now(obj_arg /* w */) { - static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64)); + static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64"); auto now = std::chrono::steady_clock::now(); auto tm = std::chrono::duration_cast(now.time_since_epoch()); return io_result_mk_ok(uint64_to_nat(tm.count())); diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp index 1b98672bb7..c9183f7846 100644 --- a/src/runtime/mpz.cpp +++ b/src/runtime/mpz.cpp @@ -327,7 +327,7 @@ void mpz::init_uint64(uint64 v) { allocate(1); m_digits[0] = v; } else { - static_assert(sizeof(uint64) == 2 * sizeof(unsigned)); + static_assert(sizeof(uint64) == 2 * sizeof(unsigned), "unsigned should be half the size of an uint64"); allocate(2); m_digits[0] = static_cast(v); m_digits[1] = static_cast(v >> 8*sizeof(mpn_digit));