You are receiving this mail as a port that you maintain
is failing to build on the FreeBSD package build server.
Please investigate the failure and submit a PR to fix
build.

Maintainer:     [email protected]
Log URL:        
https://pkg-status.freebsd.org/beefy24/data/main-amd64-default/p1edbeefa02b8_se8a3352e8b5/logs/lean4-4.31.0.log
Build URL:      
https://pkg-status.freebsd.org/beefy24/build.html?mastername=main-amd64-default&build=p1edbeefa02b8_se8a3352e8b5
Log:

=>> Building math/lean4
build started at Tue Jun 23 06:23:20 UTC 2026
port directory: /usr/ports/math/lean4
package name: lean4-4.31.0
building for: FreeBSD main-amd64-default-job-04 16.0-CURRENT FreeBSD 
16.0-CURRENT 1600019 amd64
maintained by: [email protected]
Makefile datestamp: -rw-r--r--  1 root wheel 4167 Jun 18 01:01 
/usr/ports/math/lean4/Makefile
Ports top last git commit: 1edbeefa02b8180e91f80d880ad0bf57c556ae32
Ports top unclean checkout: no
Port dir last git commit: 7ac81ad70ce30641e2d4a3d938bbbe7243ef8e5b
Port dir unclean checkout: no
Poudriere version: poudriere-git-3.4.8
Host OSVERSION: 1600018
Jail OSVERSION: 1600019
Job Id: 04




!!! Jail is newer than host. (Jail: 1600019, Host: 1600018) !!!
!!! This is not supported. !!!
!!! Host kernel must be same or newer than jail. !!!
!!! Expect build failures. !!!



---Begin Environment---
SHELL=/bin/sh
OSVERSION=1600019
UNAME_v=FreeBSD 16.0-CURRENT 1600019
UNAME_r=16.0-CURRENT
BLOCKSIZE=K
MAIL=/var/mail/root
MM_CHARSET=UTF-8
LANG=C.UTF-8
STATUS=1
HOME=/root
PATH=/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin
MAKE_OBJDIR_CHECK_WRITABLE=0
LOCALBASE=/usr/local
USER=root
POUDRIERE_NAME=poudriere-git
LIBEXECPREFIX=/usr/local/libexec/poudriere
POUDRIERE_VERSION=3.4.8
MASTERMNT=/usr/local/poudriere/data/.m/main-amd64-default/ref
LC_COLLATE=C
POUDRIERE_BUILD_TYPE=bulk
PACKAGE_BUILDING=yes
SAVED_TERM=
OUTPUT_REDIRECTED_STDERR=4
OUTPUT_REDIRECTED=1
PWD=/usr/local/poudriere/data/.m/main-amd64-default/04/.p
OUTPUT_REDIRECTED_STDOUT=3
P_PORTS_FEATURES=FLAVORS SUBPACKAGES SELECTED_OPTIONS
MASTERNAME=main-amd64-default
SCRIPTPREFIX=/usr/local/share/poudriere
SCRIPTNAME=bulk.sh
OLDPWD=/usr/local/poudriere/data/.m/main-amd64-default/ref/.p/pool
POUDRIERE_PKGNAME=poudriere-git-3.4.8
SCRIPTPATH=/usr/local/share/poudriere/bulk.sh
POUDRIEREPATH=/usr/local/bin/poudriere
---End Environment---

---Begin Poudriere Port Flags/Env---
PORT_FLAGS=
PKGENV=
FLAVOR=
MAKE_ARGS=
---End Poudriere Port Flags/Env---

---Begin OPTIONS List---
---End OPTIONS List---

--MAINTAINER--
[email protected]
--End MAINTAINER--

--CONFIGURE_ARGS--

--End CONFIGURE_ARGS--

--CONFIGURE_ENV--
MAKE=/usr/local/bin/gmake PKG_CONFIG=pkgconf PYTHON="/usr/local/bin/python3.11" 
XDG_DATA_HOME=/wrkdirs/usr/ports/math/lean4/work  
XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/lean4/work  
XDG_CACHE_HOME=/wrkdirs/usr/ports/math/lean4/work/.cache  
HOME=/wrkdirs/usr/ports/math/lean4/work TMPDIR="/tmp" 
PATH=/wrkdirs/usr/ports/math/lean4/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin
 
PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/lean4/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig
 SHELL=/bin/sh CONFIG_SHELL=/bin/sh
--End CONFIGURE_ENV--

--MAKE_ENV--
LD_LIBRARY_PATH=/wrkdirs/usr/ports/math/lean4/work/.build/stage0/lib/lean 
XDG_DATA_HOME=/wrkdirs/usr/ports/math/lean4/work  
XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/lean4/work  
XDG_CACHE_HOME=/wrkdirs/usr/ports/math/lean4/work/.cache  
HOME=/wrkdirs/usr/ports/math/lean4/work TMPDIR="/tmp" 
PATH=/wrkdirs/usr/ports/math/lean4/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin
 
PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/lean4/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig
 MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES 
PREFIX=/usr/local  LOCALBASE=/usr/local  CC="cc" CFLAGS="-O2 -pipe  -fPIC 
-fstack-protector-strong -fno-strict-aliasing "  CPP="cpp" CPPFLAGS=""  
LDFLAGS=" " LIBS=""  CXX="c++" CXXFLAGS="-O2 -pipe -fPIC 
-fstack-protector-strong -fno-strict-aliasing   -fPIC " 
BSD_INSTALL_PROGRAM="install  -s -m 555"  BSD_INSTALL_LIB="install  -s -m 0644" 
 BSD_INSTALL_SCRIPT="install  -m 555" 
 BSD_INSTALL_DATA="install  -m 0644"  BSD_INSTALL_MAN="install  -m 444"
--End MAKE_ENV--

--PLIST_SUB--
CMAKE_BUILD_TYPE="release" PYTHON_INCLUDEDIR=include/python3.11  
PYTHON_LIBDIR=lib/python3.11  PYTHON_PLATFORM=freebsd16  
PYTHON_SITELIBDIR=lib/python3.11/site-packages  PYTHON_SUFFIX=311  
PYTHON_BASESUFFIX=311  PYTHON_TAG=.cpython-311  PYTHON_SOABI=.cpython-311  
PYTHON_VER=3.11  PYTHON_BASEVER=3.11  PYTHON_VERSION=python3.11 
PYTHON2="@comment " PYTHON3="" OSREL=16.0 PREFIX=%D LOCALBASE=/usr/local  
RESETPREFIX=/usr/local LIB32DIR=lib DOCSDIR="share/doc/lean4"  
EXAMPLESDIR="share/examples/lean4"  DATADIR="share/lean4"  WWWDIR="www/lean4"  
ETCDIR="etc/lean4"
--End PLIST_SUB--

--SUB_LIST--
PYTHON_INCLUDEDIR=/usr/local/include/python3.11  
PYTHON_LIBDIR=/usr/local/lib/python3.11  PYTHON_PLATFORM=freebsd16  
PYTHON_SITELIBDIR=/usr/local/lib/python3.11/site-packages  PYTHON_SUFFIX=311  
PYTHON_BASESUFFIX=311  PYTHON_TAG=.cpython-311  PYTHON_SOABI=.cpython-311  
PYTHON_VER=3.11  PYTHON_BASEVER=3.11  PYTHON_VERSION=python3.11 
PYTHON2="@comment " PYTHON3="" PREFIX=/usr/local LOCALBASE=/usr/local  
DATADIR=/usr/local/share/lean4 DOCSDIR=/usr/local/share/doc/lean4 
EXAMPLESDIR=/usr/local/share/examples/lean4  WWWDIR=/usr/local/www/lean4 
ETCDIR=/usr/local/etc/lean4
--End SUB_LIST--

---Begin make.conf---
USE_PACKAGE_DEPENDS=yes
BATCH=yes
WRKDIRPREFIX=/wrkdirs
PORTSDIR=/usr/ports
PACKAGES=/packages
DISTDIR=/distfiles
PACKAGE_BUILDING=yes
PACKAGE_BUILDING_FLAVORS=yes
####  ####
# XXX: We really need this but cannot use it while 'make checksum' does not
# try the next mirror on checksum failure.  It currently retries the same
# failed mirror and then fails rather then trying another.  It *does*
# try the next if the size is mismatched though.
#MASTER_SITE_FREEBSD=yes
# Build ALLOW_MAKE_JOBS_PACKAGES with 3 jobs
MAKE_JOBS_NUMBER=3
#### Misc Poudriere ####
.include "/etc/make.conf.ports_env"
GID=0
UID=0
---End make.conf---
--Resource limits--
cpu time               (seconds, -t)  unlimited
file size           (512-blocks, -f)  unlimited
data seg size           (kbytes, -d)  33554432
stack size              (kbytes, -s)  524288
core file size      (512-blocks, -c)  unlimited
max memory size         (kbytes, -m)  unlimited
locked memory           (kbytes, -l)  unlimited
max user processes              (-u)  89999
open files                      (-n)  8192
virtual mem size        (kbytes, -v)  unlimited
swap limit              (kbytes, -w)  unlimited
socket buffer size       (bytes, -b)  unlimited
pseudo-terminals                (-p)  unlimited
kqueues                         (-k)  unlimited
umtx shared locks               (-o)  unlimited
pipebuf                 (kbytes, -y)  unlimited
virtual machines                (-V)  unlimited
--End resource limits--
=======================<phase: check-sanity   >============================
===== env: NO_DEPENDS=yes USER=root UID=0 GID=0

Please note that build 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

===>  License APACHE20 accepted by the user
===========================================================================
=======================<phase: pkg-depends    >============================
===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0
===>   lean4-4.31.0 depends on file: /usr/local/sbin/pkg - not found
===>   Installing existing package /packages/All/pkg-2.7.5.pkg
[main-amd64-default-job-04] Installing pkg-2.7.5...
[main-amd64-default-job-04] Extracting pkg-2.7.5: .......... done
===>   lean4-4.31.0 depends on file: /usr/local/sbin/pkg - found
===>   Returning to build of lean4-4.31.0
===========================================================================
=======================<phase: fetch-depends  >============================
===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0
===========================================================================
=======================<phase: fetch          >============================
===== env: NO_DEPENDS=yes USER=root UID=0 GID=0

Please note that build 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

===>  License APACHE20 accepted by the user
===> Fetching all distfiles required by lean4-4.31.0 for building
===========================================================================
=======================<phase: checksum       >============================
===== env: NO_DEPENDS=yes USER=root UID=0 GID=0

Please note that build 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

===>  License APACHE20 accepted by the user
===> Fetching all distfiles required by lean4-4.31.0 for building
=> SHA256 Checksum OK for leanprover-lean4-v4.31.0_GH0.tar.gz.
===========================================================================
=======================<phase: extract-depends>============================
===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0
===========================================================================
=======================<phase: extract        >============================
===== env: NO_DEPENDS=yes USER=root UID=0 GID=0

Please note that build Lean requires /proc to be mounted.
<snip>
✔ [4688/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing:c.o (2.3s)
✔ [4689/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Proof:c.o (10s)
✔ [4690/4863] Built Lean.Meta.Tactic.Grind.EMatch (41s)
✔ [4691/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Proof:c.o (13s)
✔ [4692/4863] Built Lean.Meta.Tactic.Grind.Order.Internalize (13s)
✔ [4693/4863] Built Lean.Meta.Tactic.Grind.Order (1.6s)
✔ [4694/4863] Built Lean.Meta.Tactic.Grind.Order:c.o (448ms)
✔ [4695/4863] Built Lean.Meta.Tactic.Grind.Order.Internalize:c.o (7.5s)
✔ [4696/4863] Built Lean.Meta.Tactic.Grind.EMatch:c.o (12s)
✔ [4697/4863] Built Lean.Meta.Tactic.Grind.AC.Eq (32s)
✔ [4698/4863] Built Lean.Meta.Tactic.Grind.AC.Action (1.4s)
✔ [4699/4863] Built Lean.Meta.Tactic.Grind.AC.Action:c.o (351ms)
✔ [4700/4863] Built Lean.Meta.Tactic.Grind.AC (1.7s)
✔ [4701/4863] Built Lean.Meta.Tactic.Grind.AC:c.o (479ms)
✔ [4702/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof (33s)
✔ [4703/4863] Built Lean.Meta.Tactic.Grind.AC.Eq:c.o (10s)
✔ [4704/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr (44s)
✔ [4705/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr (6.0s)
✔ [4706/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.StructId (54s)
✔ [4707/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action (1.5s)
✔ [4708/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action:c.o (826ms)
✔ [4709/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr (9.0s)
✔ [4710/4863] Built Lean.Meta.Tactic.Grind.Arith.IsRelevant (2.1s)
✔ [4711/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr:c.o (2.4s)
✔ [4712/4863] Built Lean.Meta.Tactic.Grind.Arith.IsRelevant:c.o (555ms)
✔ [4713/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing (2.0s)
✔ [4714/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing:c.o (637ms)
✔ [4715/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Internalize (5.2s)
✔ [4716/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr (5.9s)
✔ [4717/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr:c.o (4.5s)
✔ [4718/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Internalize:c.o (1.0s)
✔ [4719/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.StructId:c.o (7.1s)
✔ [4720/4863] Built Lean.Meta.Tactic.Grind.Arith.Main (1.4s)
✔ [4721/4863] Built Lean.Meta.Tactic.Grind.Arith.Main:c.o (466ms)
✔ [4722/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof:c.o (15s)
✔ [4723/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr:c.o (2.5s)
✔ [4724/4863] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr:c.o (13s)
✔ [4725/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq (13s)
✔ [4726/4863] Built Lean.Meta.Tactic.Grind.Internalize (19s)
✔ [4727/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq:c.o (6.3s)
✔ [4728/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search (21s)
✔ [4729/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr (26s)
✔ [4730/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action (1.3s)
✔ [4731/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action:c.o (355ms)
✔ [4732/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear (1.0s)
✔ [4733/4863] Built Lean.Meta.Tactic.Grind.ForallProp (8.5s)
✔ [4734/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear:c.o (520ms)
✔ [4735/4863] Built Lean.Meta.Tactic.Grind.Internalize:c.o (11s)
✔ [4736/4863] Built Lean.Meta.Tactic.Grind.ForallProp:c.o (2.9s)
✔ [4737/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars (5.8s)
✔ [4738/4863] Built Lean.Meta.Tactic.Grind.SimpUtil (4.1s)
✔ [4739/4863] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search:c.o (7.0s)
✔ [4740/4863] Built Lean.Meta.Tactic.Grind.SimpUtil:c.o (1.7s)
✔ [4741/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars:c.o (3.3s)
✔ [4742/4863] Built Lean.Meta.Tactic.Grind.Core (16s)
✔ [4743/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr:c.o (11s)
✔ [4744/4863] Built Lean.Meta.Tactic.Grind.Core:c.o (5.5s)
✔ [4745/4863] Built Lean.Meta.Tactic.Grind.Intro (9.4s)
✔ [4746/4863] Built Lean.Meta.Tactic.Grind.Intro:c.o (4.4s)
✔ [4747/4863] Built Lean.Meta.Tactic.Grind.EMatchAction (6.0s)
✔ [4748/4863] Built Lean.Meta.Tactic.Grind.EMatchAction:c.o (3.2s)
✔ [4749/4863] Built Lean.Meta.Tactic.Grind.Split (12s)
✔ [4750/4863] Built Lean.Meta.Tactic.Grind.Finish (1.2s)
✔ [4751/4863] Built Lean.Meta.Tactic.Grind.Finish:c.o (524ms)
✔ [4752/4863] Built Lean.Meta.Tactic.Grind.Solve (1.1s)
✔ [4753/4863] Built Lean.Meta.Tactic.Grind.Solve:c.o (390ms)
✔ [4754/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search (29s)
✔ [4755/4863] Built Lean.Meta.Tactic.Grind.Lookahead (4.3s)
✔ [4756/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action (1.5s)
✔ [4757/4863] Built Lean.Meta.Tactic.Grind.Split:c.o (5.2s)
✔ [4758/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action:c.o (350ms)
✔ [4759/4863] Built Lean.Meta.Tactic.Grind.Lookahead:c.o (1.3s)
✔ [4760/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat (2.1s)
✔ [4761/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat:c.o (601ms)
✔ [4762/4863] Built Lean.Meta.Tactic.Grind.Arith (1.2s)
✔ [4763/4863] Built Lean.Meta.Tactic.Grind.Arith:c.o (329ms)
✔ [4764/4863] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search:c.o (10s)
✔ [4765/4863] Built Lean.Meta.Tactic.Grind.Main (14s)
✔ [4766/4863] Built Lean.Meta.Sym.Grind (2.4s)
✔ [4767/4863] Built Lean.Meta.Tactic.Grind (3.2s)
✔ [4768/4863] Built Lean.Meta.Sym.Grind:c.o (893ms)
✔ [4769/4863] Built Lean.Meta.Sym (1.1s)
✔ [4770/4863] Built Lean.Meta.Sym:c.o (391ms)
✔ [4771/4863] Built Lean.Meta.Tactic.Grind:c.o (875ms)
✔ [4772/4863] Built Lean.Meta.Tactic.LibrarySearch (5.3s)
✔ [4773/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Util (5.6s)
✔ [4774/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Util:c.o (2.1s)
✔ [4775/4863] Built Lean.Meta.Tactic.LibrarySearch:c.o (3.1s)
✔ [4776/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache (2.9s)
✔ [4777/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache:c.o (1.0s)
✔ [4778/4863] Built Lean.Meta.Tactic.Try.Collect (4.6s)
✔ [4779/4863] Built Lean.Elab.Tactic.LibrarySearch (4.9s)
✔ [4780/4863] Built Lean.Meta.Tactic.Grind.Main:c.o (10s)
✔ [4781/4863] Built Lean.Meta.Tactic.Try (1.7s)
✔ [4782/4863] Built Lean.Meta.Tactic.Try:c.o (423ms)
✔ [4783/4863] Built Lean.Meta.Tactic.Try.Collect:c.o (2.6s)
✔ [4784/4863] Built Lean.Elab.Tactic.Grind.Basic (12s)
✔ [4785/4863] Built Lean.Elab.Tactic.LibrarySearch:c.o (2.7s)
✔ [4786/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Entails (9.1s)
✔ [4787/4863] Built Lean.Elab.Tactic.Grind.WithGrindTacticM (2.5s)
✔ [4788/4863] Built Lean.Elab.Tactic.Grind.DSimprocDSL (2.6s)
✔ [4789/4863] Built Lean.Meta.Tactic.Cbv.Main (11s)
✔ [4790/4863] Built Lean.Elab.Tactic.Grind.SimprocDSL (3.0s)
✔ [4791/4863] Built Lean.Elab.Tactic.Grind.WithGrindTacticM:c.o (523ms)
✔ [4792/4863] Built Lean.Elab.Tactic.Grind.Filter (3.2s)
✔ [4793/4863] Built Lean.Elab.Tactic.Grind.DSimprocDSL:c.o (809ms)
✔ [4794/4863] Built Lean.Elab.Tactic.Grind.Filter:c.o (1.3s)
✔ [4795/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Entails:c.o (2.6s)
✔ [4796/4863] Built Lean.Elab.Tactic.Grind.Have (4.7s)
✔ [4797/4863] Built Lean.Elab.Tactic.Grind.SimprocDSL:c.o (1.9s)
✔ [4798/4863] Built Lean.Elab.Tactic.Grind.DSimprocDSLBuiltin (2.3s)
✔ [4799/4863] Built Lean.Meta.Tactic.Cbv (2.2s)
✔ [4800/4863] Built Lean.Elab.Tactic.Grind.RegisterSymDSimp (2.8s)
✔ [4801/4863] Built Lean.Meta.Tactic.Cbv:c.o (546ms)
✔ [4802/4863] Built Lean.Elab.Tactic.Grind.Have:c.o (1.1s)
✔ [4803/4863] Built Lean.Elab.Tactic.Grind.DSimprocDSLBuiltin:c.o (947ms)
✔ [4804/4863] Built Lean.Elab.Tactic.Grind.RegisterSymDSimp:c.o (900ms)
✔ [4805/4863] Built Lean.Elab.Tactic.Grind.RegisterSymSimp (3.7s)
✔ [4806/4863] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin (3.9s)
✔ [4807/4863] Built Lean.Elab.Tactic.Conv.Cbv (1.0s)
✔ [4808/4863] Built Lean.Meta.Tactic (2.3s)
✔ [4809/4863] Built Lean.Elab.Tactic.Conv.Cbv:c.o (751ms)
✔ [4810/4863] Built Lean.Elab.Tactic.Grind.RegisterSymSimp:c.o (1.1s)
✔ [4811/4863] Built Lean.Meta.Tactic:c.o (509ms)
✔ [4812/4863] Built Lean.Elab.Tactic.Conv (1.4s)
✔ [4813/4863] Built Lean.Elab.Tactic.Grind.Basic:c.o (8.6s)
✔ [4814/4863] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin:c.o (1.8s)
✔ [4815/4863] Built Lean.Elab.Tactic.Grind.ShowState (5.7s)
✔ [4816/4863] Built Lean.Elab.Tactic.Conv:c.o (517ms)
✔ [4817/4863] Built Lean.Elab.Tactic.Grind.Param (9.3s)
✔ [4818/4863] Built Lean.Meta (1.0s)
✔ [4819/4863] Built Lean.Elab.Tactic.Cbv (2.3s)
✔ [4820/4863] Built Lean.Meta:c.o (467ms)
✔ [4821/4863] Built Lean.Meta.Tactic.Cbv.Main:c.o (7.3s)
✔ [4822/4863] Built Lean.Elab.Tactic.Grind.Sym (7.6s)
✔ [4823/4863] Built Lean.Elab.Tactic.Cbv:c.o (903ms)
✔ [4824/4863] Built Lean.Elab.Tactic.Grind.Config (11s)
✔ [4825/4863] Built Lean.Elab.Tactic.Grind.ShowState:c.o (2.6s)
✔ [4826/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Solve (11s)
✔ [4827/4863] Built Lean.Elab.Tactic.Grind.Trace (2.7s)
✔ [4828/4863] Built Lean.Elab.Tactic.Grind.Trace:c.o (896ms)
✔ [4829/4863] Built Lean.Elab.Tactic.Grind.Param:c.o (5.0s)
✔ [4830/4863] Built Lean.Elab.Tactic.Grind.Sym:c.o (4.8s)
✔ [4831/4863] Built Lean.Elab.Tactic.Grind.Lint (4.9s)
✔ [4832/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Solve:c.o (3.3s)
✔ [4833/4863] Built Lean.Elab.Tactic.Grind.LintExceptions (2.1s)
✔ [4834/4863] Built Lean.Elab.Tactic.Grind.LintExceptions:c.o (316ms)
✔ [4835/4863] Built Lean.Elab.Tactic.Grind.Lint:c.o (5.6s)
✔ [4836/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Driver (9.1s)
✔ [4837/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Driver:c.o (3.3s)
✔ [4838/4863] Built Lean.Elab.Tactic.Grind.Config:c.o (14s)
✔ [4839/4863] Built Lean.Elab.Tactic.Grind.BuiltinTactic (19s)
✔ [4840/4863] Built Lean.Elab.Tactic.Grind.Main (21s)
✔ [4841/4863] Built Lean.Elab.Tactic.Grind (1.5s)
✔ [4842/4863] Built Lean.Elab.Tactic.Grind:c.o (356ms)
✔ [4843/4863] Built Lean.Elab.Tactic.Grind.BuiltinTactic:c.o (8.5s)
✔ [4844/4863] Built Lean.Elab.Tactic.Grind.Main:c.o (6.6s)
✔ [4845/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Frontend (10s)
✔ [4846/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen (1.6s)
✔ [4847/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen:c.o (342ms)
✔ [4848/4863] Built Lean.Elab.Tactic.Do.Internal (1.5s)
✔ [4849/4863] Built Lean.Elab.Tactic.Do.Internal:c.o (351ms)
✔ [4850/4863] Built Lean.Elab.Tactic.Do (1.5s)
✔ [4851/4863] Built Lean.Elab.Tactic.Do:c.o (363ms)
✔ [4852/4863] Built Lean.Elab.Tactic.Do.Internal.VCGen.Frontend:c.o (5.3s)
✔ [4853/4863] Built Lean.Elab.Tactic.Try (27s)
✔ [4854/4863] Built Lean.Elab.Tactic (1.0s)
✔ [4855/4863] Built Lean.Elab.Tactic:c.o (469ms)
✔ [4856/4863] Built Lean.Elab (2.1s)
✔ [4857/4863] Built Lean.Elab:c.o (449ms)
✔ [4858/4863] Built Lean (2.3s)
✔ [4859/4863] Built Lean:c.o (442ms)
✔ [4860/4863] Built Lean.Elab.Tactic.Try:c.o (14s)
✔ [4861/4863] Built Lean:static (827ms)
✔ [4862/4863] Built Lean:static (793ms)
Build completed successfully (4863 jobs).
gmake[6]: Nothing to be done for 'Std'.
gmake[6]: Nothing to be done for 'Lean'.
gmake[6]: Nothing to be done for 'Leanc'.
gmake[6]: Nothing to be done for 'LeanIR'.
gmake[6]: Nothing to be done for 'Lake'.
gmake[6]: Nothing to be done for 'LeanChecker'.
gmake[6]: Leaving directory 
'/wrkdirs/usr/ports/math/lean4/work/lean4-4.31.0/src'
gmake[5]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/.build/stage1'
[ 56%] Built target make_stdlib
gmake[4]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/.build/stage1'
gmake[3]: *** [Makefile:149: all] Error 2
gmake[3]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/.build/stage1'
gmake[2]: *** [CMakeFiles/stage1.dir/build.make:98: 
stage1-prefix/src/stage1-stamp/stage1-build] Error 2
gmake[2]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/.build'
gmake[1]: *** [CMakeFiles/Makefile2:140: CMakeFiles/stage1.dir/all] Error 2
gmake[1]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/.build'
gmake: *** [Makefile:139: all] Error 2
===> Compilation failed unexpectedly.
Try to set MAKE_JOBS_UNSAFE=yes and rebuild before reporting the failure to
the maintainer.
*** Error code 1

Stop.
make: stopped making "build" in /usr/ports/math/lean4

Reply via email to