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/143amd64-default/ebebd1ac46ea/logs/lean4-4.30.0_1.log Build URL: https://pkg-status.freebsd.org/beefy22/build.html?mastername=143amd64-default&build=ebebd1ac46ea Log: =>> Building math/lean4 build started at Sat May 30 05:14:06 UTC 2026 port directory: /usr/ports/math/lean4 package name: lean4-4.30.0_1 building for: FreeBSD 143amd64-default-job-37 14.3-RELEASE-p14 FreeBSD 14.3-RELEASE-p14 amd64 maintained by: [email protected] Makefile datestamp: -rw-r--r-- 1 root wheel 3352 May 30 01:01 /usr/ports/math/lean4/Makefile Ports top last git commit: ebebd1ac46ea0fc3e57840eb0faf0370d748ce4d Ports top unclean checkout: no Port dir last git commit: 516f8a5764de5c7bdd0e9f7810601a5057bbc650 Port dir unclean checkout: no Poudriere version: poudriere-git-3.4.8 Host OSVERSION: 1600018 Jail OSVERSION: 1403000 Job Id: 37 ---Begin Environment--- SHELL=/bin/sh OSVERSION=1403000 UNAME_v=FreeBSD 14.3-RELEASE-p14 UNAME_r=14.3-RELEASE-p14 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/143amd64-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/143amd64-default/37/.p OUTPUT_REDIRECTED_STDOUT=3 P_PORTS_FEATURES=FLAVORS SUBPACKAGES SELECTED_OPTIONS MASTERNAME=143amd64-default SCRIPTPREFIX=/usr/local/share/poudriere SCRIPTNAME=bulk.sh OLDPWD=/usr/local/poudriere/data/.m/143amd64-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=freebsd14 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=14.3 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=freebsd14 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 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.30.0_1 depends on file: /usr/local/sbin/pkg - not found ===> Installing existing package /packages/All/pkg-2.7.5.pkg [143amd64-default-job-37] Installing pkg-2.7.5... [143amd64-default-job-37] Extracting pkg-2.7.5: .......... done ===> lean4-4.30.0_1 depends on file: /usr/local/sbin/pkg - found ===> Returning to build of lean4-4.30.0_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 => leanprover-lean4-v4.30.0_GH0.tar.gz doesn't seem to exist in /portdistfiles. => Attempting to fetch https://codeload.github.com/leanprover/lean4/tar.gz/v4.30.0?dummy=/leanprover-lean4-v4.30.0_GH0.tar.gz fetch: https://codeload.github.com/leanprover/lean4/tar.gz/v4.30.0?dummy=/leanprover-lean4-v4.30.0_GH0.tar.gz: size unknown fetch: https://codeload.github.com/leanprover/lean4/tar.gz/v4.30.0?dummy=/leanprover-lean4-v4.30.0_GH0.tar.gz: size of remote file is not known leanprover-lean4-v4.30.0_GH0.tar.gz 67 MB 5513 kBps 13s ===> Fetching all distfiles required by lean4-4.30.0_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.30.0_1 for building => SHA256 Checksum OK for leanprover-lean4-v4.30.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. 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: <snip> â [4464/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize:c.o (3.3s) â [4465/4625] Built Lean.Elab.Tactic.Omega (752ms) â [4466/4625] Built Lean.Elab.Tactic.Omega:c.o (147ms) â [4467/4625] Built Lean.Server.FileWorker:c.o (9.7s) â [4468/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Reify:c.o (11s) â [4469/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Var:c.o (2.1s) â [4470/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing (2.9s) â [4471/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt:c.o (7.5s) â [4472/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing:c.o (1.8s) â [4473/4625] Built Lean.Meta.Tactic.Grind.Order.Internalize (7.3s) â [4474/4625] Built Lean.Meta.Tactic.Grind.Order (655ms) â [4475/4625] Built Lean.Meta.Tactic.FunInd:c.o (37s) â [4476/4625] Built Lean.Meta.Tactic.Grind.AC.Proof:c.o (7.5s) â [4477/4625] Built Lean.Meta.Tactic.Grind.Order:c.o (226ms) â [4478/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Proof:c.o (9.8s) â [4479/4625] Built Lean.Elab.Tactic.Omega.Frontend:c.o (8.4s) â [4480/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Proof:c.o (12s) â [4481/4625] Built Lean.Server.Test.Runner:c.o (13s) â [4482/4625] Built Lean.Meta.Tactic.Grind.Order.Internalize:c.o (5.8s) â [4483/4625] Built Lean.Meta.Tactic.Grind.EMatch (28s) â [4484/4625] Built Lean.Meta.Tactic.Grind.AC.Eq (14s) â [4485/4625] Built Lean.Meta.Tactic.Grind.AC.Action (702ms) â [4486/4625] Built Lean.Meta.Tactic.Grind.AC.Action:c.o (150ms) â [4487/4625] Built Lean.Meta.Tactic.Grind.AC (657ms) â [4488/4625] Built Lean.Meta.Tactic.Grind.AC:c.o (206ms) â [4489/4625] Built Lean.Meta.Tactic.Grind.AC.Eq:c.o (7.7s) â [4490/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr (23s) â [4491/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof (17s) â [4492/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action (521ms) â [4493/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action:c.o (137ms) â [4494/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing (863ms) â [4495/4625] Built Lean.Meta.Tactic.Grind.EMatch:c.o (11s) â [4496/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing:c.o (448ms) â [4497/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr (3.4s) â [4498/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr (3.9s) â [4499/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr:c.o (1.1s) â [4500/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr:c.o (4.0s) â [4501/4625] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr:c.o (11s) â [4502/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof:c.o (13s) â [4503/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr (13s) â [4504/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars (2.6s) â [4505/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars:c.o (2.4s) â [4506/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr:c.o (8.0s) â [4507/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search (16s) â [4508/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action (652ms) â [4509/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action:c.o (164ms) â [4510/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat (888ms) â [4511/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat:c.o (384ms) â [4512/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.StructId (65s) â [4513/4625] Built Lean.Meta.Tactic.Grind.Arith.IsRelevant (556ms) â [4514/4625] Built Lean.Meta.Tactic.Grind.Arith.IsRelevant:c.o (177ms) â [4515/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Internalize (2.0s) â [4516/4625] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search:c.o (6.6s) â [4517/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr (2.4s) â [4518/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Internalize:c.o (734ms) â [4519/4625] Built Lean.Meta.Tactic.Grind.Arith.Main (675ms) â [4520/4625] Built Lean.Meta.Tactic.Grind.Arith.Main:c.o (286ms) â [4521/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr:c.o (1.6s) â [4522/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.StructId:c.o (5.3s) â [4523/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq (6.2s) â [4524/4625] Built Lean.Meta.Tactic.Grind.Internalize (9.8s) â [4525/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq:c.o (4.4s) â [4526/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search (11s) â [4527/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action (530ms) â [4528/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action:c.o (126ms) â [4529/4625] Built Lean.Meta.Tactic.Grind.ForallProp (4.2s) â [4530/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear (780ms) â [4531/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear:c.o (225ms) â [4532/4625] Built Lean.Meta.Tactic.Grind.Arith (513ms) â [4533/4625] Built Lean.Meta.Tactic.Grind.Arith:c.o (118ms) â [4534/4625] Built Lean.Meta.Tactic.Grind.SimpUtil (1.9s) â [4535/4625] Built Lean.Meta.Tactic.Grind.ForallProp:c.o (2.2s) â [4536/4625] Built Lean.Meta.Tactic.Grind.SimpUtil:c.o (1.5s) â [4537/4625] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search:c.o (5.9s) â [4538/4625] Built Lean.Meta.Tactic.Grind.Core (9.3s) â [4539/4625] Built Lean.Meta.Tactic.Grind.Internalize:c.o (9.6s) â [4540/4625] Built Lean.Meta.Tactic.Grind.Core:c.o (3.7s) â [4541/4625] Built Lean.Meta.Tactic.Grind.Intro (4.9s) â [4542/4625] Built Lean.Meta.Tactic.Grind.EMatchAction (1.9s) â [4543/4625] Built Lean.Meta.Tactic.Grind.Intro:c.o (3.2s) â [4544/4625] Built Lean.Meta.Tactic.Grind.EMatchAction:c.o (1.7s) â [4545/4625] Built Lean.Meta.Tactic.Grind.Split (5.4s) â [4546/4625] Built Lean.Meta.Tactic.Grind.Finish (491ms) â [4547/4625] Built Lean.Meta.Tactic.Grind.Finish:c.o (189ms) â [4548/4625] Built Lean.Meta.Tactic.Grind.Solve (593ms) â [4549/4625] Built Lean.Meta.Tactic.Grind.Solve:c.o (154ms) â [4550/4625] Built Lean.Meta.Tactic.Grind.Lookahead (1.9s) â [4551/4625] Built Lean.Meta.Tactic.Grind.Lookahead:c.o (804ms) â [4552/4625] Built Lean.Meta.Tactic.Grind.Split:c.o (3.7s) â [4553/4625] Built Lean.Meta.Tactic.Grind.Main (4.3s) â [4554/4625] Built Lean.Meta.Sym.Grind (757ms) â [4555/4625] Built Lean.Meta.Sym (441ms) â [4556/4625] Built Lean.Meta.Sym.Grind:c.o (460ms) â [4557/4625] Built Lean.Meta.Sym:c.o (191ms) â [4558/4625] Built Lean.Meta.Tactic.Grind (1.4s) â [4559/4625] Built Lean.Meta.Tactic.Grind:c.o (463ms) â [4560/4625] Built Lean.Meta.Tactic.LibrarySearch (1.0s) â [4561/4625] Built Lean.Meta.Tactic.Try.Collect (1.7s) â [4562/4625] Built Lean.Elab.Tactic.LibrarySearch (1.9s) â [4563/4625] Built Lean.Meta.Tactic.LibrarySearch:c.o (2.1s) â [4564/4625] Built Lean.Elab.Tactic.Grind.Basic (4.3s) â [4565/4625] Built Lean.Meta.Tactic.Try (718ms) â [4566/4625] Built Lean.Meta.Tactic.Try:c.o (178ms) â [4567/4625] Built Lean.Meta.Tactic.Try.Collect:c.o (1.8s) â [4568/4625] Built Lean.Elab.Tactic.Grind.SimprocDSL (1.2s) â [4569/4625] Built Lean.Elab.Tactic.Grind.Filter (1.4s) â [4570/4625] Built Lean.Elab.Tactic.Grind.Have (1.8s) â [4571/4625] Built Lean.Elab.Tactic.Grind.Filter:c.o (540ms) â [4572/4625] Built Lean.Elab.Tactic.LibrarySearch:c.o (2.4s) â [4573/4625] Built Lean.Elab.Tactic.Grind.SimprocDSL:c.o (670ms) â [4574/4625] Built Lean.Elab.Tactic.Grind.RegisterSymSimp (1.2s) â [4575/4625] Built Lean.Elab.Tactic.Grind.Have:c.o (784ms) â [4576/4625] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin (1.3s) â [4577/4625] Built Lean.Meta.Tactic.Grind.Main:c.o (6.9s) â [4578/4625] Built Lean.Meta.Tactic.Cbv.Main (6.1s) â [4579/4625] Built Lean.Elab.Tactic.Grind.Config (3.3s) â [4580/4625] Built Lean.Elab.Tactic.Grind.RegisterSymSimp:c.o (878ms) â [4581/4625] Built Lean.Elab.Tactic.Grind.ShowState (1.0s) â [4582/4625] Built Lean.Meta.Tactic.Cbv (494ms) â [4583/4625] Built Lean.Meta.Tactic.Cbv:c.o (204ms) â [4584/4625] Built Lean.Elab.Tactic.Grind.Sym (2.4s) â [4585/4625] Built Lean.Elab.Tactic.Grind.Param (3.8s) â [4586/4625] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin:c.o (1.2s) â [4587/4625] Built Lean.Elab.Tactic.Conv.Cbv (949ms) â [4588/4625] Built Lean.Meta.Tactic (998ms) â [4589/4625] Built Lean.Elab.Tactic.Conv.Cbv:c.o (282ms) â [4590/4625] Built Lean.Meta.Tactic:c.o (254ms) â [4591/4625] Built Lean.Elab.Tactic.Grind.ShowState:c.o (1.8s) â [4592/4625] Built Lean.Elab.Tactic.Grind.Trace (1.3s) â [4593/4625] Built Lean.Elab.Tactic.Conv (932ms) â [4594/4625] Built Lean.Elab.Tactic.Conv:c.o (170ms) â [4595/4625] Built Lean.Elab.Tactic.Grind.Lint (2.3s) â [4596/4625] Built Lean.Meta (1.1s) â [4597/4625] Built Lean.Elab.Tactic.Grind.Trace:c.o (631ms) â [4598/4625] Built Lean.Meta:c.o (290ms) â [4599/4625] Built Lean.Elab.Tactic.Cbv (1.4s) â [4600/4625] Built Lean.Elab.Tactic.Grind.Basic:c.o (6.2s) â [4601/4625] Built Lean.Elab.Tactic.Grind.Sym:c.o (2.6s) â [4602/4625] Built Lean.Elab.Tactic.Cbv:c.o (641ms) â [4603/4625] Built Lean.Elab.Tactic.Grind.LintExceptions (1.1s) â [4604/4625] Built Lean.Elab.Tactic.Grind.LintExceptions:c.o (143ms) â [4605/4625] Built Lean.Elab.Tactic.Grind.Config:c.o (4.2s) â [4606/4625] Built Lean.Elab.Tactic.Grind.Lint:c.o (2.4s) â [4607/4625] Built Lean.Elab.Tactic.Grind.Param:c.o (4.3s) â [4608/4625] Built Lean.Elab.Tactic.Grind.BuiltinTactic (5.0s) â [4609/4625] Built Lean.Meta.Tactic.Cbv.Main:c.o (6.0s) â [4610/4625] Built Lean.Elab.Tactic.Grind.Main (7.3s) â [4611/4625] Built Lean.Elab.Tactic.Grind (729ms) â [4612/4625] Built Lean.Elab.Tactic.Grind:c.o (139ms) â [4613/4625] Built Lean.Elab.Tactic.Grind.BuiltinTactic:c.o (5.3s) â [4614/4625] Built Lean.Elab.Tactic.Grind.Main:c.o (5.8s) â [4615/4625] Built Lean.Elab.Tactic.Try (9.5s) â [4616/4625] Built Lean.Elab.Tactic (1.1s) â [4617/4625] Built Lean.Elab.Tactic:c.o (207ms) â [4618/4625] Built Lean.Elab (1.1s) â [4619/4625] Built Lean.Elab:c.o (186ms) â [4620/4625] Built Lean (1.2s) â [4621/4625] Built Lean:c.o (166ms) â [4622/4625] Built Lean.Elab.Tactic.Try:c.o (11s) â [4623/4625] Building Lean:static (42ms) 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 â [4624/4625] Building Lean:static (45ms) 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 - LeanIR:static - Std:static - Std: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[6]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/lean4-4.30.0/src' gmake[5]: *** [CMakeFiles/make_stdlib.dir/build.make:73: CMakeFiles/make_stdlib] Error 2 gmake[5]: Leaving directory '/wrkdirs/usr/ports/math/lean4/work/.build/stage1' gmake[4]: *** [CMakeFiles/Makefile2:1412: CMakeFiles/make_stdlib.dir/all] Error 2 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:139: 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 in /usr/ports/math/lean4
