Building package "lean4-git" INFO: Starting build... INFO: Verifying bootstrap image /home/u726578/chaotic/cache/lower/20220808000251.sif WARNING: integrity: signature not found for object group 1 WARNING: Bootstrap image could not be verified, but build will continue. INFO: Creating sandbox directory... INFO: Build complete: /scratch/chaotic/sandbox/pkg5302b62f821 :: Synchronizing package databases... core downloading... extra downloading... community downloading... multilib downloading... chaotic-aur downloading... :: Starting full system upgrade... there is nothing to do resolving dependencies... looking for conflicting packages... Packages (4) perl-error-0.17029-4 perl-mailtools-2.21-6 perl-timedate-2.33-4 git-2.37.1-1 Total Installed Size: 34.70 MiB :: Proceed with installation? [Y/n] checking keyring... checking package integrity... loading package files... checking for file conflicts... checking available disk space... :: Processing package changes... installing perl-error... installing perl-timedate... installing perl-mailtools... installing git... Optional dependencies for git tk: gitk and git gui perl-libwww: git svn perl-term-readkey: git svn and interactive.singlekey setting perl-io-socket-ssl: git send-email TLS support perl-authen-sasl: git send-email TLS support perl-mediawiki-api: git mediawiki support perl-datetime-format-iso8601: git mediawiki support perl-lwp-protocol-https: git mediawiki https support perl-cgi: gitweb (web interface) support python: git svn & git p4 subversion: git svn org.freedesktop.secrets: keyring credential helper libsecret: libsecret credential helper [installed] :: Running post-transaction hooks... (1/4) Creating system user accounts... Creating group 'git' with GID 974. Creating user 'git' (git daemon user) with UID 974 and GID 974. (2/4) Reloading system manager configuration... Skipped: Current root is not booted. (3/4) Arming ConditionNeedsUpdate... (4/4) Warn about old perl modules warning: glibc-2.36-1 is up to date -- skipping warning: gmp-6.2.1-2 is up to date -- skipping warning: git-2.37.1-1 is up to date -- skipping resolving dependencies... looking for conflicting packages... Packages (6) hicolor-icon-theme-0.17-2 jsoncpp-1.9.5-2 libnsl-2.0.0-2 libuv-1.44.2-1 rhash-1.4.2-1 cmake-3.23.3-1 Total Installed Size: 66.06 MiB :: Proceed with installation? [Y/n] checking keyring... checking package integrity... loading package files... checking for file conflicts... checking available disk space... :: Processing package changes... installing hicolor-icon-theme... installing jsoncpp... Optional dependencies for jsoncpp jsoncpp-doc: documentation installing libnsl... installing libuv... installing rhash... installing cmake... Optional dependencies for cmake qt6-base: cmake-gui :: Running post-transaction hooks... (1/1) Arming ConditionNeedsUpdate... ==> Making package: lean4-git r25881.g81400109f3-1 (Mon 08 Aug 2022 09:04:46 AM -03) ==> Checking runtime dependencies... ==> Checking buildtime dependencies... ==> Retrieving sources... -> Updating lean4 git repo... From https://github.com/leanprover/lean4 - [deleted] (none) -> refs/pull/1407/merge 234212caee..8f4fe77acd gh-pages -> gh-pages fdaae20594..0204c5f9b7 master -> master + 4b9d4a9e7c...e29a97710b refs/pull/1257/merge -> refs/pull/1257/merge (forced update) + 31be3d62b8...54af42555a refs/pull/1318/merge -> refs/pull/1318/merge (forced update) + 03d6683344...c3e6166be1 refs/pull/1332/merge -> refs/pull/1332/merge (forced update) + c8e705511b...11493510e0 refs/pull/1356/head -> refs/pull/1356/head (forced update) + 8e5da131b4...5c77252f66 refs/pull/1356/merge -> refs/pull/1356/merge (forced update) 67429de6e7..eb1cee254e refs/pull/1407/head -> refs/pull/1407/head * [new ref] refs/pull/1423/head -> refs/pull/1423/head * [new ref] refs/pull/1424/head -> refs/pull/1424/head * [new ref] refs/pull/1425/head -> refs/pull/1425/head * [new ref] refs/pull/1427/head -> refs/pull/1427/head * [new ref] refs/pull/1428/head -> refs/pull/1428/head * [new ref] refs/pull/1430/head -> refs/pull/1430/head * [new ref] refs/pull/1431/head -> refs/pull/1431/head * [new ref] refs/pull/1432/head -> refs/pull/1432/head * [new ref] refs/pull/1434/head -> refs/pull/1434/head * [new ref] refs/pull/1437/head -> refs/pull/1437/head * [new ref] refs/pull/1439/head -> refs/pull/1439/head * [new ref] refs/pull/1440/head -> refs/pull/1440/head * [new ref] refs/pull/1442/head -> refs/pull/1442/head * [new ref] refs/pull/1442/merge -> refs/pull/1442/merge * [new ref] refs/pull/1444/head -> refs/pull/1444/head * [new ref] refs/pull/1444/merge -> refs/pull/1444/merge * [new ref] refs/pull/1445/head -> refs/pull/1445/head * [new ref] refs/pull/1445/merge -> refs/pull/1445/merge * [new ref] refs/pull/1446/head -> refs/pull/1446/head * [new ref] refs/pull/1446/merge -> refs/pull/1446/merge * [new ref] refs/pull/1447/head -> refs/pull/1447/head * [new ref] refs/pull/1447/merge -> refs/pull/1447/merge * [new tag] v4.0.0-m5 -> v4.0.0-m5 ==> WARNING: Skipping verification of source file PGP signatures. ==> Validating source files with sha256sums... lean4 ... Skipped ==> Extracting sources... -> Creating working copy of lean4 git repo... Cloning into 'lean4'... done. Updating files: 42% (1982/4702) Updating files: 43% (2022/4702) Updating files: 44% (2069/4702) Updating files: 45% (2116/4702) Updating files: 46% (2163/4702) Updating files: 47% (2210/4702) Updating files: 48% (2257/4702) Updating files: 48% (2270/4702) Updating files: 49% (2304/4702) Updating files: 50% (2351/4702) Updating files: 51% (2399/4702) Updating files: 52% (2446/4702) Updating files: 53% (2493/4702) Updating files: 54% (2540/4702) Updating files: 55% (2587/4702) Updating files: 56% (2634/4702) Updating files: 57% (2681/4702) Updating files: 58% (2728/4702) Updating files: 59% (2775/4702) Updating files: 60% (2822/4702) Updating files: 61% (2869/4702) Updating files: 62% (2916/4702) Updating files: 63% (2963/4702) Updating files: 64% (3010/4702) Updating files: 65% (3057/4702) Updating files: 66% (3104/4702) Updating files: 67% (3151/4702) Updating files: 68% (3198/4702) Updating files: 69% (3245/4702) Updating files: 70% (3292/4702) Updating files: 71% (3339/4702) Updating files: 72% (3386/4702) Updating files: 73% (3433/4702) Updating files: 74% (3480/4702) Updating files: 75% (3527/4702) Updating files: 76% (3574/4702) Updating files: 77% (3621/4702) Updating files: 78% (3668/4702) Updating files: 79% (3715/4702) Updating files: 80% (3762/4702) Updating files: 81% (3809/4702) Updating files: 82% (3856/4702) Updating files: 83% (3903/4702) Updating files: 84% (3950/4702) Updating files: 85% (3997/4702) Updating files: 86% (4044/4702) Updating files: 87% (4091/4702) Updating files: 88% (4138/4702) Updating files: 89% (4185/4702) Updating files: 90% (4232/4702) Updating files: 91% (4279/4702) Updating files: 92% (4326/4702) Updating files: 93% (4373/4702) Updating files: 94% (4420/4702) Updating files: 95% (4467/4702) Updating files: 96% (4514/4702) Updating files: 97% (4561/4702) Updating files: 98% (4608/4702) Updating files: 99% (4655/4702) Updating files: 100% (4702/4702) Updating files: 100% (4702/4702), done. ==> Starting pkgver()... ==> Updated version: lean4-git r29876.g0204c5f9b7-1 ==> Starting build()... -- The CXX compiler identification is GNU 12.1.1 -- The C compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/sbin/c++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/sbin/cc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Configuring done -- Generating done -- Build files have been written to: /home/main-builder/pkgwork/src/lean4/_build make: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' make[1]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' make[2]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' make[3]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' make[3]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' make[3]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' [ 4%] Creating directories for 'stage0' [ 8%] No download step for 'stage0' [ 12%] No update step for 'stage0' [ 16%] No patch step for 'stage0' [ 20%] Performing configure step for 'stage0' -- The CXX compiler identification is GNU 12.1.1 -- The C compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/sbin/c++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/sbin/cc - skipped -- Detecting C compile features -- Detecting C compile features - done -- No build type selected, default to Release -- 64-bit machine detected -- Found GMP: /usr/include (Required is at least version "5.0.5") CMake Warning at CMakeLists.txt:257 (message): Failed to find ccache, prepare for longer and redundant builds... -- Could NOT find PythonInterp (missing: PYTHON_EXECUTABLE) -- Configuring done -- Generating done CMake Warning: Manually-specified variables were not used by the project: CMAKE_EDIT_COMMAND -- Build files have been written to: /home/main-builder/pkgwork/src/lean4/_build/stage0 [ 25%] Performing build step for 'stage0' make[4]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[5]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[7]: Entering directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 2%] Building CXX object initialize/CMakeFiles/initialize.dir/init.cpp.o [ 2%] Building CXX object kernel/CMakeFiles/kernel.dir/level.cpp.o [ 2%] Building CXX object library/CMakeFiles/library.dir/expr_lt.cpp.o make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 3%] Building CXX object library/compiler/CMakeFiles/compiler.dir/init_module.cpp.o [ 3%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/debug.cpp.o make[8]: Entering directory '/home/main-builder/pkgwork/src/lean4/stage0/src' [ 4%] Building CXX object library/constructions/CMakeFiles/constructions.dir/rec_on.cpp.o [ 5%] Building CXX object util/CMakeFiles/util.dir/name.cpp.o [ ] Building ../stdlib//Init/WFTactics.c [ 6%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/thread.cpp.o make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 6%] Built target initialize [ ] Building ../stdlib//Init/WF.c [ 7%] Building CXX object library/CMakeFiles/library.dir/bin_app.cpp.o [ 8%] Building CXX object library/CMakeFiles/library.dir/constants.cpp.o [ 9%] Building CXX object library/compiler/CMakeFiles/compiler.dir/compiler.cpp.o [ 10%] Building CXX object library/constructions/CMakeFiles/constructions.dir/cases_on.cpp.o [ 10%] Building CXX object util/CMakeFiles/util.dir/name_set.cpp.o [ ] Building ../stdlib//Init/Util.c [ 11%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/mpz.cpp.o [ 11%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/utf8.cpp.o [ 12%] Building CXX object util/CMakeFiles/util.dir/escaped.cpp.o [ 13%] Building CXX object library/CMakeFiles/library.dir/max_sharing.cpp.o [ ] Building ../stdlib//Init/Tactics.c [ 14%] Building CXX object util/CMakeFiles/util.dir/bit_tricks.cpp.o [ 15%] Building CXX object library/compiler/CMakeFiles/compiler.dir/util.cpp.o In file included from /usr/include/c++/12.1.1/memory:76, from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:7: In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp: In function ‘void lean::display(std::ostream&, const __mpz_struct*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp: In function ‘void lean::display(std::ostream&, const __mpz_struct*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ In function ‘void lean::display(std::ostream&, const __mpz_struct*)’, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ In function ‘void lean::display(std::ostream&, const __mpz_struct*)’, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ [ 16%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/object.cpp.o [ 16%] Building CXX object util/CMakeFiles/util.dir/ascii.cpp.o [ 17%] Building CXX object util/CMakeFiles/util.dir/path.cpp.o [ 17%] Building CXX object kernel/CMakeFiles/kernel.dir/expr.cpp.o [ 17%] Building CXX object library/CMakeFiles/library.dir/module.cpp.o [ 17%] Building CXX object library/constructions/CMakeFiles/constructions.dir/no_confusion.cpp.o [ 18%] Building CXX object util/CMakeFiles/util.dir/lbool.cpp.o [ 19%] Building CXX object util/CMakeFiles/util.dir/init_module.cpp.o [ 19%] Building CXX object util/CMakeFiles/util.dir/list_fn.cpp.o [ 20%] Building CXX object library/CMakeFiles/library.dir/replace_visitor.cpp.o [ 21%] Building CXX object library/CMakeFiles/library.dir/num.cpp.o [ 22%] Building CXX object kernel/CMakeFiles/kernel.dir/expr_eq_fn.cpp.o [ 23%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/apply.cpp.o [ 24%] Building CXX object util/CMakeFiles/util.dir/timeit.cpp.o [ 25%] Building CXX object util/CMakeFiles/util.dir/timer.cpp.o [ 25%] Building CXX object util/CMakeFiles/util.dir/name_generator.cpp.o [ 25%] Building CXX object library/CMakeFiles/library.dir/class.cpp.o [ 26%] Building CXX object library/constructions/CMakeFiles/constructions.dir/projection.cpp.o [ 27%] Building CXX object kernel/CMakeFiles/kernel.dir/for_each_fn.cpp.o [ 28%] Building CXX object library/CMakeFiles/library.dir/util.cpp.o [ 28%] Building CXX object library/compiler/CMakeFiles/compiler.dir/lcnf.cpp.o [ 29%] Building CXX object library/CMakeFiles/library.dir/print.cpp.o [ ] Building ../stdlib//Init/System/ST.c [ 30%] Building CXX object util/CMakeFiles/util.dir/kvmap.cpp.o [ ] Building ../stdlib//Init/System/Platform.c [ ] Building ../stdlib//Init/System/IOError.c [ 31%] Building CXX object kernel/CMakeFiles/kernel.dir/replace_fn.cpp.o [ 32%] Building CXX object library/constructions/CMakeFiles/constructions.dir/brec_on.cpp.o [ ] Building ../stdlib//Init/System/IO.c [ 33%] Building CXX object util/CMakeFiles/util.dir/map_foreach.cpp.o [ 34%] Building CXX object util/CMakeFiles/util.dir/options.cpp.o [ 34%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/exception.cpp.o [ 34%] Building CXX object kernel/CMakeFiles/kernel.dir/abstract.cpp.o [ 35%] Building CXX object library/compiler/CMakeFiles/compiler.dir/csimp.cpp.o [ 36%] Building CXX object library/CMakeFiles/library.dir/annotation.cpp.o [ 36%] Building CXX object util/CMakeFiles/util.dir/format.cpp.o [ 37%] Building CXX object library/constructions/CMakeFiles/constructions.dir/init_module.cpp.o [ 38%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/interrupt.cpp.o [ 39%] Building CXX object kernel/CMakeFiles/kernel.dir/instantiate.cpp.o [ 40%] Building CXX object library/compiler/CMakeFiles/compiler.dir/elim_dead_let.cpp.o [ 40%] Building CXX object library/constructions/CMakeFiles/constructions.dir/util.cpp.o [ 41%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/memory.cpp.o [ 41%] Building CXX object library/CMakeFiles/library.dir/protected.cpp.o [ 42%] Building CXX object util/CMakeFiles/util.dir/option_declarations.cpp.o [ 43%] Building CXX object kernel/CMakeFiles/kernel.dir/local_ctx.cpp.o [ 44%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/stackinfo.cpp.o [ ] Building ../stdlib//Init/System/FilePath.c make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 44%] Built target constructions [ 44%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/compact.cpp.o [ 45%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/init_module.cpp.o [ 46%] Building CXX object library/CMakeFiles/library.dir/reducible.cpp.o make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 47%] Building CXX object runtime/CMakeFiles/leanrt.dir/debug.cpp.o [ 48%] Building CXX object util/CMakeFiles/util.dir/shell.cpp.o [ ] Building ../stdlib//Init/System.c [ 48%] Building CXX object kernel/CMakeFiles/kernel.dir/declaration.cpp.o [ ] Building ../stdlib//Init/SizeOfLemmas.c [ ] Building ../stdlib//Init/SizeOf.c [ 49%] Building CXX object runtime/CMakeFiles/leanrt.dir/thread.cpp.o /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.cpp: In member function ‘void lean::object_compactor::insert_mpz(lean::object*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.cpp:264:11: warning: ‘void* memcpy(void*, const void*, size_t)’ writing to an object of type ‘struct lean::mpz_object’ with no trivial copy-assignment; use copy-assignment or copy-initialization instead [-Wclass-memaccess] 264 | memcpy(new_o, to_mpz(o), sizeof(mpz_object)); | ~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In file included from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.h:11, from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.cpp:14: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object.h:26:8: note: ‘struct lean::mpz_object’ declared here 26 | struct mpz_object { | ^~~~~~~~~~ make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 50%] Building CXX object shell/CMakeFiles/shell.dir/lean.cpp.o [ ] Building ../stdlib//Init/SimpLemmas.c make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 50%] Built target shell [ 51%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/load_dynlib.cpp.o [ ] Building ../stdlib//Init/Prelude.c [ 52%] Building CXX object library/CMakeFiles/library.dir/init_module.cpp.o [ 53%] Building CXX object library/CMakeFiles/library.dir/projection.cpp.o [ 54%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/io.cpp.o [ 54%] Building CXX object runtime/CMakeFiles/leanrt.dir/mpz.cpp.o [ 55%] Building CXX object runtime/CMakeFiles/leanrt.dir/utf8.cpp.o [ 56%] Building CXX object kernel/CMakeFiles/kernel.dir/environment.cpp.o In file included from /usr/include/c++/12.1.1/memory:76, from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:7: In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp: In function ‘void lean::display(std::ostream&, const __mpz_struct*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp: In function ‘void lean::display(std::ostream&, const __mpz_struct*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ In function ‘void lean::display(std::ostream&, const __mpz_struct*)’, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ In member function ‘void std::default_delete<_Tp>::operator()(_Tp*) const [with _Tp = char]’, inlined from ‘std::unique_ptr<_Tp, _Dp>::~unique_ptr() [with _Tp = char; _Dp = std::default_delete]’ at /usr/include/c++/12.1.1/bits/unique_ptr.h:396:17, inlined from ‘void lean::display(std::ostream&, const __mpz_struct*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:251:5, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /usr/include/c++/12.1.1/bits/unique_ptr.h:95:9: warning: ‘void operator delete(void*, std::size_t)’ called on pointer returned from a mismatched allocation function [-Wmismatched-new-delete] 95 | delete __ptr; | ^~~~~~~~~~~~ In function ‘void lean::display(std::ostream&, const __mpz_struct*)’, inlined from ‘std::ostream& lean::operator<<(std::ostream&, const mpz&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:255:12: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpz.cpp:248:49: note: returned from ‘void* operator new [](std::size_t)’ 248 | std::unique_ptr buffer(new char[sz]); | ^ [ 56%] Building CXX object library/CMakeFiles/library.dir/aux_recursors.cpp.o [ 57%] Building CXX object library/compiler/CMakeFiles/compiler.dir/cse.cpp.o [ 57%] Building CXX object library/compiler/CMakeFiles/compiler.dir/erase_irrelevant.cpp.o [ 57%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/hash.cpp.o [ 58%] Building CXX object runtime/CMakeFiles/leanrt.dir/object.cpp.o [ 59%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/platform.cpp.o [ 60%] Building CXX object library/CMakeFiles/library.dir/trace.cpp.o [ 61%] Building CXX object util/CMakeFiles/util.dir/ffi.cpp.o [ 62%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/alloc.cpp.o make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 62%] Built target util [ 62%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/allocprof.cpp.o [ 63%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/sharecommon.cpp.o [ 64%] Building CXX object kernel/CMakeFiles/kernel.dir/type_checker.cpp.o [ 65%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/stack_overflow.cpp.o [ 66%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/process.cpp.o [ 67%] Building CXX object library/CMakeFiles/library.dir/profiling.cpp.o [ ] Building ../stdlib//Init/NotationExtra.c [ 67%] Building CXX object library/CMakeFiles/library.dir/time_task.cpp.o [ 67%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/object_ref.cpp.o [ 68%] Building CXX object library/compiler/CMakeFiles/compiler.dir/specialize.cpp.o [ 69%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/mpn.cpp.o [ 70%] Building CXX object library/compiler/CMakeFiles/compiler.dir/lambda_lifting.cpp.o /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp: In function ‘void lean::mpn_add(const mpn_digit*, size_t, const mpn_digit*, size_t, mpn_digit*, size_t, size_t*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp:51:43: warning: unused parameter ‘lngc_alloc’ [-Wunused-parameter] 51 | mpn_digit * c, size_t const lngc_alloc, | ~~~~~~~~~~~~~^~~~~~~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp: In function ‘void lean::div_n(mpn_buffer&, const mpn_buffer&, mpn_digit*, mpn_digit*, mpn_buffer&, mpn_buffer&)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp:224:49: warning: unused parameter ‘rem’ [-Wunused-parameter] 224 | mpn_digit * quot, mpn_digit * rem, | ~~~~~~~~~~~~^~~ [ 71%] Building CXX object runtime/CMakeFiles/leanrt.dir/apply.cpp.o [ 72%] Linking CXX static library libleanrt_initial-exec.a make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 72%] Built target leanrt_initial-exec [ 72%] Building CXX object runtime/CMakeFiles/leanrt.dir/exception.cpp.o [ 73%] Building CXX object library/CMakeFiles/library.dir/formatter.cpp.o [ 74%] Building CXX object runtime/CMakeFiles/leanrt.dir/interrupt.cpp.o [ 74%] Building CXX object library/compiler/CMakeFiles/compiler.dir/extract_closed.cpp.o [ 75%] Building CXX object library/compiler/CMakeFiles/compiler.dir/simp_app_args.cpp.o [ 76%] Building CXX object kernel/CMakeFiles/kernel.dir/init_module.cpp.o [ 77%] Building CXX object runtime/CMakeFiles/leanrt.dir/memory.cpp.o make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 77%] Built target library [ 77%] Building CXX object kernel/CMakeFiles/kernel.dir/expr_cache.cpp.o [ 77%] Building CXX object runtime/CMakeFiles/leanrt.dir/stackinfo.cpp.o [ 78%] Building CXX object kernel/CMakeFiles/kernel.dir/equiv_manager.cpp.o [ 79%] Building CXX object kernel/CMakeFiles/kernel.dir/quot.cpp.o [ 80%] Building CXX object library/compiler/CMakeFiles/compiler.dir/llnf.cpp.o [ 81%] Building CXX object runtime/CMakeFiles/leanrt.dir/compact.cpp.o [ 81%] Building CXX object kernel/CMakeFiles/kernel.dir/inductive.cpp.o /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.cpp: In member function ‘void lean::object_compactor::insert_mpz(lean::object*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.cpp:264:11: warning: ‘void* memcpy(void*, const void*, size_t)’ writing to an object of type ‘struct lean::mpz_object’ with no trivial copy-assignment; use copy-assignment or copy-initialization instead [-Wclass-memaccess] 264 | memcpy(new_o, to_mpz(o), sizeof(mpz_object)); | ~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In file included from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.h:11, from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/compact.cpp:14: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object.h:26:8: note: ‘struct lean::mpz_object’ declared here 26 | struct mpz_object { | ^~~~~~~~~~ [ 82%] Building CXX object library/compiler/CMakeFiles/compiler.dir/ll_infer_type.cpp.o [ 82%] Building CXX object library/compiler/CMakeFiles/compiler.dir/reduce_arity.cpp.o [ 83%] Building CXX object runtime/CMakeFiles/leanrt.dir/init_module.cpp.o [ 84%] Building CXX object runtime/CMakeFiles/leanrt.dir/load_dynlib.cpp.o [ 84%] Building CXX object runtime/CMakeFiles/leanrt.dir/io.cpp.o [ 85%] Building CXX object runtime/CMakeFiles/leanrt.dir/hash.cpp.o [ 86%] Building CXX object runtime/CMakeFiles/leanrt.dir/platform.cpp.o [ 86%] Building CXX object runtime/CMakeFiles/leanrt.dir/alloc.cpp.o [ 87%] Building CXX object library/compiler/CMakeFiles/compiler.dir/closed_term_cache.cpp.o [ 88%] Building CXX object runtime/CMakeFiles/leanrt.dir/allocprof.cpp.o [ 89%] Building CXX object runtime/CMakeFiles/leanrt.dir/sharecommon.cpp.o [ 90%] Building CXX object runtime/CMakeFiles/leanrt.dir/stack_overflow.cpp.o [ ] Building ../stdlib//Init/Notation.c [ 91%] Building CXX object library/compiler/CMakeFiles/compiler.dir/export_attribute.cpp.o [ 91%] Building CXX object runtime/CMakeFiles/leanrt.dir/process.cpp.o [ 92%] Building CXX object runtime/CMakeFiles/leanrt.dir/object_ref.cpp.o [ 92%] Building CXX object library/compiler/CMakeFiles/compiler.dir/extern_attribute.cpp.o [ 93%] Building CXX object library/compiler/CMakeFiles/compiler.dir/borrowed_annotation.cpp.o [ 94%] Building CXX object runtime/CMakeFiles/leanrt.dir/mpn.cpp.o [ 95%] Building CXX object library/compiler/CMakeFiles/compiler.dir/init_attribute.cpp.o [ ] Building ../stdlib//Init/Meta.c /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp: In function ‘void lean::mpn_add(const mpn_digit*, size_t, const mpn_digit*, size_t, mpn_digit*, size_t, size_t*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp:51:43: warning: unused parameter ‘lngc_alloc’ [-Wunused-parameter] 51 | mpn_digit * c, size_t const lngc_alloc, | ~~~~~~~~~~~~~^~~~~~~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp: In function ‘void lean::div_n(mpn_buffer&, const mpn_buffer&, mpn_digit*, mpn_digit*, mpn_buffer&, mpn_buffer&)’: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/mpn.cpp:224:49: warning: unused parameter ‘rem’ [-Wunused-parameter] 224 | mpn_digit * quot, mpn_digit * rem, | ~~~~~~~~~~~~^~~ In file included from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object_ref.h:10, from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/string_ref.h:10, from /home/main-builder/pkgwork/src/lean4/stage0/src/util/name.h:14, from /home/main-builder/pkgwork/src/lean4/stage0/src/util/name_generator.h:8, from /home/main-builder/pkgwork/src/lean4/stage0/src/kernel/inductive.cpp:9: In function ‘void lean::dec(object*)’, inlined from ‘lean::object_ref::~object_ref()’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object_ref.h:24:24, inlined from ‘lean::expr::~expr()’ at /home/main-builder/pkgwork/src/lean4/stage0/src/kernel/expr.h:86:7, inlined from ‘lean::optional& lean::optional::operator=(T&&) [with T = lean::expr]’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/optional.h:99:23, inlined from ‘lean::optional lean::elim_nested_inductive_fn::replace_if_nested(const lean::local_ctx&, const lean::buffer&, const lean::expr&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/kernel/inductive.cpp:999:94: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object.h:56:39: warning: ‘*(lean::object_ref*)((char*)&result + offsetof(lean::optional,lean::optional::)).lean::object_ref::m_obj’ may be used uninitialized [-Wmaybe-uninitialized] 56 | inline void dec(object * o) { lean_dec(o); } | ~~~~~~~~^~~ /home/main-builder/pkgwork/src/lean4/stage0/src/kernel/inductive.cpp: In member function ‘lean::optional lean::elim_nested_inductive_fn::replace_if_nested(const lean::local_ctx&, const lean::buffer&, const lean::expr&)’: /home/main-builder/pkgwork/src/lean4/stage0/src/kernel/inductive.cpp:982:28: note: ‘*(lean::object_ref*)((char*)&result + offsetof(lean::optional,lean::optional::)).lean::object_ref::m_obj’ was declared here 982 | optional result; | ^~~~~~ [ 96%] Building CXX object library/compiler/CMakeFiles/compiler.dir/eager_lambda_lifting.cpp.o [ 96%] Building CXX object library/compiler/CMakeFiles/compiler.dir/struct_cases_on.cpp.o [ 97%] Building CXX object library/compiler/CMakeFiles/compiler.dir/find_jp.cpp.o [ ] Building ../stdlib//Init/Hints.c [ 97%] Linking CXX static library ../lib/lean/libleanrt.a make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 97%] Built target leanrt [ ] Building ../stdlib//Init/Data/UInt.c [ 98%] Building CXX object library/compiler/CMakeFiles/compiler.dir/ir.cpp.o make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 98%] Built target kernel [ ] Building ../stdlib//Init/Data/ToString/Macro.c [ ] Building ../stdlib//Init/Data/ToString/Basic.c [ ] Building ../stdlib//Init/Data/ToString.c [ ] Building ../stdlib//Init/Data/String/Extra.c [ ] Building ../stdlib//Init/Data/String/Basic.c [ ] Building ../stdlib//Init/Data/String.c [ ] Building ../stdlib//Init/Data/Stream.c [ 98%] Building CXX object library/compiler/CMakeFiles/compiler.dir/implemented_by_attribute.cpp.o [ 99%] Building CXX object library/compiler/CMakeFiles/compiler.dir/ir_interpreter.cpp.o [ ] Building ../stdlib//Init/Data/Repr.c [ ] Building ../stdlib//Init/Data/Range.c [ ] Building ../stdlib//Init/Data/Random.c [ ] Building ../stdlib//Init/Data/Prod.c [ ] Building ../stdlib//Init/Data/Ord.c [ ] Building ../stdlib//Init/Data/Option/Instances.c [ ] Building ../stdlib//Init/Data/Option/BasicAux.c [ ] Building ../stdlib//Init/Data/Option/Basic.c [ ] Building ../stdlib//Init/Data/Option.c [ ] Building ../stdlib//Init/Data/OfScientific.c [ ] Building ../stdlib//Init/Data/Nat/SOM.c [ ] Building ../stdlib//Init/Data/Nat/Log2.c [ ] Building ../stdlib//Init/Data/Nat/Linear.c [ ] Building ../stdlib//Init/Data/Nat/Gcd.c [ ] Building ../stdlib//Init/Data/Nat/Div.c [ ] Building ../stdlib//Init/Data/Nat/Control.c [ ] Building ../stdlib//Init/Data/Nat/Bitwise.c [ ] Building ../stdlib//Init/Data/Nat/Basic.c [ ] Building ../stdlib//Init/Data/Nat.c [ ] Building ../stdlib//Init/Data/List/Control.c [ ] Building ../stdlib//Init/Data/List/BasicAux.c [ ] Building ../stdlib//Init/Data/List/Basic.c [ ] Building ../stdlib//Init/Data/List.c [ ] Building ../stdlib//Init/Data/Int/Basic.c [ ] Building ../stdlib//Init/Data/Int.c [ ] Building ../stdlib//Init/Data/Hashable.c [ ] Building ../stdlib//Init/Data/Format/Syntax.c [ ] Building ../stdlib//Init/Data/Format/Macro.c [ ] Building ../stdlib//Init/Data/Format/Instances.c [ ] Building ../stdlib//Init/Data/Format/Basic.c [ ] Building ../stdlib//Init/Data/Format.c [ ] Building ../stdlib//Init/Data/FloatArray/Basic.c In static member function ‘static lean::object* lean::ir::interpreter::stub_m_aux(lean::object**)’, inlined from ‘static lean::object* lean::ir::interpreter::stub_1_aux(lean::object*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:898:105: /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:891:29: warning: array subscript 1 is outside array bounds of ‘lean::object* [1]’ {aka ‘lean_object* [1]’} [-Warray-bounds] 891 | options opts(args[1]); | ^ /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp: In static member function ‘static lean::object* lean::ir::interpreter::stub_1_aux(lean::object*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:898:57: note: at offset 8 into object ‘args’ of size 8 898 | static object * stub_1_aux(object * x_1) { object * args[] = { x_1 }; return interpreter::stub_m_aux(args); } | ^~~~ In file included from /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/option_ref.h:8, from /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:41: In member function ‘lean::object* lean::object_ref::raw() const’, inlined from ‘const T& lean::cnstr_get_ref_t(const object_ref&, unsigned int) [with T = name]’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object_ref.h:142:48, inlined from ‘const lean::ir::fun_id& lean::ir::decl_fun_id(const decl&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:178:76, inlined from ‘static lean::object* lean::ir::interpreter::stub_m_aux(lean::object**)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:892:65, inlined from ‘static lean::object* lean::ir::interpreter::stub_1_aux(lean::object*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:898:105: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object_ref.h:38:35: warning: array subscript 2 is outside array bounds of ‘lean::object* [1]’ {aka ‘lean_object* [1]’} [-Warray-bounds] 38 | object * raw() const { return m_obj; } | ^~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp: In static member function ‘static lean::object* lean::ir::interpreter::stub_1_aux(lean::object*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:898:57: note: at offset 16 into object ‘args’ of size 8 898 | static object * stub_1_aux(object * x_1) { object * args[] = { x_1 }; return interpreter::stub_m_aux(args); } | ^~~~ [ ] Building ../stdlib//Init/Data/FloatArray.c [ ] Building ../stdlib//Init/Data/Float.c [ ] Building ../stdlib//Init/Data/Fin/Basic.c In member function ‘lean::object* lean::object_ref::raw() const’, inlined from ‘const T& lean::cnstr_get_ref_t(const object_ref&, unsigned int) [with T = name]’ at /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object_ref.h:142:48, inlined from ‘const lean::ir::fun_id& lean::ir::decl_fun_id(const decl&)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:178:76, inlined from ‘static lean::object* lean::ir::interpreter::stub_m_aux(lean::object**)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:892:65, inlined from ‘static lean::object* lean::ir::interpreter::stub_2_aux(lean::object*, lean::object*)’ at /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:899:124: /home/main-builder/pkgwork/src/lean4/stage0/src/runtime/object_ref.h:38:35: warning: array subscript 2 is outside array bounds of ‘lean::object* [2]’ {aka ‘lean_object* [2]’} [-Warray-bounds] 38 | object * raw() const { return m_obj; } | ^~~~~ /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp: In static member function ‘static lean::object* lean::ir::interpreter::stub_2_aux(lean::object*, lean::object*)’: /home/main-builder/pkgwork/src/lean4/stage0/src/library/compiler/ir_interpreter.cpp:899:71: note: at offset 16 into object ‘args’ of size 16 899 | static object * stub_2_aux(object * x_1, object * x_2) { object * args[] = { x_1, x_2 }; return interpreter::stub_m_aux(args); } | ^~~~ make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ ] Building ../stdlib//Init/Data/Fin.c [ 99%] Built target compiler make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [100%] Linking CXX static library lib/lean/libleancpp.a [ ] Building ../stdlib//Init/Data/Char/Basic.c [ ] Building ../stdlib//Init/Data/Char.c make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [100%] Built target leancpp [ ] Building ../stdlib//Init/Data/ByteArray/Basic.c [ ] Building ../stdlib//Init/Data/ByteArray.c [ ] Building ../stdlib//Init/Data/Basic.c [ ] Building ../stdlib//Init/Data/Array/Subarray.c [ ] Building ../stdlib//Init/Data/Array/QSort.c [ ] Building ../stdlib//Init/Data/Array/Mem.c [ ] Building ../stdlib//Init/Data/Array/InsertionSort.c [ ] Building ../stdlib//Init/Data/Array/DecidableEq.c [ ] Building ../stdlib//Init/Data/Array/BinSearch.c [ ] Building ../stdlib//Init/Data/Array/BasicAux.c [ ] Building ../stdlib//Init/Data/Array/Basic.c [ ] Building ../stdlib//Init/Data/Array.c [ ] Building ../stdlib//Init/Data/AC.c [ ] Building ../stdlib//Init/Data.c [ ] Building ../stdlib//Init/Core.c [ ] Building ../stdlib//Init/Conv.c [ ] Building ../stdlib//Init/Control/StateRef.c [ ] Building ../stdlib//Init/Control/StateCps.c [ ] Building ../stdlib//Init/Control/State.c [ ] Building ../stdlib//Init/Control/Reader.c [ ] Building ../stdlib//Init/Control/Option.c [ ] Building ../stdlib//Init/Control/Lawful.c [ ] Building ../stdlib//Init/Control/Id.c [ ] Building ../stdlib//Init/Control/ExceptCps.c [ ] Building ../stdlib//Init/Control/Except.c [ ] Building ../stdlib//Init/Control/EState.c [ ] Building ../stdlib//Init/Control/Basic.c [ ] Building ../stdlib//Init/Control.c [ ] Building ../stdlib//Init/Coe.c [ ] Building ../stdlib//Init/Classical.c [ ] Building ../stdlib//Init.c make[8]: Leaving directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[8]: Entering directory '/home/main-builder/pkgwork/src/lean4/stage0/src' [ ] Building ../stdlib//Std/ShareCommon.c [ ] Building ../stdlib//Std/Data/Stack.c [ ] Building ../stdlib//Std/Data/RBTree.c [ ] Building ../stdlib//Std/Data/RBMap.c [ ] Building ../stdlib//Std/Data/Queue.c [ ] Building ../stdlib//Std/Data/PersistentHashSet.c [ ] Building ../stdlib//Std/Data/PersistentHashMap.c [ ] Building ../stdlib//Std/Data/PersistentArray.c [ ] Building ../stdlib//Std/Data/HashSet.c [ ] Building ../stdlib//Std/Data/HashMap.c [ ] Building ../stdlib//Std/Data/DList.c [ ] Building ../stdlib//Std/Data/BinomialHeap.c [ ] Building ../stdlib//Std/Data/AssocList.c [ ] Building ../stdlib//Std/Data.c [ ] Building ../stdlib//Std.c make[8]: Leaving directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[8]: Entering directory '/home/main-builder/pkgwork/src/lean4/stage0/src' [ ] Building ../stdlib//Lean/Widget/UserWidget.c [ ] Building ../stdlib//Lean/Widget/TaggedText.c [ ] Building ../stdlib//Lean/Widget/InteractiveGoal.c [ ] Building ../stdlib//Lean/Widget/InteractiveDiagnostic.c [ ] Building ../stdlib//Lean/Widget/InteractiveCode.c [ ] Building ../stdlib//Lean/Widget/Basic.c [ ] Building ../stdlib//Lean/Widget.c [ ] Building ../stdlib//Lean/Util/Trace.c [ ] Building ../stdlib//Lean/Util/Sorry.c [ ] Building ../stdlib//Lean/Util/SCC.c [ ] Building ../stdlib//Lean/Util/ReplaceLevel.c [ ] Building ../stdlib//Lean/Util/ReplaceExpr.c [ ] Building ../stdlib//Lean/Util/Recognizers.c [ ] Building ../stdlib//Lean/Util/RecDepth.c [ ] Building ../stdlib//Lean/Util/Profile.c [ ] Building ../stdlib//Lean/Util/Paths.c [ ] Building ../stdlib//Lean/Util/Path.c [ ] Building ../stdlib//Lean/Util/PPExt.c [ ] Building ../stdlib//Lean/Util/OccursCheck.c [ ] Building ../stdlib//Lean/Util/MonadCache.c [ ] Building ../stdlib//Lean/Util/MonadBacktrack.c [ ] Building ../stdlib//Lean/Util/HasConstCache.c [ ] Building ../stdlib//Lean/Util/ForEachExpr.c [ ] Building ../stdlib//Lean/Util/FoldConsts.c [ ] Building ../stdlib//Lean/Util/FindMVar.c [ ] Building ../stdlib//Lean/Util/FindLevelMVar.c [ ] Building ../stdlib//Lean/Util/FindExpr.c [ ] Building ../stdlib//Lean/Util/CollectMVars.c [ ] Building ../stdlib//Lean/Util/CollectLevelParams.c [ ] Building ../stdlib//Lean/Util/CollectFVars.c [ ] Building ../stdlib//Lean/Util.c [ ] Building ../stdlib//Lean/ToExpr.c [ ] Building ../stdlib//Lean/Syntax.c [ ] Building ../stdlib//Lean/SubExpr.c [ ] Building ../stdlib//Lean/Structure.c [ ] Building ../stdlib//Lean/Server/Watchdog.c [ ] Building ../stdlib//Lean/Server/Utils.c [ ] Building ../stdlib//Lean/Server/Snapshots.c [ ] Building ../stdlib//Lean/Server/Rpc/RequestHandling.c [ ] Building ../stdlib//Lean/Server/Rpc/Deriving.c [ ] Building ../stdlib//Lean/Server/Rpc/Basic.c [ ] Building ../stdlib//Lean/Server/Rpc.c [ ] Building ../stdlib//Lean/Server/Requests.c [ ] Building ../stdlib//Lean/Server/References.c [ ] Building ../stdlib//Lean/Server/InfoUtils.c [ ] Building ../stdlib//Lean/Server/GoTo.c [ ] Building ../stdlib//Lean/Server/FileWorker/WidgetRequests.c [ ] Building ../stdlib//Lean/Server/FileWorker/Utils.c [ ] Building ../stdlib//Lean/Server/FileWorker/RequestHandling.c [ ] Building ../stdlib//Lean/Server/FileWorker.c [ ] Building ../stdlib//Lean/Server/FileSource.c [ ] Building ../stdlib//Lean/Server/Completion.c [ ] Building ../stdlib//Lean/Server/AsyncList.c [ ] Building ../stdlib//Lean/Server.c [ ] Building ../stdlib//Lean/ScopedEnvExtension.c [ ] Building ../stdlib//Lean/Runtime.c [ ] Building ../stdlib//Lean/ResolveName.c [ ] Building ../stdlib//Lean/ReducibilityAttrs.c [ ] Building ../stdlib//Lean/ProjFns.c [ ] Building ../stdlib//Lean/PrettyPrinter/Parenthesizer.c [ ] Building ../stdlib//Lean/PrettyPrinter/Formatter.c [ ] Building ../stdlib//Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c [ ] Building ../stdlib//Lean/PrettyPrinter/Delaborator/SubExpr.c [ ] Building ../stdlib//Lean/PrettyPrinter/Delaborator/Options.c [ ] Building ../stdlib//Lean/PrettyPrinter/Delaborator/Builtins.c [ ] Building ../stdlib//Lean/PrettyPrinter/Delaborator/Basic.c [ ] Building ../stdlib//Lean/PrettyPrinter/Delaborator.c [ ] Building ../stdlib//Lean/PrettyPrinter/Basic.c [ ] Building ../stdlib//Lean/PrettyPrinter.c [ ] Building ../stdlib//Lean/ParserCompiler/Attribute.c [ ] Building ../stdlib//Lean/ParserCompiler.c [ ] Building ../stdlib//Lean/Parser/Term.c [ ] Building ../stdlib//Lean/Parser/Tactic.c [ ] Building ../stdlib//Lean/Parser/Syntax.c [ ] Building ../stdlib//Lean/Parser/StrInterpolation.c [ ] Building ../stdlib//Lean/Parser/Module.c [ ] Building ../stdlib//Lean/Parser/Level.c [ ] Building ../stdlib//Lean/Parser/Extra.c [ ] Building ../stdlib//Lean/Parser/Extension.c [ ] Building ../stdlib//Lean/Parser/Do.c [ ] Building ../stdlib//Lean/Parser/Command.c [ ] Building ../stdlib//Lean/Parser/Basic.c [ ] Building ../stdlib//Lean/Parser/Attr.c [ ] Building ../stdlib//Lean/Parser.c [ ] Building ../stdlib//Lean/MonadEnv.c [ ] Building ../stdlib//Lean/Modifiers.c [ ] Building ../stdlib//Lean/MetavarContext.c [ ] Building ../stdlib//Lean/Meta/WHNF.c [ ] Building ../stdlib//Lean/Meta/UnificationHint.c [ ] Building ../stdlib//Lean/Meta/TransparencyMode.c [ ] Building ../stdlib//Lean/Meta/Transform.c [ ] Building ../stdlib//Lean/Meta/Tactic/Util.c [ ] Building ../stdlib//Lean/Meta/Tactic/UnifyEq.c [ ] Building ../stdlib//Lean/Meta/Tactic/Unfold.c [ ] Building ../stdlib//Lean/Meta/Tactic/Subst.c [ ] Building ../stdlib//Lean/Meta/Tactic/SplitIf.c [ ] Building ../stdlib//Lean/Meta/Tactic/Split.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp/Types.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp/SimpTheorems.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp/SimpCongrTheorems.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp/SimpAll.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp/Rewrite.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp/Main.c [ ] Building ../stdlib//Lean/Meta/Tactic/Simp.c [ ] Building ../stdlib//Lean/Meta/Tactic/Rewrite.c [ ] Building ../stdlib//Lean/Meta/Tactic/Revert.c [ ] Building ../stdlib//Lean/Meta/Tactic/Replace.c [ ] Building ../stdlib//Lean/Meta/Tactic/Rename.c [ ] Building ../stdlib//Lean/Meta/Tactic/Refl.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Solver.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Simp.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Nat/Solver.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Nat/Simp.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Nat/Basic.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Nat.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Main.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith/Basic.c [ ] Building ../stdlib//Lean/Meta/Tactic/LinearArith.c [ ] Building ../stdlib//Lean/Meta/Tactic/Intro.c [ ] Building ../stdlib//Lean/Meta/Tactic/Injection.c [ ] Building ../stdlib//Lean/Meta/Tactic/Induction.c [ ] Building ../stdlib//Lean/Meta/Tactic/Generalize.c [ ] Building ../stdlib//Lean/Meta/Tactic/FVarSubst.c [ ] Building ../stdlib//Lean/Meta/Tactic/ElimInfo.c [ ] Building ../stdlib//Lean/Meta/Tactic/Delta.c [ ] Building ../stdlib//Lean/Meta/Tactic/Contradiction.c [ ] Building ../stdlib//Lean/Meta/Tactic/Constructor.c [ ] Building ../stdlib//Lean/Meta/Tactic/Congr.c [ ] Building ../stdlib//Lean/Meta/Tactic/Clear.c [ ] Building ../stdlib//Lean/Meta/Tactic/Cleanup.c [ ] Building ../stdlib//Lean/Meta/Tactic/Cases.c [ ] Building ../stdlib//Lean/Meta/Tactic/AuxLemma.c [ ] Building ../stdlib//Lean/Meta/Tactic/Assumption.c [ ] Building ../stdlib//Lean/Meta/Tactic/Assert.c [ ] Building ../stdlib//Lean/Meta/Tactic/Apply.c [ ] Building ../stdlib//Lean/Meta/Tactic/Acyclic.c [ ] Building ../stdlib//Lean/Meta/Tactic/AC/Main.c [ ] Building ../stdlib//Lean/Meta/Tactic/AC.c [ ] Building ../stdlib//Lean/Meta/Tactic.c [ ] Building ../stdlib//Lean/Meta/SynthInstance.c [ ] Building ../stdlib//Lean/Meta/Structure.c [ ] Building ../stdlib//Lean/Meta/SizeOf.c [ ] Building ../stdlib//Lean/Meta/ReduceEval.c [ ] Building ../stdlib//Lean/Meta/Reduce.c [ ] Building ../stdlib//Lean/Meta/RecursorInfo.c [ ] Building ../stdlib//Lean/Meta/PPGoal.c [ ] Building ../stdlib//Lean/Meta/Offset.c [ ] Building ../stdlib//Lean/Meta/MatchUtil.c [ ] Building ../stdlib//Lean/Meta/Match/Value.c [ ] Building ../stdlib//Lean/Meta/Match/MatcherInfo.c [ ] Building ../stdlib//Lean/Meta/Match/MatchPatternAttr.c [ ] Building ../stdlib//Lean/Meta/Match/MatchEqsExt.c [ ] Building ../stdlib//Lean/Meta/Match/MatchEqs.c [ ] Building ../stdlib//Lean/Meta/Match/Match.c [ ] Building ../stdlib//Lean/Meta/Match/MVarRenaming.c [ ] Building ../stdlib//Lean/Meta/Match/CaseValues.c [ ] Building ../stdlib//Lean/Meta/Match/CaseArraySizes.c [ ] Building ../stdlib//Lean/Meta/Match/Basic.c [ ] Building ../stdlib//Lean/Meta/Match.c [ ] Building ../stdlib//Lean/Meta/LevelDefEq.c [ ] Building ../stdlib//Lean/Meta/KExprMap.c [ ] Building ../stdlib//Lean/Meta/KAbstract.c [ ] Building ../stdlib//Lean/Meta/Instances.c [ ] Building ../stdlib//Lean/Meta/Injective.c [ ] Building ../stdlib//Lean/Meta/InferType.c [ ] Building ../stdlib//Lean/Meta/Inductive.c [ ] Building ../stdlib//Lean/Meta/IndPredBelow.c [ ] Building ../stdlib//Lean/Meta/GlobalInstances.c [ ] Building ../stdlib//Lean/Meta/GetConst.c [ ] Building ../stdlib//Lean/Meta/GeneralizeVars.c [ ] Building ../stdlib//Lean/Meta/GeneralizeTelescope.c [ ] Building ../stdlib//Lean/Meta/FunInfo.c [ ] Building ../stdlib//Lean/Meta/ForEachExpr.c [ ] Building ../stdlib//Lean/Meta/ExprTraverse.c [ ] Building ../stdlib//Lean/Meta/ExprLens.c [ ] Building ../stdlib//Lean/Meta/ExprDefEq.c [ ] Building ../stdlib//Lean/Meta/Eval.c [ ] Building ../stdlib//Lean/Meta/Eqns.c [ ] Building ../stdlib//Lean/Meta/DiscrTreeTypes.c [ ] Building ../stdlib//Lean/Meta/DiscrTree.c [ ] Building ../stdlib//Lean/Meta/DecLevel.c [ ] Building ../stdlib//Lean/Meta/Constructions.c [ ] Building ../stdlib//Lean/Meta/CongrTheorems.c [ ] Building ../stdlib//Lean/Meta/CollectMVars.c [ ] Building ../stdlib//Lean/Meta/CollectFVars.c [ ] Building ../stdlib//Lean/Meta/Coe.c [ ] Building ../stdlib//Lean/Meta/Closure.c [ ] Building ../stdlib//Lean/Meta/Check.c [ ] Building ../stdlib//Lean/Meta/CasesOn.c [ ] Building ../stdlib//Lean/Meta/Basic.c [ ] Building ../stdlib//Lean/Meta/AppBuilder.c [ ] Building ../stdlib//Lean/Meta/AbstractNestedProofs.c [ ] Building ../stdlib//Lean/Meta/AbstractMVars.c [ ] Building ../stdlib//Lean/Meta/ACLt.c [ ] Building ../stdlib//Lean/Meta.c [ ] Building ../stdlib//Lean/Message.c [ ] Building ../stdlib//Lean/Log.c [ ] Building ../stdlib//Lean/LocalContext.c [ ] Building ../stdlib//Lean/LoadDynlib.c [ ] Building ../stdlib//Lean/Linter/Util.c [ ] Building ../stdlib//Lean/Linter/UnusedVariables.c [ ] Building ../stdlib//Lean/Linter/MissingDocs.c [ ] Building ../stdlib//Lean/Linter/Builtin.c [ ] Building ../stdlib//Lean/Linter.c [ ] Building ../stdlib//Lean/Level.c [ ] Building ../stdlib//Lean/LazyInitExtension.c [ ] Building ../stdlib//Lean/KeyedDeclsAttribute.c [ ] Building ../stdlib//Lean/InternalExceptionId.c [ ] Building ../stdlib//Lean/ImportingFlag.c [ ] Building ../stdlib//Lean/Hygiene.c [ ] Building ../stdlib//Lean/HeadIndex.c [ ] Building ../stdlib//Lean/Expr.c [ ] Building ../stdlib//Lean/Exception.c [ ] Building ../stdlib//Lean/Eval.c [ ] Building ../stdlib//Lean/Environment.c [ ] Building ../stdlib//Lean/Elab/Util.c [ ] Building ../stdlib//Lean/Elab/Term.c [ ] Building ../stdlib//Lean/Elab/Tactic/Unfold.c [ ] Building ../stdlib//Lean/Elab/Tactic/Split.c [ ] Building ../stdlib//Lean/Elab/Tactic/Simp.c [ ] Building ../stdlib//Lean/Elab/Tactic/Rewrite.c [ ] Building ../stdlib//Lean/Elab/Tactic/Meta.c [ ] Building ../stdlib//Lean/Elab/Tactic/Match.c [ ] Building ../stdlib//Lean/Elab/Tactic/Location.c [ ] Building ../stdlib//Lean/Elab/Tactic/Injection.c [ ] Building ../stdlib//Lean/Elab/Tactic/Induction.c [ ] Building ../stdlib//Lean/Elab/Tactic/Generalize.c [ ] Building ../stdlib//Lean/Elab/Tactic/ElabTerm.c [ ] Building ../stdlib//Lean/Elab/Tactic/Delta.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Unfold.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Simp.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Rewrite.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Pattern.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Delta.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Congr.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Change.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv/Basic.c [ ] Building ../stdlib//Lean/Elab/Tactic/Conv.c [ ] Building ../stdlib//Lean/Elab/Tactic/Congr.c [ ] Building ../stdlib//Lean/Elab/Tactic/Config.c [ ] Building ../stdlib//Lean/Elab/Tactic/Calc.c [ ] Building ../stdlib//Lean/Elab/Tactic/Cache.c [ ] Building ../stdlib//Lean/Elab/Tactic/BuiltinTactic.c [ ] Building ../stdlib//Lean/Elab/Tactic/Basic.c [ ] Building ../stdlib//Lean/Elab/Tactic.c [ ] Building ../stdlib//Lean/Elab/SyntheticMVars.c [ ] Building ../stdlib//Lean/Elab/Syntax.c [ ] Building ../stdlib//Lean/Elab/Structure.c [ ] Building ../stdlib//Lean/Elab/StructInst.c [ ] Building ../stdlib//Lean/Elab/SetOption.c [ ] Building ../stdlib//Lean/Elab/RecAppSyntax.c [ ] Building ../stdlib//Lean/Elab/Quotation/Util.c [ ] Building ../stdlib//Lean/Elab/Quotation/Precheck.c [ ] Building ../stdlib//Lean/Elab/Quotation.c [ ] Building ../stdlib//Lean/Elab/Print.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/TerminationHint.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/Rel.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/PackMutual.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/PackDomain.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/Main.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/Ite.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/Fix.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF/Eqns.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/WF.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/SmartUnfolding.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/Preprocess.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/Main.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/IndPred.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/FindRecArg.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/Eqns.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/Basic.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural/BRecOn.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Structural.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/MkInhabitant.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Main.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Eqns.c [ ] Building ../stdlib//Lean/Elab/PreDefinition/Basic.c [ ] Building ../stdlib//Lean/Elab/PreDefinition.c [ ] Building ../stdlib//Lean/Elab/PatternVar.c [ ] Building ../stdlib//Lean/Elab/Open.c [ ] Building ../stdlib//Lean/Elab/Notation.c [ ] Building ../stdlib//Lean/Elab/MutualDef.c [ ] Building ../stdlib//Lean/Elab/Mixfix.c [ ] Building ../stdlib//Lean/Elab/MatchAltView.c [ ] Building ../stdlib//Lean/Elab/Match.c [ ] Building ../stdlib//Lean/Elab/MacroRules.c [ ] Building ../stdlib//Lean/Elab/MacroArgUtil.c [ ] Building ../stdlib//Lean/Elab/Macro.c [ ] Building ../stdlib//Lean/Elab/Level.c [ ] Building ../stdlib//Lean/Elab/LetRec.c [ ] Building ../stdlib//Lean/Elab/InfoTree/Types.c [ ] Building ../stdlib//Lean/Elab/InfoTree/Main.c [ ] Building ../stdlib//Lean/Elab/InfoTree.c [ ] Building ../stdlib//Lean/Elab/Inductive.c [ ] Building ../stdlib//Lean/Elab/Import.c [ ] Building ../stdlib//Lean/Elab/GenInjective.c [ ] Building ../stdlib//Lean/Elab/Frontend.c [ ] Building ../stdlib//Lean/Elab/Extra.c [ ] Building ../stdlib//Lean/Elab/Exception.c [ ] Building ../stdlib//Lean/Elab/Eval.c [ ] Building ../stdlib//Lean/Elab/ElabRules.c [ ] Building ../stdlib//Lean/Elab/Do.c [ ] Building ../stdlib//Lean/Elab/Deriving/Util.c [ ] Building ../stdlib//Lean/Elab/Deriving/SizeOf.c [ ] Building ../stdlib//Lean/Elab/Deriving/Repr.c [ ] Building ../stdlib//Lean/Elab/Deriving/Ord.c [ ] Building ../stdlib//Lean/Elab/Deriving/Inhabited.c [ ] Building ../stdlib//Lean/Elab/Deriving/Hashable.c [ ] Building ../stdlib//Lean/Elab/Deriving/FromToJson.c [ ] Building ../stdlib//Lean/Elab/Deriving/DecEq.c [ ] Building ../stdlib//Lean/Elab/Deriving/Basic.c [ ] Building ../stdlib//Lean/Elab/Deriving/BEq.c [ ] Building ../stdlib//Lean/Elab/Deriving.c [ ] Building ../stdlib//Lean/Elab/DefView.c [ ] Building ../stdlib//Lean/Elab/DeclarationRange.c [ ] Building ../stdlib//Lean/Elab/Declaration.c [ ] Building ../stdlib//Lean/Elab/DeclUtil.c [ ] Building ../stdlib//Lean/Elab/DeclModifiers.c [ ] Building ../stdlib//Lean/Elab/Config.c [ ] Building ../stdlib//Lean/Elab/ComputedFields.c [ ] Building ../stdlib//Lean/Elab/Command.c [ ] Building ../stdlib//Lean/Elab/Calc.c [ ] Building ../stdlib//Lean/Elab/BuiltinTerm.c [ ] Building ../stdlib//Lean/Elab/BuiltinNotation.c [ ] Building ../stdlib//Lean/Elab/BuiltinCommand.c [ ] Building ../stdlib//Lean/Elab/BindersUtil.c [ ] Building ../stdlib//Lean/Elab/Binders.c [ ] Building ../stdlib//Lean/Elab/AuxDiscr.c [ ] Building ../stdlib//Lean/Elab/AuxDef.c [ ] Building ../stdlib//Lean/Elab/AutoBound.c [ ] Building ../stdlib//Lean/Elab/Attributes.c [ ] Building ../stdlib//Lean/Elab/Arg.c [ ] Building ../stdlib//Lean/Elab/App.c [ ] Building ../stdlib//Lean/Elab.c [ ] Building ../stdlib//Lean/DocString.c [ ] Building ../stdlib//Lean/Deprecated.c [ ] Building ../stdlib//Lean/DeclarationRange.c [ ] Building ../stdlib//Lean/Declaration.c [ ] Building ../stdlib//Lean/Data/Xml/Parser.c [ ] Building ../stdlib//Lean/Data/Xml/Basic.c [ ] Building ../stdlib//Lean/Data/Xml.c [ ] Building ../stdlib//Lean/Data/Trie.c [ ] Building ../stdlib//Lean/Data/SSet.c [ ] Building ../stdlib//Lean/Data/SMap.c [ ] Building ../stdlib//Lean/Data/Rat.c [ ] Building ../stdlib//Lean/Data/PrefixTree.c [ ] Building ../stdlib//Lean/Data/Position.c [ ] Building ../stdlib//Lean/Data/Parsec.c [ ] Building ../stdlib//Lean/Data/Options.c [ ] Building ../stdlib//Lean/Data/OpenDecl.c [ ] Building ../stdlib//Lean/Data/Occurrences.c [ ] Building ../stdlib//Lean/Data/NameTrie.c [ ] Building ../stdlib//Lean/Data/Name.c [ ] Building ../stdlib//Lean/Data/Lsp/Workspace.c [ ] Building ../stdlib//Lean/Data/Lsp/Utf16.c [ ] Building ../stdlib//Lean/Data/Lsp/TextSync.c [ ] Building ../stdlib//Lean/Data/Lsp/LanguageFeatures.c [ ] Building ../stdlib//Lean/Data/Lsp/Ipc.c [ ] Building ../stdlib//Lean/Data/Lsp/Internal.c [ ] Building ../stdlib//Lean/Data/Lsp/InitShutdown.c [ ] Building ../stdlib//Lean/Data/Lsp/Extra.c [ ] Building ../stdlib//Lean/Data/Lsp/Diagnostics.c [ ] Building ../stdlib//Lean/Data/Lsp/Communication.c [ ] Building ../stdlib//Lean/Data/Lsp/Client.c [ ] Building ../stdlib//Lean/Data/Lsp/Capabilities.c [ ] Building ../stdlib//Lean/Data/Lsp/Basic.c [ ] Building ../stdlib//Lean/Data/Lsp.c [ ] Building ../stdlib//Lean/Data/LOption.c [ ] Building ../stdlib//Lean/Data/LBool.c [ ] Building ../stdlib//Lean/Data/KVMap.c [ ] Building ../stdlib//Lean/Data/JsonRpc.c [ ] Building ../stdlib//Lean/Data/Json/Stream.c [ ] Building ../stdlib//Lean/Data/Json/Printer.c [ ] Building ../stdlib//Lean/Data/Json/Parser.c [ ] Building ../stdlib//Lean/Data/Json/FromToJson.c [ ] Building ../stdlib//Lean/Data/Json/Basic.c [ ] Building ../stdlib//Lean/Data/Json.c [ ] Building ../stdlib//Lean/Data/FuzzyMatching.c [ ] Building ../stdlib//Lean/Data/Format.c [ ] Building ../stdlib//Lean/Data.c [ ] Building ../stdlib//Lean/CoreM.c [ ] Building ../stdlib//Lean/Compiler/Util.c [ ] Building ../stdlib//Lean/Compiler/Specialize.c [ ] Building ../stdlib//Lean/Compiler/Old.c [ ] Building ../stdlib//Lean/Compiler/NoncomputableAttr.c [ ] Building ../stdlib//Lean/Compiler/NeverExtractAttr.c [ ] Building ../stdlib//Lean/Compiler/NameMangling.c [ ] Building ../stdlib//Lean/Compiler/Main.c [ ] Building ../stdlib//Lean/Compiler/LCNF.c [ ] Building ../stdlib//Lean/Compiler/InlineAttrs.c [ ] Building ../stdlib//Lean/Compiler/InitAttr.c [ ] Building ../stdlib//Lean/Compiler/ImplementedByAttr.c [ ] Building ../stdlib//Lean/Compiler/IR/UnboxResult.c [ ] Building ../stdlib//Lean/Compiler/IR/Sorry.c [ ] Building ../stdlib//Lean/Compiler/IR/SimpCase.c [ ] Building ../stdlib//Lean/Compiler/IR/ResetReuse.c [ ] Building ../stdlib//Lean/Compiler/IR/RC.c [ ] Building ../stdlib//Lean/Compiler/IR/PushProj.c [ ] Building ../stdlib//Lean/Compiler/IR/NormIds.c [ ] Building ../stdlib//Lean/Compiler/IR/LiveVars.c [ ] Building ../stdlib//Lean/Compiler/IR/FreeVars.c [ ] Building ../stdlib//Lean/Compiler/IR/Format.c [ ] Building ../stdlib//Lean/Compiler/IR/ExpandResetReuse.c [ ] Building ../stdlib//Lean/Compiler/IR/EmitUtil.c [ ] Building ../stdlib//Lean/Compiler/IR/EmitC.c [ ] Building ../stdlib//Lean/Compiler/IR/ElimDeadVars.c [ ] Building ../stdlib//Lean/Compiler/IR/ElimDeadBranches.c [ ] Building ../stdlib//Lean/Compiler/IR/CtorLayout.c [ ] Building ../stdlib//Lean/Compiler/IR/CompilerM.c [ ] Building ../stdlib//Lean/Compiler/IR/Checker.c [ ] Building ../stdlib//Lean/Compiler/IR/Boxing.c [ ] Building ../stdlib//Lean/Compiler/IR/Borrow.c [ ] Building ../stdlib//Lean/Compiler/IR/Basic.c [ ] Building ../stdlib//Lean/Compiler/IR.c [ ] Building ../stdlib//Lean/Compiler/FFI.c [ ] Building ../stdlib//Lean/Compiler/ExternAttr.c [ ] Building ../stdlib//Lean/Compiler/ExportAttr.c [ ] Building ../stdlib//Lean/Compiler/Decl.c [ ] Building ../stdlib//Lean/Compiler/ConstFolding.c [ ] Building ../stdlib//Lean/Compiler/CompilerM.c [ ] Building ../stdlib//Lean/Compiler/ClosedTermCache.c [ ] Building ../stdlib//Lean/Compiler/CSimpAttr.c [ ] Building ../stdlib//Lean/Compiler/BorrowedAnnotation.c [ ] Building ../stdlib//Lean/Compiler/AtMostOnce.c [ ] Building ../stdlib//Lean/Compiler.c [ ] Building ../stdlib//Lean/Class.c [ ] Building ../stdlib//Lean/Attributes.c [ ] Building ../stdlib//Lean/AuxRecursor.c [ ] Building ../stdlib//Lean.c make[8]: Leaving directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[7]: Leaving directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [100%] Built target make_stdlib make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[7]: Entering directory '/home/main-builder/pkgwork/src/lean4/stage0/src' [ ] Building /home/main-builder/pkgwork/src/lean4/_build/stage0/lib/lean/libleanshared.so make[7]: Leaving directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [100%] Built target leanshared make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[6]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[7]: Entering directory '/home/main-builder/pkgwork/src/lean4/stage0/src' [ ] Building /home/main-builder/pkgwork/src/lean4/_build/stage0/bin/lean make[7]: Leaving directory '/home/main-builder/pkgwork/src/lean4/stage0/src' make[6]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [100%] Built target lean make[5]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' make[4]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build/stage0' [ 29%] No install step for 'stage0' [ 33%] Completed 'stage0' make[3]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' [ 33%] Built target stage0 make[3]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' make[3]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' make[3]: Entering directory '/home/main-builder/pkgwork/src/lean4/_build' [ 37%] Creating directories for 'stage1' [ 41%] No download step for 'stage1' [ 45%] No update step for 'stage1' [ 50%] No patch step for 'stage1' [ 54%] Performing configure step for 'stage1' -- The CXX compiler identification is GNU 12.1.1 -- The C compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/sbin/c++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/sbin/cc - skipped -- Detecting C compile features -- Detecting C compile features - done -- 64-bit machine detected -- Found GMP: /usr/include (Required is at least version "5.0.5") CMake Warning at CMakeLists.txt:257 (message): Failed to find ccache, prepare for longer and redundant builds... -- Could NOT find PythonInterp (missing: PYTHON_EXECUTABLE) -- git commit sha1: 0204c5f9b7042f42f995bfc336130c37c4a7eaa4 CMake Error at CMakeLists.txt:479 (message): src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`. -- Configuring incomplete, errors occurred! See also "/home/main-builder/pkgwork/src/lean4/_build/stage1/CMakeFiles/CMakeOutput.log". make[3]: *** [CMakeFiles/stage1.dir/build.make:92: stage1-prefix/src/stage1-stamp/stage1-configure] Error 1 make[3]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' make[2]: *** [CMakeFiles/Makefile2:116: CMakeFiles/stage1.dir/all] Error 2 make[2]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' make[1]: *** [CMakeFiles/Makefile2:149: CMakeFiles/stage2.dir/rule] Error 2 make[1]: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' make: *** [Makefile:195: stage2] Error 2 make: Leaving directory '/home/main-builder/pkgwork/src/lean4/_build' ==> ERROR: A failure occurred in build(). Aborting...