git: 258e95b1faee - main - math/lean: Add to pkg-message

From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Tue, 06 Sep 2022 16:06:12 UTC
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=258e95b1faee70d25f552938ee948972deb83b74

commit 258e95b1faee70d25f552938ee948972deb83b74
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2022-09-06 16:05:45 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2022-09-06 16:06:07 +0000

    math/lean: Add to pkg-message
---
 math/lean/pkg-message | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/math/lean/pkg-message b/math/lean/pkg-message
index c3656195ef46..e0c1a26dc720 100644
--- a/math/lean/pkg-message
+++ b/math/lean/pkg-message
@@ -1,16 +1,22 @@
 [
 { type: install
   message: <<EOM
-You installed lean: The Theorem Prover.
+================================================================================
+You installed Lean: The Theorem Prover.
 
-Please note that lean requires /proc to be mounted.
+(1) Please note that Lean requires /proc to be mounted.
 
-The usual way to do this is to add this line to /etc/fstab:
-proc /proc procfs rw 0 0
+    The usual way to do this is to add this line to /etc/fstab:
+    proc /proc procfs rw 0 0
 
-and then run this command as root:
-# mount /proc
+    and then run this command as root:
+    # mount /proc
 
+(2) You might also want to install mathlibtools (math/mathlibtools) in case
+    you need to use the mathematical library of Lean.
+    mathlibtools download this library to user's home directory for further
+    use by Lean.
+================================================================================
 EOM
 }
 ]