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/5c01d7a330c3/logs/lean4-4.33.1.log Build URL: https://pkg-status.freebsd.org/beefy22/build.html?mastername=144amd64-default&build=5c01d7a330c3 Log: =>> Building math/lean4 build started at Tue Sep 8 15:39:54 UTC 2026 port directory: /usr/ports/math/lean4 package name: lean4-4.33.1 building for: FreeBSD 144amd64-default-job-23 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: 5c01d7a330c3ff8c750eea5c052c8db3165d7d00 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: 23 ---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/23/.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-23] Installing pkg-2.8.4... [144amd64-default-job-23] 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 => leanprover-lean4-v4.33.1_GH0.tar.gz doesn't seem to exist in /portdistfiles. => Attempting to fetch https://codeload.github.com/leanprover/lean4/tar.gz/v4.33.1?dummy=/leanprover-lean4-v4.33.1_GH0.tar.gz fetch: https://codeload.github.com/leanprover/lean4/tar.gz/v4.33.1?dummy=/leanprover-lean4-v4.33.1_GH0.tar.gz: size unknown fetch: https://codeload.github.com/leanprover/lean4/tar.gz/v4.33.1?dummy=/leanprover-lean4-v4.33.1_GH0.tar.gz: size of remote file is not known leanprover-lean4-v4.33.1_GH0.tar.gz 82 MB 3986 kBps 22s ===> 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: <snip> â [4827/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr (16s) â [4828/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action (586ms) â [4829/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.Action:c.o (209ms) â [4830/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof (11s) â [4831/4991] Built Lean.Meta.Tactic.Grind.Internalize (6.0s) â [4832/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing (767ms) â [4833/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq (5.7s) â [4834/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing:c.o (462ms) â [4835/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.StructId:c.o (8.2s) â [4836/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search (7.5s) â [4837/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr (2.5s) â [4838/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action (619ms) â [4839/4991] Built Lean.Meta.Tactic.Grind.ForallProp (2.8s) â [4840/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr (3.1s) â [4841/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Action:c.o (266ms) â [4842/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear (902ms) â [4843/4991] Built Lean.Meta.Tactic.Grind.Arith.Main (748ms) â [4844/4991] Built Lean.Meta.Tactic.Grind.AC.Eq:c.o (10s) â [4845/4991] Built Lean.Meta.Tactic.Grind.Arith.Main:c.o (342ms) â [4846/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear:c.o (441ms) â [4847/4991] Built Lean.Meta.Tactic.Grind.SimpUtil (1.7s) â [4848/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr:c.o (2.3s) â [4849/4991] Built Lean.Meta.Tactic.Grind.ForallProp:c.o (2.8s) â [4850/4991] Built Lean.Meta.Tactic.Grind.SimpUtil:c.o (1.6s) â [4851/4991] Built Lean.Meta.Tactic.Grind.Core (6.2s) â [4852/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr:c.o (3.9s) â [4853/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq:c.o (7.1s) â [4854/4991] Built Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr:c.o (10s) â [4855/4991] Built Lean.Meta.Tactic.Grind.Arith.Linear.Search:c.o (7.6s) â [4856/4991] Built Lean.Meta.Tactic.Grind.Intro (3.8s) â [4857/4991] Built Lean.Meta.Tactic.Grind.Internalize:c.o (11s) â [4858/4991] Built Lean.Meta.Tactic.Grind.Core:c.o (5.7s) â [4859/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr (8.9s) â [4860/4991] Built Lean.Meta.Tactic.Grind.EMatchAction (1.9s) â [4861/4991] Built Lean.Meta.Tactic.Grind.Intro:c.o (3.4s) â [4862/4991] Built Lean.Meta.Tactic.Grind.Split (3.9s) â [4863/4991] Built Lean.Meta.Tactic.Grind.EMatchAction:c.o (2.4s) â [4864/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars (2.4s) â [4865/4991] Built Lean.Meta.Tactic.Grind.Finish (601ms) â [4866/4991] Built Lean.Meta.Tactic.Grind.Finish:c.o (329ms) â [4867/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof:c.o (14s) â [4868/4991] Built Lean.Meta.Tactic.Grind.Solve (534ms) â [4869/4991] Built Lean.Meta.Tactic.Grind.Solve:c.o (204ms) â [4870/4991] Built Lean.Meta.Tactic.Grind.Lookahead (1.6s) â [4871/4991] Built Lean.Meta.Tactic.Grind.Lookahead:c.o (921ms) â [4872/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.ReorderVars:c.o (2.9s) â [4873/4991] Built Lean.Meta.Tactic.Grind.Split:c.o (4.6s) â [4874/4991] Built Lean.Meta.Tactic.Grind.Main (4.6s) â [4875/4991] Built Lean.Meta.Sym.Grind (770ms) â [4876/4991] Built Lean.Meta.Sym.Grind:c.o (699ms) â [4877/4991] Built Lean.Meta.Sym (700ms) â [4878/4991] Built Lean.Meta.Sym:c.o (176ms) â [4879/4991] Built Lean.Meta.Tactic.LibrarySearch (2.0s) â [4880/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Util (2.2s) â [4881/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr:c.o (10s) â [4882/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.EPost (1.1s) â [4883/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Util:c.o (1.3s) â [4884/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.EPost:c.o (1.1s) â [4885/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache (1.4s) â [4886/4991] Built Lean.Meta.Tactic.Try.Collect (1.7s) â [4887/4991] Built Lean.Elab.Tactic.LibrarySearch (2.1s) â [4888/4991] Built Lean.Meta.Tactic.Try (773ms) â [4889/4991] Built Lean.Elab.Tactic.Grind.Basic (4.6s) â [4890/4991] Built Lean.Meta.Tactic.Try:c.o (302ms) â [4891/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search (10s) â [4892/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache:c.o (1.2s) â [4893/4991] Built Lean.Meta.Tactic.LibrarySearch:c.o (2.0s) â [4894/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Entails (2.0s) â [4895/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action (796ms) â [4896/4991] Built Lean.Elab.Tactic.Grind.WithGrindTacticM (1.1s) â [4897/4991] Built Lean.Elab.Tactic.Grind.Filter (1.3s) â [4898/4991] Built Lean.Elab.Tactic.Grind.SimprocDSL (1.3s) â [4899/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSL (1.2s) â [4900/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Action:c.o (285ms) â [4901/4991] Built Lean.Elab.Tactic.Grind.WithGrindTacticM:c.o (378ms) â [4902/4991] Built Lean.Elab.Tactic.LibrarySearch:c.o (2.2s) â [4903/4991] Built Lean.Elab.Tactic.Grind.Have (1.8s) â [4904/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSL:c.o (533ms) â [4905/4991] Built Lean.Meta.Tactic.Try.Collect:c.o (2.7s) â [4906/4991] Built Lean.Elab.Tactic.Grind.Rewrite (1.8s) â [4907/4991] Built Lean.Elab.Tactic.Grind.SimprocDSL:c.o (703ms) â [4908/4991] Built Lean.Elab.Tactic.Grind.Filter:c.o (731ms) â [4909/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat (1.1s) â [4910/4991] Built Lean.Meta.Tactic.Cbv.Main (5.4s) â [4911/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSLBuiltin (1.2s) â [4912/4991] Built Lean.Elab.Tactic.Grind.RegisterSymSimp (1.2s) â [4913/4991] Built Lean.Elab.Tactic.Grind.RegisterSymDSimp (1.4s) â [4914/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat:c.o (480ms) â [4915/4991] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin (1.5s) â [4916/4991] Built Lean.Elab.Tactic.Grind.Have:c.o (1.1s) â [4917/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Entails:c.o (1.9s) â [4918/4991] Built Lean.Meta.Tactic.Grind.Arith (787ms) â [4919/4991] Built Lean.Meta.Tactic.Cbv (753ms) â [4920/4991] Built Lean.Elab.Tactic.Grind.DSimp (1.8s) â [4921/4991] Built Lean.Meta.Tactic.Grind.Main:c.o (7.8s) â [4922/4991] Built Lean.Elab.Tactic.Grind.Cbv (990ms) â [4923/4991] Built Lean.Elab.Tactic.Grind.RegisterSymDSimp:c.o (642ms) â [4924/4991] Built Lean.Meta.Tactic.Grind.Arith:c.o (246ms) â [4925/4991] Built Lean.Meta.Tactic.Cbv:c.o (326ms) â [4926/4991] Built Lean.Elab.Tactic.Grind.RegisterSymSimp:c.o (850ms) â [4927/4991] Built Lean.Elab.Tactic.Grind.DSimprocDSLBuiltin:c.o (840ms) â [4928/4991] Built Lean.Elab.Tactic.Grind.ShowState (2.1s) â [4929/4991] Built Lean.Elab.Tactic.Grind.Cbv:c.o (306ms) â [4930/4991] Built Lean.Elab.Tactic.Conv.Cbv (890ms) â [4931/4991] Built Lean.Elab.Tactic.Grind.Sym (2.6s) â [4932/4991] Built Lean.Elab.Tactic.Grind.SimprocDSLBuiltin:c.o (1.2s) â [4933/4991] Built Lean.Elab.Tactic.Grind.Param (4.1s) â [4934/4991] Built Lean.Meta.Tactic.Grind (1.4s) â [4935/4991] Built Lean.Elab.Tactic.Conv.Cbv:c.o (514ms) â [4936/4991] Built Lean.Elab.Tactic.Grind.Rewrite:c.o (2.6s) â [4937/4991] Built Lean.Elab.Tactic.Conv (797ms) â [4938/4991] Built Lean.Elab.Tactic.Grind.Config (4.7s) â [4939/4991] Built Lean.Elab.Tactic.Conv:c.o (187ms) â [4940/4991] Built Lean.Elab.Tactic.Grind.DSimp:c.o (1.8s) â [4941/4991] Built Lean.Meta.Tactic.Grind:c.o (772ms) â [4942/4991] Built Lean.Meta.Tactic (990ms) â [4943/4991] Built Lean.Meta.Tactic:c.o (256ms) â [4944/4991] Built Lean.Elab.Tactic.Grind.ShowState:c.o (2.5s) â [4945/4991] Built Lean.Elab.Tactic.Grind.Trace (1.7s) â [4946/4991] Built Lean.Meta (1.2s) â [4947/4991] Built Lean.Elab.Tactic.Grind.Sym:c.o (2.7s) â [4948/4991] Built Lean.Elab.Tactic.Cbv (1.4s) â [4949/4991] Built Lean.Elab.Tactic.Grind.Lint (2.1s) â [4950/4991] Built Lean.Meta:c.o (354ms) â [4951/4991] Built Lean.Elab.Tactic.Cbv:c.o (531ms) â [4952/4991] Built Lean.Elab.Tactic.Grind.Trace:c.o (962ms) â [4953/4991] Built Lean.Elab.Tactic.Grind.Basic:c.o (7.4s) â [4954/4991] Built Lean.Elab.Tactic.Grind.LintExceptions (862ms) â [4955/4991] Built Lean.Elab.Tactic.Grind.LintExceptions:c.o (136ms) â [4956/4991] Built Lean.Meta.Tactic.Cbv.Main:c.o (6.4s) â [4957/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Solve (8.3s) â [4958/4991] Built Lean.Elab.Tactic.Grind.BuiltinTactic (5.3s) â [4959/4991] Built Lean.Elab.Tactic.Grind.Param:c.o (6.1s) â [4960/4991] Built Lean.Elab.Tactic.Grind.Lint:c.o (3.4s) â [4961/4991] Built Lean.Meta.Tactic.Grind.Arith.Cutsat.Search:c.o (10s) â [4962/4991] Built Lean.Elab.Tactic.Grind.Main (6.5s) â [4963/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Driver (1.9s) â [4964/4991] Built Lean.Elab.Tactic.Grind (702ms) â [4965/4991] Built Lean.Elab.Tactic.Grind:c.o (215ms) â [4966/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Driver:c.o (2.2s) â [4967/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Solve:c.o (5.5s) â [4968/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Frontend (3.9s) â [4969/4991] Built Lean.Elab.Tactic.Grind.Config:c.o (10s) â [4970/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen (824ms) â [4971/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen:c.o (169ms) â [4972/4991] Built Lean.Elab.Tactic.Do.Internal (786ms) â [4973/4991] Built Lean.Elab.Tactic.Do.Internal:c.o (146ms) â [4974/4991] Built Lean.Elab.Tactic.Grind.Main:c.o (5.9s) â [4975/4991] Built Lean.Elab.Tactic.Do (900ms) â [4976/4991] Built Lean.Elab.Tactic.Do:c.o (201ms) â [4977/4991] Built Lean.Elab.Tactic.Grind.BuiltinTactic:c.o (8.5s) â [4978/4991] Built Lean.Elab.Tactic.Do.Internal.VCGen.Frontend:c.o (5.1s) â [4979/4991] Built Lean.Elab.Tactic.Try (9.2s) â [4980/4991] Built Lean.Elab.Tactic.AutoTry (2.8s) â [4981/4991] Built Lean.Elab.Tactic (1.2s) â [4982/4991] Built Lean.Elab.Tactic:c.o (332ms) â [4983/4991] Built Lean.Elab (1.0s) â [4984/4991] Built Lean.Elab:c.o (401ms) â [4985/4991] Built Lean (1.2s) â [4986/4991] Built Lean:c.o (213ms) â [4987/4991] Built Lean.Elab.Tactic.AutoTry:c.o (4.2s) â [4988/4991] Built Lean.Elab.Tactic.Try:c.o (10s) â [4989/4991] Building Lean:static (64ms) 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 (42ms) 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
