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/beefy22/data/144amd64-default/08bf8552608d/logs/lean4-4.33.1.log
Build URL:      
https://pkg-status.freebsd.org/beefy22/build.html?mastername=144amd64-default&build=08bf8552608d
Log:

=>> Building math/lean4
build started at Sun Sep 13 06:12:38 UTC 2026
port directory: /usr/ports/math/lean4
package name: lean4-4.33.1
building for: FreeBSD 144amd64-default-job-06 14.4-RELEASE-p9 FreeBSD 
14.4-RELEASE-p9 amd64
maintained by: [email protected]
Makefile datestamp: -rw-r--r--  1 root wheel 3876 Sep  8 01:01 
/usr/ports/math/lean4/Makefile
Ports top last git commit: 08bf8552608d33a4ffd8818cf846d5dbb12c64f9
Ports top unclean checkout: no
Port dir last git commit: 6dd0fb54cd6ce538fccd4e3d5eafff4740cffff9
Port dir unclean checkout: no
Poudriere version: poudriere-git-3.4.8-2-g2e891d4a
Host OSVERSION: 1600022
Jail OSVERSION: 1404000
Job Id: 06

---Begin Environment---
SHELL=/bin/sh
OSVERSION=1404000
UNAME_v=FreeBSD 14.4-RELEASE-p9
UNAME_r=14.4-RELEASE-p9
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-2-g2e891d4a
MASTERMNT=/usr/local/poudriere/data/.m/144amd64-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/144amd64-default/06/.p
OUTPUT_REDIRECTED_STDOUT=3
P_PORTS_FEATURES=FLAVORS SUBPACKAGES SELECTED_OPTIONS
MASTERNAME=144amd64-default
SCRIPTPREFIX=/usr/local/share/poudriere
SCRIPTNAME=bulk.sh
OLDPWD=/usr/local/poudriere/data/.m/144amd64-default/ref/.p/pool
POUDRIERE_PKGNAME=poudriere-git-3.4.8-2-g2e891d4a
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.12" 
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.12  
PYTHON_LIBDIR=lib/python3.12  PYTHON_PLATFORM=freebsd14  
PYTHON_SITELIBDIR=lib/python3.12/site-packages  PYTHON_SUFFIX=312  
PYTHON_BASESUFFIX=312  PYTHON_TAG=.cpython-312  PYTHON_SOABI=.cpython-312  
PYTHON_VER=3.12  PYTHON_BASEVER=3.12  PYTHON_VERSION=python3.12 
PYTHON2="@comment " PYTHON3="" OSREL=14.4 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.12  
PYTHON_LIBDIR=/usr/local/lib/python3.12  PYTHON_PLATFORM=freebsd14  
PYTHON_SITELIBDIR=/usr/local/lib/python3.12/site-packages  PYTHON_SUFFIX=312  
PYTHON_BASESUFFIX=312  PYTHON_TAG=.cpython-312  PYTHON_SOABI=.cpython-312  
PYTHON_VER=3.12  PYTHON_BASEVER=3.12  PYTHON_VERSION=python3.12 
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
DISABLE_MAKE_JOBS=poudriere
---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                         (-y)  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.33.1 depends on file: /usr/local/sbin/pkg - not found
===>   Installing existing package /packages/All/pkg-2.8.4.pkg
[144amd64-default-job-06] Installing pkg-2.8.4...
[144amd64-default-job-06] Extracting pkg-2.8.4: .......... done
===>   lean4-4.33.1 depends on file: /usr/local/sbin/pkg - found
===>   Returning to build of lean4-4.33.1
===========================================================================
=======================<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.33.1 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.33.1 for building
=> SHA256 Checksum OK for leanprover-lean4-v4.33.1_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.

  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.33.1 for building
===>  Extracting for lean4-4.33.1
<snip>
✔ [4827/4991] Built Lean.Server.Test.Runner:c.o (17s)
✔ [4828/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action (610ms)
✔ [4829/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq (4.8s)
✔ [4830/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action:c.o (186ms)
✔ [4831/4991] Built Lean.Meta.Tactic.Grind.Internalize (6.0s)
✔ [4832/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof (12s)
✔ [4833/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing (913ms)
✔ [4834/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing:c.o (457ms)
✔ [4835/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.StructId:c.o (8.7s)
✔ [4836/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search (6.0s)
✔ [4837/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action (548ms)
✔ [4838/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action:c.o (186ms)
✔ [4839/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr (2.6s)
✔ [4840/4991] Built Lean.Meta.Tactic.Grind.ForallProp (3.1s)
✔ [4841/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear (783ms)
✔ [4842/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr (3.2s)
✔ [4843/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear:c.o (421ms)
✔ [4844/4991] Built Lean.Meta.Tactic.Grind.Arith.Main (753ms)
✔ [4845/4991] Built Lean.Meta.Tactic.Grind.Arith.Main:c.o (404ms)
✔ [4846/4991] Built Lean.Meta.Tactic.Grind.SimpUtil (1.6s)
✔ [4847/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr:c.o (1.9s)
✔ [4848/4991] Built Lean.Meta.Tactic.Grind.AC.Eq:c.o (9.7s)
✔ [4849/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq:c.o (5.7s)
✔ [4850/4991] Built Lean.Meta.Tactic.Grind.Core (5.6s)
✔ [4851/4991] Built Lean.Meta.Tactic.Grind.ForallProp:c.o (2.5s)
✔ [4852/4991] Built Lean.Meta.Tactic.Grind.SimpUtil:c.o (1.5s)
✔ [4853/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr:c.o (3.7s)
✔ [4854/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search:c.o (6.8s)
✔ [4855/4991] Built Lean.Meta.Tactic.Grind.Internalize:c.o (8.8s)
✔ [4856/4991] Built Lean.Meta.Tactic.Grind.Intro (3.7s)
✔ [4857/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr:c.o (11s)
✔ [4858/4991] Built Lean.Meta.Tactic.Grind.Core:c.o (4.0s)
✔ [4859/4991] Built Lean.Meta.Tactic.Grind.EMatchAction (2.1s)
✔ [4860/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr (8.4s)
✔ [4861/4991] Built Lean.Meta.Tactic.Grind.Intro:c.o (2.8s)
✔ [4862/4991] Built Lean.Meta.Tactic.Grind.Split (4.6s)
✔ [4863/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars (1.0s)
✔ [4864/4991] Built Lean.Meta.Tactic.Grind.EMatchAction:c.o (3.1s)
✔ [4865/4991] Built Lean.Meta.Tactic.Grind.Finish (668ms)
✔ [4866/4991] Built Lean.Meta.Tactic.Grind.Finish:c.o (222ms)
✔ [4867/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof:c.o (14s)
✔ [4868/4991] Built Lean.Meta.Tactic.Grind.Solve (655ms)
✔ [4869/4991] Built Lean.Meta.Tactic.Grind.Lookahead (1.3s)
✔ [4870/4991] Built Lean.Meta.Tactic.Grind.Solve:c.o (179ms)
✔ [4871/4991] Built Lean.Meta.Tactic.Grind.Lookahead:c.o (1.1s)
✔ [4872/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars:c.o (2.7s)
✔ [4873/4991] Built Lean.Meta.Tactic.Grind.Split:c.o (4.0s)
✔ [4874/4991] Built Lean.Meta.Tactic.Grind.Main (4.4s)
✔ [4875/4991] Built Lean.Meta.Sym.Grind (732ms)
✔ [4876/4991] Built Lean.Meta.Sym (516ms)
✔ [4877/4991] Built Lean.Meta.Sym.Grind:c.o (613ms)
✔ [4878/4991] Built Lean.Meta.Sym:c.o (273ms)
✔ [4879/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr:c.o (9.3s)
✔ [4880/4991] Built Lean.Meta.Tactic.LibrarySearch (2.1s)
✔ [4881/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Util (2.1s)
✔ [4882/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.EPost (1.2s)
✔ [4883/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.EPost:c.o (848ms)
✔ [4884/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache (1.5s)
✔ [4885/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Util:c.o (1.5s)
✔ [4886/4991] Built Lean.Elab.Tactic.LibrarySearch (1.7s)
✔ [4887/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search (9.6s)
✔ [4888/4991] Built Lean.Meta.Tactic.Try.Collect (2.1s)
✔ [4889/4991] Built Lean.Elab.Tactic.Grind.Basic (4.2s)
✔ [4890/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache:c.o (938ms)
✔ [4891/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action (670ms)
✔ [4892/4991] Built Lean.Meta.Tactic.LibrarySearch:c.o (2.7s)
✔ [4893/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action:c.o (274ms)
✔ [4894/4991] Built Lean.Meta.Tactic.Try (863ms)
✔ [4895/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSL (1.1s)
✔ [4896/4991] Built Lean.Meta.Tactic.Try:c.o (304ms)
✔ [4897/4991] Built Lean.Elab.Tactic.Grind.SimprocDSL (1.2s)
✔ [4898/4991] Built Lean.Elab.Tactic.Grind.WithGrindTacticM (1.1s)
✔ [4899/4991] Built Lean.Elab.Tactic.Grind.Filter (1.3s)
✔ [4900/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Entails (1.0s)
✔ [4901/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat (883ms)
✔ [4902/4991] Built Lean.Elab.Tactic.Grind.WithGrindTacticM:c.o (389ms)
✔ [4903/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSL:c.o (523ms)
✔ [4904/4991] Built Lean.Elab.Tactic.Grind.Have (1.7s)
✔ [4905/4991] Built Lean.Elab.Tactic.Grind.Rewrite (1.8s)
✔ [4906/4991] Built Lean.Elab.Tactic.Grind.SimprocDSL:c.o (793ms)
✔ [4907/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat:c.o (626ms)
✔ [4908/4991] Built Lean.Meta.Tactic.Cbv.Main (4.0s)
✔ [4909/4991] Built Lean.Elab.Tactic.LibrarySearch:c.o (2.7s)
✔ [4910/4991] Built Lean.Elab.Tactic.Grind.Filter:c.o (843ms)
✔ [4911/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSLBuiltin (1.1s)
✔ [4912/4991] Built Lean.Meta.Tactic.Try.Collect:c.o (2.4s)
✔ [4913/4991] Built Lean.Meta.Tactic.Grind.Arith (921ms)
✔ [4914/4991] Built Lean.Elab.Tactic.Grind.RegisterSymDSimp (1.3s)
✔ [4915/4991] Built Lean.Elab.Tactic.Grind.RegisterSymSimp (1.3s)
✔ [4916/4991] Built Lean.Meta.Tactic.Grind.Arith:c.o (239ms)
✔ [4917/4991] Built Lean.Elab.Tactic.Grind.Have:c.o (1.0s)
✔ [4918/4991] Built Lean.Elab.Tactic.Grind.DSimp (1.5s)
✔ [4919/4991] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin (1.4s)
✔ [4920/4991] Built Lean.Meta.Tactic.Cbv (700ms)
✔ [4921/4991] Built Lean.Elab.Tactic.Grind.Cbv (897ms)
✔ [4922/4991] Built Lean.Meta.Tactic.Cbv:c.o (319ms)
✔ [4923/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSLBuiltin:c.o (851ms)
✔ [4924/4991] Built Lean.Elab.Tactic.Grind.Cbv:c.o (290ms)
✔ [4925/4991] Built Lean.Elab.Tactic.Grind.RegisterSymDSimp:c.o (726ms)
✔ [4926/4991] Built Lean.Elab.Tactic.Grind.RegisterSymSimp:c.o (892ms)
✔ [4927/4991] Built Lean.Elab.Tactic.Grind.ShowState (2.2s)
✔ [4928/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Entails:c.o (2.2s)
✔ [4929/4991] Built Lean.Elab.Tactic.Conv.Cbv (913ms)
✔ [4930/4991] Built Lean.Meta.Tactic.Grind (1.4s)
✔ [4931/4991] Built Lean.Elab.Tactic.Grind.Param (3.8s)
✔ [4932/4991] Built Lean.Elab.Tactic.Grind.Sym (2.6s)
✔ [4933/4991] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin:c.o (1.4s)
✔ [4934/4991] Built Lean.Elab.Tactic.Conv.Cbv:c.o (488ms)
✔ [4935/4991] Built Lean.Meta.Tactic.Grind:c.o (661ms)
✔ [4936/4991] Built Lean.Elab.Tactic.Grind.Rewrite:c.o (2.7s)
✔ [4937/4991] Built Lean.Meta.Tactic.Grind.Main:c.o (8.8s)
✔ [4938/4991] Built Lean.Elab.Tactic.Conv (910ms)
✔ [4939/4991] Built Lean.Elab.Tactic.Grind.DSimp:c.o (1.9s)
✔ [4940/4991] Built Lean.Elab.Tactic.Conv:c.o (233ms)
✔ [4941/4991] Built Lean.Elab.Tactic.Grind.Config (4.0s)
✔ [4942/4991] Built Lean.Meta.Tactic (1.3s)
✔ [4943/4991] Built Lean.Meta.Tactic:c.o (242ms)
✔ [4944/4991] Built Lean.Elab.Tactic.Grind.ShowState:c.o (2.1s)
✔ [4945/4991] Built Lean.Meta (1.3s)
✔ [4946/4991] Built Lean.Elab.Tactic.Cbv (1.6s)
✔ [4947/4991] Built Lean.Meta:c.o (351ms)
✔ [4948/4991] Built Lean.Elab.Tactic.Grind.Trace (1.7s)
✔ [4949/4991] Built Lean.Elab.Tactic.Grind.Lint (2.1s)
✔ [4950/4991] Built Lean.Elab.Tactic.Cbv:c.o (525ms)
✔ [4951/4991] Built Lean.Elab.Tactic.Grind.Sym:c.o (3.7s)
✔ [4952/4991] Built Lean.Elab.Tactic.Grind.Trace:c.o (869ms)
✔ [4953/4991] Built Lean.Meta.Tactic.Cbv.Main:c.o (6.0s)
✔ [4954/4991] Built Lean.Elab.Tactic.Grind.LintExceptions (1.2s)
✔ [4955/4991] Built Lean.Elab.Tactic.Grind.Basic:c.o (8.4s)
✔ [4956/4991] Built Lean.Elab.Tactic.Grind.LintExceptions:c.o (193ms)
✔ [4957/4991] Built Lean.Elab.Tactic.Grind.Param:c.o (5.1s)
✔ [4958/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Solve (7.9s)
✔ [4959/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search:c.o (9.6s)
✔ [4960/4991] Built Lean.Elab.Tactic.Grind.Main (5.2s)
✔ [4961/4991] Built Lean.Elab.Tactic.Grind.Lint:c.o (3.4s)
✔ [4962/4991] Built Lean.Elab.Tactic.Grind.BuiltinTactic (5.7s)
✔ [4963/4991] Built Lean.Elab.Tactic.Grind (710ms)
✔ [4964/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Driver (2.2s)
✔ [4965/4991] Built Lean.Elab.Tactic.Grind:c.o (224ms)
✔ [4966/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Driver:c.o (1.6s)
✔ [4967/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Solve:c.o (4.9s)
✔ [4968/4991] Built Lean.Elab.Tactic.Grind.Config:c.o (9.9s)
✔ [4969/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Frontend (4.0s)
✔ [4970/4991] Built Lean.Elab.Tactic.Grind.Main:c.o (5.7s)
✔ [4971/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen (910ms)
✔ [4972/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen:c.o (212ms)
✔ [4973/4991] Built Lean.Elab.Tactic.Do.Internal (717ms)
✔ [4974/4991] Built Lean.Elab.Tactic.Do.Internal:c.o (149ms)
✔ [4975/4991] Built Lean.Elab.Tactic.Do (725ms)
✔ [4976/4991] Built Lean.Elab.Tactic.Do:c.o (146ms)
✔ [4977/4991] Built Lean.Elab.Tactic.Try (8.8s)
✔ [4978/4991] Built Lean.Elab.Tactic.Grind.BuiltinTactic:c.o (9.0s)
✔ [4979/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Frontend:c.o (5.4s)
✔ [4980/4991] Built Lean.Elab.Tactic.AutoTry (2.5s)
✔ [4981/4991] Built Lean.Elab.Tactic (902ms)
✔ [4982/4991] Built Lean.Elab.Tactic:c.o (310ms)
✔ [4983/4991] Built Lean.Elab (1.1s)
✔ [4984/4991] Built Lean.Elab:c.o (382ms)
✔ [4985/4991] Built Lean (1.4s)
✔ [4986/4991] Built Lean:c.o (315ms)
✔ [4987/4991] Built Lean.Elab.Tactic.AutoTry:c.o (4.1s)
✔ [4988/4991] Built Lean.Elab.Tactic.Try:c.o (10s)
✖ [4989/4991] Building Lean:static (56ms)
trace: .> ar rcs 
/wrkdirs/usr/ports/math/lean4/work/.build/stage1/lib/lean/libLean.a 
@/wrkdirs/usr/ports/math/lean4/work/.build/stage1/lib/lean/libLean.a.rsp
info: stderr:
ar: warning: can't open file: 
@/wrkdirs/usr/ports/math/lean4/work/.build/stage1/lib/lean/libLean.a.rsp: No 
such file or directory
error: external command 'ar' exited with code 1
✖ [4990/4991] Building Lean:static (44ms)
trace: .> ar rcs 
/wrkdirs/usr/ports/math/lean4/work/.build/stage1/lib/lean/libLean.a.export 
@/wrkdirs/usr/ports/math/lean4/work/.build/stage1/lib/lean/libLean.a.export.rsp
info: stderr:
ar: warning: can't open file: 
@/wrkdirs/usr/ports/math/lean4/work/.build/stage1/lib/lean/libLean.a.export.rsp:
 No such file or directory
error: external command 'ar' exited with code 1
Some required targets logged failures:
- Init:static
- Init:static
- Leanc:static
- LeanChecker:static
- Std:static
- Std:static
- LeanIR:static
- LakeMain:static
- Lake:static
- Lake:static
- Lean:static
- Lean:static
error: build failed
gmake[6]: *** [/wrkdirs/usr/ports/math/lean4/work/.build/stage1/stdlib.make:57: 
Init] Error 1
gmake[5]: *** [CMakeFiles/make_stdlib.dir/build.make:70: 
CMakeFiles/make_stdlib] Error 2
gmake[4]: *** [CMakeFiles/Makefile2:1444: CMakeFiles/make_stdlib.dir/all] Error 
2
gmake[3]: *** [Makefile:146: 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
*** Error code 1

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

Reply via email to