From 0c24e5796f2c7ad34428d63a4ed0ca51fa319e84 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 26 Aug 2024 05:06:54 +0900
Subject: [PATCH] =?UTF-8?q?#time=20=E3=82=B3=E3=83=9E=E3=83=B3=E3=83=89?=
 =?UTF-8?q?=E3=81=A7=E8=A8=88=E6=B8=AC=E3=81=95=E3=82=8C=E3=82=8BLean?=
 =?UTF-8?q?=E3=81=AE=E8=A8=88=E7=AE=97=E6=99=82=E9=96=93=E3=81=AF=E3=81=AA?=
 =?UTF-8?q?=E3=81=9C=E9=81=85=E3=81=84=E3=81=AE=E3=81=8B=20Fixes=20#559?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Command/Diagnostic/Time.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Examples/Command/Diagnostic/Time.lean b/Examples/Command/Diagnostic/Time.lean
index f22f05ee..75dcf12a 100644
--- a/Examples/Command/Diagnostic/Time.lean
+++ b/Examples/Command/Diagnostic/Time.lean
@@ -28,6 +28,14 @@ where
 -- 10 ms 程度で終わる
 #time #eval fib 32
 
+/-
+```admonish warning title="注意"
+エディタ上から [`#eval`](./Eval.md) コマンドで実行したり、コマンドラインで `lean --run` で実行したときにはインタプリタが使用されます。これはコンパイル後のバイナリの実行時間とは異なります。
+
+コンパイル後のバイナリの実行時間を計測するには [`lean_exe`](https://github.com/leanprover/lean4/tree/master/src/lake#binary-executables) という `lakefile` のオプションを使用してください。
+```
+-/
+
 /- ## 舞台裏
 `IO.monoMsNow` という関数でそのときの時刻を取得し、その差を計算することで実行時間を計測することができます。これにより `#time` コマンドと同様のコマンドを自作することができます。
 -/