diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index abfc3004d07b..aa4a44690ce8 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,46 +1,58 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
 DISTVERSION=	4.11.0
+PORTREVISION=	1
 CATEGORIES=	math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
 
 MAINTAINER=	yuri@FreeBSD.org
 COMMENT=	Theorem prover and functional language for math (new gen)
 WWW=		https://lean-lang.org/
 
 LICENSE=	APACHE20
 LICENSE_FILE=	${WRKSRC}/LICENSE
 
 BROKEN_armv7=	compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory
 BROKEN_i386=	linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter)
 
 BUILD_DEPENDS=	bash:shells/bash
 LIB_DEPENDS=	libgmp.so:math/gmp
 
 USES=		cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project
 
 USE_GITHUB=	yes
 GH_ACCOUNT=	leanprover
 
 CFLAGS+=	-fPIC
 CXXFLAGS+=	-fPIC
 
 BINARY_ALIAS=	make=${GMAKE} python=${PYTHON_CMD}
 
+pre-everything::
+	@${ECHO_MSG} ""
+	@${ECHO_MSG} "Please note that build Lean requires /proc to be mounted."
+	@${ECHO_MSG} ""
+	@${ECHO_MSG} "  The usual way to do this is to add this line to /etc/fstab:"
+	@${ECHO_MSG} "  proc /proc procfs rw 0 0"
+	@${ECHO_MSG} ""
+	@${ECHO_MSG} "  and then run this command as root:"
+	@${ECHO_MSG} "  # mount /proc"
+	@${ECHO_MSG} ""
+
 post-install:
 	# remove empty dirs
 	@${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete
 	# remove stray files
 	@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
 	# strip binaries
 	@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
 		bin/lake \
 		bin/lean \
 		bin/leanc \
 		lib/lean/libInit_shared.so \
 		lib/lean/libleanshared.so
 
 # 2 test failures:
 # https://github.com/leanprover/lean4/issues/4396: The test leanlaketest_old times out
 # https://github.com/leanprover/lean4/issues/4397: The test leanlaketest_serve fails: error: unexpected identifier; expected command
 
 .include <bsd.port.mk>
diff --git a/math/lean4/pkg-message b/math/lean4/pkg-message
deleted file mode 100644
index e0c1a26dc720..000000000000
--- a/math/lean4/pkg-message
+++ /dev/null
@@ -1,22 +0,0 @@
-[
-{ type: install
-  message: <<EOM
-================================================================================
-You installed Lean: The Theorem Prover.
-
-(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
-
-    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
-}
-]