From bd89787a87869f9d2dcb0d12851ce698e8e5aab3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 1 Dec 2023 14:00:01 +0100
Subject: [PATCH] chore: fix CPP warnings about `static_assert` (#3005)

else I see
```
[ 69%] Building CXX object runtime/CMakeFiles/leanrt.dir/platform.cpp.o
/home/jojo/build/lean/lean4/src/runtime/io.cpp:509:75: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
    static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64));
                                                                          ^
                                                                          , ""
/home/jojo/build/lean/lean4/src/runtime/io.cpp:517:74: warning: 'static_assert' with no message is a C++17 extension [-Wc++17-extensions]
    static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64));
                                                                         ^
                                                                         , ""
2 warnings generated.
```
when building
---
 src/runtime/io.cpp  | 4 ++--
 src/runtime/mpz.cpp | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

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<std::chrono::milliseconds>(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<std::chrono::nanoseconds>(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<mpn_digit>(v);
         m_digits[1] = static_cast<mpn_digit>(v >> 8*sizeof(mpn_digit));