search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
552 stars 83 forks source link

Trying to translate natural language reasoning text to lean code and trace it using LeanDoJo #12

Closed Some-random closed 1 year ago

Some-random commented 1 year ago

I'm trying to explore whether it's possible to translate some reasoning test set to lean code and solve it using ATP models. The prompt I gave to GPT-4 was: 

I want you to translate this to lean: "Translate this to the language of Lean: "Every zumpus is a tumpus. Each zumpus is transparent. Vumpuses are zumpuses. Every vumpus is not brown. Each wumpus is a vumpus. Wumpuses are wooden. Jompuses are wumpuses. Each jompus is not floral. Yumpuses are jompuses. Yumpuses are mean. Dumpuses are yumpuses. Rompuses are brown. Dumpuses are spicy. Impuses are dumpuses. Every impus is large. Every numpus is an impus. Numpuses are not feisty. Polly is a vumpus. True or false: Polly is not brown."

And the GPT-4 response was

universe u
constant obj : Type u

constant zumpus : obj → Prop
constant tumpus : obj → Prop
constant transparent : obj → Prop
constant vumpus : obj → Prop
constant brown : obj → Prop
constant wumpus : obj → Prop
constant wooden : obj → Prop
constant jompus : obj → Prop
constant floral : obj → Prop
constant yumpus : obj → Prop
constant mean : obj → Prop
constant dumpus : obj → Prop
constant rompus : obj → Prop
constant spicy : obj → Prop
constant impus : obj → Prop
constant large : obj → Prop
constant numpus : obj → Prop
constant feisty : obj → Prop
constant polly : obj

axiom A1 : ∀ x, zumpus x → tumpus x
axiom A2 : ∀ x, zumpus x → transparent x
axiom A3 : ∀ x, vumpus x → zumpus x
axiom A4 : ∀ x, vumpus x → ¬ brown x
axiom A5 : ∀ x, wumpus x → vumpus x
axiom A6 : ∀ x, wumpus x → wooden x
axiom A7 : ∀ x, jompus x → wumpus x
axiom A8 : ∀ x, jompus x → ¬ floral x
axiom A9 : ∀ x, yumpus x → jompus x
axiom A10 : ∀ x, yumpus x → mean x
axiom A11 : ∀ x, dumpus x → yumpus x
axiom A12 : ∀ x, rompus x → brown x
axiom A13 : ∀ x, dumpus x → spicy x
axiom A14 : ∀ x, impus x → dumpus x
axiom A15 : ∀ x, impus x → large x
axiom A16 : ∀ x, numpus x → impus x
axiom A17 : ∀ x, numpus x → ¬ feisty x
axiom A18 : vumpus polly

-- Theorem to check if Polly is not brown
theorem polly_is_not_brown : ¬ brown polly :=
begin
  apply A4,
  exact A18,
end

which gave me no error when I run it in the Lean web editor. But when I tried to upload it to github and trace it using LeanDoJo with this code

from lean_dojo import LeanGitRepo, trace
import os

repo = LeanGitRepo("https://github.com/Some-random/lean-example", "4067a13790e7d02af9cda2f4ab249b3f88ff9884")
trace(repo, dst_dir="traced_natural_language_inference")

it gave me this error 

Traceback (most recent call last):
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/LeanDojo/test_trace.py", line 19, in <module>
    trace(repo, dst_dir="traced_natural_language_inference")
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 165, in trace
    traced_repo = TracedRepo.load_from_disk(cached_path)
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1283, in load_from_disk
    traced_files = list(
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/tqdm/std.py", line 1178, in __iter__
    for obj in iterable:
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/ray/util/actor_pool.py", line 126, in get_generator
    yield self.get_next_unordered()
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/ray/util/actor_pool.py", line 273, in get_next_unordered
    return ray.get(future)
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/ray/_private/auto_init_hook.py", line 18, in auto_init_wrapper
    return fn(*args, **kwargs)
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/ray/_private/worker.py", line 2540, in get
    raise value.as_instanceof_cause()
ray.exceptions.RayTaskError(TypeError): ray::_TracedRepoHelper.load_xml_from_disk() (pid=3474923, ip=172.31.130.94, actor_id=ee7d2d4c9ee49fb3f634f7c201000000, repr=<lean_dojo.data_extraction.traced_data._TracedRepoHelper object at 0x7f4fe803d810>)
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1080, in load_xml_from_disk
    return TracedFile.from_xml(self.root_dir, path, self.repo)
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1035, in from_xml
    exprs = [Expr.from_xml(e) for e in exprs_tree]
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1035, in <listcomp>
    exprs = [Expr.from_xml(e) for e in exprs_tree]
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/ast/lean3/expr.py", line 93, in from_xml
    kwargs[field.name] = Expr.from_xml(tree[i])
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/ast/lean3/expr.py", line 93, in from_xml
    kwargs[field.name] = Expr.from_xml(tree[i])
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/ast/lean3/expr.py", line 93, in from_xml
    kwargs[field.name] = Expr.from_xml(tree[i])
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/ast/lean3/expr.py", line 115, in from_xml
    kwargs[field.name] = field.type(tree.attrib[field.name])  # type: ignore
  File "/bask/projects/j/jlxi8926-auto-sum/dongwei/miniconda/envs/dojo/lib/python3.10/typing.py", line 955, in __call__
    raise TypeError(f"Type {self._name} cannot be instantiated; "
TypeError: Type List cannot be instantiated; use list() instead

I'm still digging into the way LeanDoJo traces theorems, and any help would be greatly appreciated!

yangky11 commented 1 year ago

I just tried your code but wasn't able to reproduce the problem. Could you please delete the traced repo in the cache (if any) and retry with the debug mode (setting the environment variable VERBOSE=1). Also, make sure you're using the latest version of LeanDojo (1.1.2)

yangky11 commented 1 year ago

My output:

(lean-dojo) kaiyu@tensorlab-DGX:~/LeanDojo$ VERBOSE=1 ipython
Python 3.10.11 (main, May 16 2023, 00:28:57) [GCC 11.2.0]
Type 'copyright', 'credits' or 'license' for more information
IPython 8.12.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: from lean_dojo import LeanGitRepo, trace
   ...: import os
   ...: 
   ...: repo = LeanGitRepo("https://github.com/Some-random/lean-example", "4067a137
   ...: 90e7d02af9cda2f4ab249b3f88ff9884")
   ...: trace(repo, dst_dir="traced_natural_language_inference")

2023-07-07 20:22:25.473 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:132 - Tracing LeanGitRepo(url='https://github.com/Some-random/lean-example', commit='4067a13790e7d02af9cda2f4ab249b3f88ff9884')
2023-07-07 20:22:25.473 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:134 - Working in the temporary directory /raid/kaiyu/tmp/tmpukon9kz5
2023-07-07 20:22:26.268 | DEBUG    | lean_dojo.data_extraction.lean:clone_and_checkout:370 - Cloning LeanGitRepo(url='https://github.com/Some-random/lean-example', commit='4067a13790e7d02af9cda2f4ab249b3f88ff9884')
2023-07-07 20:22:26.765 | DEBUG    | lean_dojo.data_extraction.trace:_modify_lean3:37 - Modifying Lean v3.50.3
2023-07-07 20:22:31.051 | DEBUG    | lean_dojo.data_extraction.trace:_modify_lean3:48 - Applying the modification patch
2023-07-07 20:22:31.055 | DEBUG    | lean_dojo.data_extraction.trace:_trace_lean3:79 - Tracing LeanGitRepo(url='https://github.com/Some-random/lean-example', commit='4067a13790e7d02af9cda2f4ab249b3f88ff9884')
2023-07-07 20:22:31.055 | DEBUG    | lean_dojo.container:run:301 - docker run --cidfile wy5471ot.cid --rm -u 1013 --mount type=bind,src="/raid/kaiyu/tmp/tmpukon9kz5/lean-example",target="/workspace/lean-example" --mount type=bind,src="/home/kaiyu/miniconda3/envs/lean-dojo/lib/python3.10/site-packages/lean_dojo/data_extraction/build_lean3_repo.py",target="/workspace/build_lean3_repo.py" --env NUM_PROCS=32 --workdir /workspace yangky11/lean-dojo python3 build_lean3_repo.py lean-example
2023-07-08 03:22:31.553 | INFO     | __main__:main:103 - Building modifed Lean
CMake Deprecation Warning at CMakeLists.txt:1 (cmake_minimum_required):
  Compatibility with CMake < 2.8.12 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.

-- The CXX compiler identification is GNU 12.2.1
-- The C compiler identification is GNU 12.2.1
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/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/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- No build type selected, default to Release
-- Lean library will be installed at /usr/local/lib/lean
-- Found GMP: /usr/include (Required is at least version "5.0.5")
-- Using standard malloc.
-- Found PythonInterp: /usr/bin/python3.11 (found version "3.11") 
-- git commit sha1: 855e5b74e3a52a40552e8f067169d747d48743fd
-- Configuring done
-- Generating done
-- Build files have been written to: /workspace/lean-example/_target/deps/lean/build/release
[  0%] Building CXX object init/CMakeFiles/init.dir/init.cpp.o
[  0%] Building CXX object util/numerics/CMakeFiles/numerics.dir/mpz.cpp.o
[  0%] Building CXX object kernel/quotient/CMakeFiles/quotient.dir/quotient.cpp.o
[  0%] Building CXX object util/numerics/CMakeFiles/numerics.dir/mpq.cpp.o
[  0%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/init_module.cpp.o
[  0%] Building CXX object kernel/inductive/CMakeFiles/inductive.dir/inductive.cpp.o
[  0%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/compiler.cpp.o
[  0%] Building CXX object library/tactic/backward/CMakeFiles/backward.dir/init_module.cpp.o
[  0%] Building CXX object kernel/CMakeFiles/kernel.dir/level.cpp.o
[  0%] Building CXX object util/CMakeFiles/util.dir/debug.cpp.o
[  0%] Building CXX object util/CMakeFiles/util.dir/name_set.cpp.o
[  0%] Building CXX object kernel/CMakeFiles/kernel.dir/expr_eq_fn.cpp.o
[  0%] Building CXX object util/sexpr/CMakeFiles/sexpr.dir/format.cpp.o
[  0%] Building CXX object library/constructions/CMakeFiles/constructions.dir/rec_on.cpp.o
[  1%] Building CXX object util/sexpr/CMakeFiles/sexpr.dir/sexpr_fn.cpp.o
[  1%] Building CXX object util/sexpr/CMakeFiles/sexpr.dir/sexpr.cpp.o
[  1%] Building CXX object kernel/CMakeFiles/kernel.dir/expr.cpp.o
[  1%] Building CXX object util/CMakeFiles/util.dir/name.cpp.o
[  1%] Building CXX object util/sexpr/CMakeFiles/sexpr.dir/options.cpp.o
[  1%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/equations.cpp.o
[  2%] Building CXX object util/sexpr/CMakeFiles/sexpr.dir/option_declarations.cpp.o
[  3%] Building CXX object util/sexpr/CMakeFiles/sexpr.dir/init_module.cpp.o
[  3%] Building CXX object util/CMakeFiles/util.dir/fresh_name.cpp.o
[  3%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/util.cpp.o
[  3%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/congruence_closure.cpp.o
[  3%] Building CXX object library/tactic/CMakeFiles/tactic.dir/occurrences.cpp.o
[  3%] Building CXX object library/CMakeFiles/library.dir/deep_copy.cpp.o
[  4%] Building CXX object library/vm/CMakeFiles/vm.dir/vm.cpp.o
[  4%] Building CXX object library/predict/CMakeFiles/predict.dir/predict.cpp.o
[  4%] Building CXX object shell/CMakeFiles/shell_js.dir/lean_js.cpp.o
[  4%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/tokens.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  4%] Building CXX object library/compiler/CMakeFiles/compiler.dir/util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /workspace/lean-example/_target/deps/lean/src/library/predict/knn.cpp:2,
                 from /workspace/lean-example/_target/deps/lean/src/library/predict/predict.cpp:1:
/workspace/lean-example/_target/deps/lean/src/library/predict/predictor.cpp: In member function ‘virtual void Predictor::import_data(std::string)’:
/workspace/lean-example/_target/deps/lean/src/library/predict/predictor.cpp:21:37: warning: unused parameter ‘location’ [-Wunused-parameter]
   21 |     virtual void import_data(string location) {}
      |                              ~~~~~~~^~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/predict/predictor.cpp: In member function ‘virtual void Predictor::export_data(std::string) const’:
/workspace/lean-example/_target/deps/lean/src/library/predict/predictor.cpp:22:37: warning: unused parameter ‘location’ [-Wunused-parameter]
   22 |     virtual void export_data(string location) const {}
      |                              ~~~~~~~^~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/predict/predictor.cpp: In constructor ‘Predictor::Predictor(LVecVec, LVecVec, LVecVec, long int)’:
/workspace/lean-example/_target/deps/lean/src/library/predict/predictor.cpp:38:72: warning: unused parameter ‘sym_num’ [-Wunused-parameter]
   38 | Predictor::Predictor(LVecVec deps, LVecVec syms, LVecVec sym_ths, long sym_num)
      |                                                                   ~~~~~^~~~~~~
[  4%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/token_table.cpp.o
[  4%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/scanner.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  4%] Building CXX object library/vm/CMakeFiles/vm.dir/optimize.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  4%] Building CXX object library/CMakeFiles/library.dir/expr_lt.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  4%] Built target numerics
[  5%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/parse_table.cpp.o
[  5%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_nat.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  5%] Building CXX object library/CMakeFiles/library.dir/io_state.cpp.o
[  5%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/parser_config.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  5%] Built target init
[  5%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/parser.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  5%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/parser_pos_provider.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  6%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/pack_domain.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  6%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/structural_rec.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  6%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/unbounded_rec.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  6%] Building CXX object library/tactic/CMakeFiles/tactic.dir/kabstract.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  6%] Building CXX object library/tactic/backward/CMakeFiles/backward.dir/backward_lemmas.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  6%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/elim_match.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  7%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/add_decl.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  7%] Building CXX object library/constructions/CMakeFiles/constructions.dir/cases_on.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  8%] Building CXX object library/constructions/CMakeFiles/constructions.dir/no_confusion.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  8%] Built target sexpr
[  8%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/ginductive_decl.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  8%] Building CXX object library/constructions/CMakeFiles/constructions.dir/projection.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  8%] Building CXX object util/CMakeFiles/util.dir/exception.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  8%] Building CXX object library/compiler/CMakeFiles/compiler.dir/eta_expansion.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  8%] Built target quotient
[  8%] Building CXX object library/compiler/CMakeFiles/compiler.dir/preprocess.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  9%] Building CXX object library/CMakeFiles/library.dir/io_state_stream.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[  9%] Building CXX object library/CMakeFiles/library.dir/bin_app.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 10%] Building CXX object library/compiler/CMakeFiles/compiler.dir/compiler_step_visitor.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 10%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/ginductive.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 11%] Building CXX object kernel/CMakeFiles/kernel.dir/for_each_fn.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 11%] Building CXX object util/CMakeFiles/util.dir/interrupt.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 11%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/basic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 12%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/compiler.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /usr/include/c++/12/bits/new_allocator.h:36,
                 from /usr/include/c++/12/x86_64-redhat-linux/bits/c++allocator.h:33,
                 from /usr/include/c++/12/bits/allocator.h:46,
                 from /usr/include/c++/12/string:41,
                 from /workspace/lean-example/_target/deps/lean/src/shell/lean_js.cpp:7:
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
In file included from /workspace/lean-example/_target/deps/lean/src/util/lean_json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:19,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/pos_info_provider.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/library/abstract_parser.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser_state.h:12,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/module_parser.h:14,
                 from /workspace/lean-example/_target/deps/lean/src/library/module_mgr.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/shell/lean_js.cpp:8:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:38: note: ‘<anonymous>’ declared here
 9059 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:34: note: ‘<anonymous>’ declared here
 9113 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:38: note: ‘<anonymous>’ declared here
 9138 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:34: note: ‘<anonymous>’ declared here
 9169 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:24:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:26: note: ‘<anonymous>’ declared here
 9222 |                 result = basic_json(value_t::discarded);
      |                          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[ 12%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/mutual.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 13%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/nested.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 13%] Building CXX object util/CMakeFiles/util.dir/hash.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 14%] Building CXX object shell/CMakeFiles/shell_js.dir/server.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object util/CMakeFiles/util.dir/escaped.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object kernel/CMakeFiles/kernel.dir/replace_fn.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object kernel/CMakeFiles/kernel.dir/free_vars.cpp.o
[ 15%] Building CXX object library/constructions/CMakeFiles/constructions.dir/brec_on.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Built target inductive
[ 15%] Building CXX object library/inductive_compiler/CMakeFiles/inductive_compiler.dir/util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp: In function ‘uint64_t lean::MurmurHash64A(const void*, int, unsigned int)’:
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:98:15: warning: this statement may fall through [-Wimplicit-fallthrough=]
   98 |     case 7: h ^= uint64_t(data2[6]) << 48;
      |             ~~^~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:99:5: note: here
   99 |     case 6: h ^= uint64_t(data2[5]) << 40;
      |     ^~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:99:15: warning: this statement may fall through [-Wimplicit-fallthrough=]
   99 |     case 6: h ^= uint64_t(data2[5]) << 40;
      |             ~~^~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:100:5: note: here
  100 |     case 5: h ^= uint64_t(data2[4]) << 32;
      |     ^~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:100:15: warning: this statement may fall through [-Wimplicit-fallthrough=]
  100 |     case 5: h ^= uint64_t(data2[4]) << 32;
      |             ~~^~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:101:5: note: here
  101 |     case 4: h ^= uint64_t(data2[3]) << 24;
      |     ^~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:101:15: warning: this statement may fall through [-Wimplicit-fallthrough=]
  101 |     case 4: h ^= uint64_t(data2[3]) << 24;
      |             ~~^~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:102:5: note: here
  102 |     case 3: h ^= uint64_t(data2[2]) << 16;
      |     ^~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:102:15: warning: this statement may fall through [-Wimplicit-fallthrough=]
  102 |     case 3: h ^= uint64_t(data2[2]) << 16;
      |             ~~^~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:103:5: note: here
  103 |     case 2: h ^= uint64_t(data2[1]) << 8;
      |     ^~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:103:15: warning: this statement may fall through [-Wimplicit-fallthrough=]
  103 |     case 2: h ^= uint64_t(data2[1]) << 8;
      |             ~~^~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/util/hash.cpp:104:5: note: here
  104 |     case 1: h ^= uint64_t(data2[0]);
      |     ^~~~
[ 15%] Building CXX object kernel/CMakeFiles/kernel.dir/abstract.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object library/CMakeFiles/library.dir/constants.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object util/CMakeFiles/util.dir/bit_tricks.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object library/CMakeFiles/library.dir/kernel_serializer.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object util/CMakeFiles/util.dir/safe_arith.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 15%] Building CXX object util/CMakeFiles/util.dir/ascii.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 16%] Building CXX object library/CMakeFiles/library.dir/max_sharing.cpp.o
[ 16%] Building CXX object library/CMakeFiles/library.dir/shared_environment.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 16%] Building CXX object library/tactic/CMakeFiles/tactic.dir/tactic_state.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 16%] Built target predict
[ 17%] Building CXX object kernel/CMakeFiles/kernel.dir/instantiate.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 17%] Building CXX object kernel/CMakeFiles/kernel.dir/formatter.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 17%] Building CXX object util/CMakeFiles/util.dir/memory.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 17%] Building CXX object library/compiler/CMakeFiles/compiler.dir/elim_recursors.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 17%] Building CXX object library/CMakeFiles/library.dir/module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 17%] Building CXX object library/CMakeFiles/library.dir/private.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 18%] Building CXX object util/CMakeFiles/util.dir/shared_mutex.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 18%] Building CXX object library/CMakeFiles/library.dir/placeholder.cpp.o
[ 19%] Building CXX object library/CMakeFiles/library.dir/aliases.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 19%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/builtin_cmds.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 19%] Building CXX object library/CMakeFiles/library.dir/update_declaration.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 19%] Building CXX object library/CMakeFiles/library.dir/scoped_ext.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 19%] Building CXX object library/CMakeFiles/library.dir/sorry.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object library/CMakeFiles/library.dir/replace_visitor.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object library/constructions/CMakeFiles/constructions.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/wf_rec.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object util/CMakeFiles/util.dir/path.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /workspace/lean-example/_target/deps/lean/src/util/name_map.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/util/sexpr/option_declarations.h:11,
                 from /workspace/lean-example/_target/deps/lean/src/library/equations_compiler/elim_match.cpp:9:
In destructor ‘lean::name::~name()’,
    inlined from ‘lean::optional<T>::~optional() [with T = lean::name]’ at /workspace/lean-example/_target/deps/lean/src/util/optional.h:47:23,
    inlined from ‘bool lean::elim_match_fn::is_transport_transition(const problem&)’ at /workspace/lean-example/_target/deps/lean/src/library/equations_compiler/elim_match.cpp:531:5,
    inlined from ‘lean::list<lean::elim_match_fn::lemma> lean::elim_match_fn::process(const problem&)’ at /workspace/lean-example/_target/deps/lean/src/library/equations_compiler/elim_match.cpp:1280:51:
/workspace/lean-example/_target/deps/lean/src/util/name.h:87:40: warning: ‘*(lean::name*)((char*)&fn_name + offsetof(lean::optional<lean::name>,lean::optional<lean::name>::<unnamed>)).lean::name::m_ptr’ may be used uninitialized [-Wmaybe-uninitialized]
   87 |     ~name() { if (m_ptr) m_ptr->dec_ref(); }
      |                          ~~~~~~~~~~~~~~^~
/workspace/lean-example/_target/deps/lean/src/library/equations_compiler/elim_match.cpp: In member function ‘lean::list<lean::elim_match_fn::lemma> lean::elim_match_fn::process(const problem&)’:
/workspace/lean-example/_target/deps/lean/src/library/equations_compiler/elim_match.cpp:520:24: note: ‘*(lean::name*)((char*)&fn_name + offsetof(lean::optional<lean::name>,lean::optional<lean::name>::<unnamed>)).lean::name::m_ptr’ was declared here
  520 |         optional<name> fn_name;
      |                        ^~~~~~~
[ 20%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/pack_mutual.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object util/CMakeFiles/util.dir/stackinfo.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object util/CMakeFiles/util.dir/lean_path.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 20%] Building CXX object library/CMakeFiles/library.dir/explicit.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 21%] Building CXX object util/CMakeFiles/util.dir/serializer.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object library/constructions/CMakeFiles/constructions.dir/has_sizeof.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object library/equations_compiler/CMakeFiles/equations_compiler.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object util/CMakeFiles/util.dir/lbool.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object util/CMakeFiles/util.dir/bitap_fuzzy_search.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object kernel/CMakeFiles/kernel.dir/declaration.cpp.o
[ 22%] Building CXX object library/constructions/CMakeFiles/constructions.dir/constructor.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object kernel/CMakeFiles/kernel.dir/environment.cpp.o
In file included from /workspace/lean-example/_target/deps/lean/src/library/library_task_builder.h:8,
                 from /workspace/lean-example/_target/deps/lean/src/library/module.cpp:34:
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h: In instantiation of ‘lean::task<std::vector<T, std::allocator<_Tp1> > > lean::traverse(const std::vector<std::shared_ptr<task_cell<Res> > >&) [with Res = expr; task<std::vector<T, std::allocator<_Tp1> > > = std::shared_ptr<task_cell<std::vector<expr, std::allocator<expr> > > >]’:
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h:181:37:   required from ‘lean::task<bool> lean::any(const std::vector<std::shared_ptr<task_cell<T> > >&, Fn&&) [with Fn = has_sorry(const modification_list&)::<lambda(const expr&)>; T = expr; task<bool> = std::shared_ptr<task_cell<bool> >]’
/workspace/lean-example/_target/deps/lean/src/library/module.cpp:294:15:   required from here
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h:143:24: warning: loop variable ‘t’ of type ‘const lean::gtask&’ {aka ‘const std::shared_ptr<lean::gtask_cell>&’} binds to a temporary constructed from type ‘const std::shared_ptr<lean::task_cell<lean::expr> >’ [-Wrange-loop-construct]
  143 |     for (gtask const & t : ts) {
      |                        ^
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h:143:24: note: use non-reference type ‘const lean::gtask’ {aka ‘const std::shared_ptr<lean::gtask_cell>’} to make the copy explicit or ‘const std::shared_ptr<lean::task_cell<lean::expr> >&’ to prevent copying
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 22%] Building CXX object library/tactic/backward/CMakeFiles/backward.dir/backward_chaining.cpp.o
[ 22%] Building CXX object kernel/CMakeFiles/kernel.dir/pos_info_provider.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h: In instantiation of ‘lean::task<std::vector<T, std::allocator<_Tp1> > > lean::traverse(const std::vector<std::shared_ptr<task_cell<Res> > >&) [with Res = bool; task<std::vector<T, std::allocator<_Tp1> > > = std::shared_ptr<task_cell<std::vector<bool, std::allocator<bool> > > >]’:
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h:181:37:   required from ‘lean::task<bool> lean::any(const std::vector<std::shared_ptr<task_cell<T> > >&, Fn&&) [with Fn = module::error_already_reported()::<lambda(bool)>; T = bool; task<bool> = std::shared_ptr<task_cell<bool> >]’
/workspace/lean-example/_target/deps/lean/src/library/module.cpp:525:15:   required from here
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h:143:24: warning: loop variable ‘t’ of type ‘const lean::gtask&’ {aka ‘const std::shared_ptr<lean::gtask_cell>&’} binds to a temporary constructed from type ‘const std::shared_ptr<lean::task_cell<bool> >’ [-Wrange-loop-construct]
/workspace/lean-example/_target/deps/lean/src/util/task_builder.h:143:24: note: use non-reference type ‘const lean::gtask’ {aka ‘const std::shared_ptr<lean::gtask_cell>’} to make the copy explicit or ‘const std::shared_ptr<lean::task_cell<bool> >&’ to prevent copying
[ 23%] Building CXX object kernel/CMakeFiles/kernel.dir/type_checker.cpp.o
[ 23%] Building CXX object kernel/CMakeFiles/kernel.dir/error_msgs.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 23%] Building CXX object library/compiler/CMakeFiles/compiler.dir/comp_irrelevant.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 23%] Building CXX object util/CMakeFiles/util.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 24%] Building CXX object util/CMakeFiles/util.dir/thread.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 25%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/builtin_exprs.cpp.o
[ 25%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/notation_cmd.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 25%] Building CXX object util/CMakeFiles/util.dir/memory_pool.cpp.o
[ 25%] Building CXX object util/CMakeFiles/util.dir/utf8.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 25%] Building CXX object library/compiler/CMakeFiles/compiler.dir/inliner.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 26%] Building CXX object library/compiler/CMakeFiles/compiler.dir/rec_fn_macro.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 26%] Building CXX object util/CMakeFiles/util.dir/name_map.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 26%] Building CXX object library/CMakeFiles/library.dir/num.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 26%] Building CXX object library/CMakeFiles/library.dir/string.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 27%] Building CXX object library/CMakeFiles/library.dir/head_map.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 27%] Building CXX object library/CMakeFiles/library.dir/class.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 27%] Building CXX object library/CMakeFiles/library.dir/util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 27%] Building CXX object kernel/CMakeFiles/kernel.dir/kernel_exception.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 27%] Building CXX object library/CMakeFiles/library.dir/print.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 28%] Building CXX object util/CMakeFiles/util.dir/line_endings.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 28%] Building CXX object kernel/CMakeFiles/kernel.dir/normalizer_extension.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 28%] Building CXX object util/CMakeFiles/util.dir/list_fn.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 29%] Building CXX object kernel/CMakeFiles/kernel.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/congruence_tactics.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/hinst_lemmas.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/ematch.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/theory_ac.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object util/CMakeFiles/util.dir/file_lock.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object util/CMakeFiles/util.dir/timeit.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Built target backward
[ 30%] Building CXX object kernel/CMakeFiles/kernel.dir/expr_cache.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object kernel/CMakeFiles/kernel.dir/scope_pos_info_provider.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 30%] Building CXX object kernel/CMakeFiles/kernel.dir/equiv_manager.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 31%] Building CXX object kernel/CMakeFiles/kernel.dir/abstract_type_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 31%] Building CXX object kernel/CMakeFiles/kernel.dir/standard_kernel.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 32%] Building CXX object library/CMakeFiles/library.dir/annotation.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 33%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 33%] Built target equations_compiler
[ 33%] Building CXX object library/CMakeFiles/library.dir/quote.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object util/CMakeFiles/util.dir/timer.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/smt_state.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/tactic/smt/CMakeFiles/smt.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/compiler/CMakeFiles/compiler.dir/erase_irrelevant.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/compiler/CMakeFiles/compiler.dir/reduce_arity.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/compiler/CMakeFiles/compiler.dir/lambda_lifting.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/constructions/CMakeFiles/constructions.dir/drec.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object util/CMakeFiles/util.dir/task.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/constructions/CMakeFiles/constructions.dir/injective.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/constructions/CMakeFiles/constructions.dir/util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /usr/include/c++/12/bits/stl_pair.h:61,
                 from /usr/include/c++/12/bits/stl_algobase.h:64,
                 from /usr/include/c++/12/list:60,
                 from /workspace/lean-example/_target/deps/lean/src/shell/server.cpp:14:
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
In file included from /workspace/lean-example/_target/deps/lean/src/util/lean_json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:19,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/pos_info_provider.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/library/abstract_parser.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser_state.h:12,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/module_parser.h:14,
                 from /workspace/lean-example/_target/deps/lean/src/shell/server.cpp:19:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:38: note: ‘<anonymous>’ declared here
 9059 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:34: note: ‘<anonymous>’ declared here
 9113 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:38: note: ‘<anonymous>’ declared here
 9138 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:34: note: ‘<anonymous>’ declared here
 9169 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:24:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:26: note: ‘<anonymous>’ declared here
 9222 |                 result = basic_json(value_t::discarded);
      |                          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[ 34%] Building CXX object util/CMakeFiles/util.dir/task_builder.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Building CXX object library/compiler/CMakeFiles/compiler.dir/simp_inductive.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 34%] Built target kernel
[ 35%] Building CXX object library/compiler/CMakeFiles/compiler.dir/nat_value.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 35%] Building CXX object util/CMakeFiles/util.dir/cancellable.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 35%] Building CXX object library/compiler/CMakeFiles/compiler.dir/vm_compiler.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 35%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_string.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 35%] Building CXX object library/compiler/CMakeFiles/compiler.dir/cse.cpp.o
[ 35%] Built target shell_js
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 35%] Building CXX object library/compiler/CMakeFiles/compiler.dir/elim_unused_lets.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 36%] Building CXX object library/compiler/CMakeFiles/compiler.dir/extract_values.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 36%] Building CXX object library/compiler/CMakeFiles/compiler.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 36%] Building CXX object util/CMakeFiles/util.dir/log_tree.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 36%] Building CXX object library/CMakeFiles/library.dir/typed_expr.cpp.o
[ 36%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/calc.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
/workspace/lean-example/_target/deps/lean/src/frontends/lean/notation_cmd.cpp: In function ‘lean::pair<lean::notation_entry, lean::optional<lean::token_entry> > lean::parse_mixfix_notation(parser&, ast_data&, mixfix_kind, bool, notation_entry_group, bool, unsigned int)’:
/workspace/lean-example/_target/deps/lean/src/frontends/lean/notation_cmd.cpp:206:26: warning: ‘*(unsigned int*)((char*)&prec + offsetof(lean::optional<unsigned int>,lean::optional<unsigned int>::<unnamed>))’ may be used uninitialized [-Wmaybe-uninitialized]
  206 |             prec = *prec - 1;
      |                    ~~~~~~^~~
/workspace/lean-example/_target/deps/lean/src/frontends/lean/notation_cmd.cpp:154:24: note: ‘*(unsigned int*)((char*)&prec + offsetof(lean::optional<unsigned int>,lean::optional<unsigned int>::<unnamed>))’ was declared here
  154 |     optional<unsigned> prec;
      |                        ^~~~
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 36%] Building CXX object library/CMakeFiles/library.dir/protected.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /usr/include/c++/12/atomic:41,
                 from /workspace/lean-example/_target/deps/lean/src/util/thread.h:23,
                 from /workspace/lean-example/_target/deps/lean/src/util/rc.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/util/name.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/util/sexpr/options.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/library/profiling.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:11:
In member function ‘std::__atomic_base<_IntTp>::__int_type std::__atomic_base<_IntTp>::load(std::memory_order) const [with _ITp = unsigned int]’,
    inlined from ‘std::__atomic_base<_IntTp>::operator __int_type() const [with _ITp = unsigned int]’ at /usr/include/c++/12/bits/atomic_base.h:348:20,
    inlined from ‘lean::tag lean::expr_cell::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:83:34,
    inlined from ‘lean::tag lean::expr::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:130:48,
    inlined from ‘lean::tag lean::parser::get_tag(lean::expr)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:272:22,
    inlined from ‘virtual lean::expr lean::parser::save_pos(const lean::expr&, lean::pos_info)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:335:21:
/usr/include/c++/12/bits/atomic_base.h:488:31: warning: ‘unsigned int __atomic_load_4(const volatile void*, int)’ writing 4 bytes into a region of size 0 overflows the destination [-Wstringop-overflow=]
  488 |         return __atomic_load_n(&_M_i, int(__m));
      |                ~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
[ 36%] Building CXX object library/CMakeFiles/library.dir/reducible.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 37%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_aux.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In member function ‘std::__atomic_base<_IntTp>::__int_type std::__atomic_base<_IntTp>::load(std::memory_order) const [with _ITp = unsigned int]’,
    inlined from ‘std::__atomic_base<_IntTp>::operator __int_type() const [with _ITp = unsigned int]’ at /usr/include/c++/12/bits/atomic_base.h:348:20,
    inlined from ‘lean::tag lean::expr_cell::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:83:34,
    inlined from ‘lean::tag lean::expr::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:130:48,
    inlined from ‘lean::tag lean::parser::get_tag(lean::expr)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:272:22,
    inlined from ‘lean::expr lean::parser::update_pos(lean::expr, lean::pos_info)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:347:21:
/usr/include/c++/12/bits/atomic_base.h:488:31: warning: ‘unsigned int __atomic_load_4(const volatile void*, int)’ writing 4 bytes into a region of size 0 overflows the destination [-Wstringop-overflow=]
  488 |         return __atomic_load_n(&_M_i, int(__m));
      |                ~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
[ 38%] Building CXX object library/tactic/CMakeFiles/tactic.dir/tactic_log.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 38%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/decl_cmds.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In member function ‘std::__atomic_base<_IntTp>::__int_type std::__atomic_base<_IntTp>::load(std::memory_order) const [with _ITp = unsigned int]’,
    inlined from ‘std::__atomic_base<_IntTp>::operator __int_type() const [with _ITp = unsigned int]’ at /usr/include/c++/12/bits/atomic_base.h:348:20,
    inlined from ‘lean::tag lean::expr_cell::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:83:34,
    inlined from ‘lean::tag lean::expr::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:130:48,
    inlined from ‘lean::tag lean::parser::get_tag(lean::expr)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:272:22,
    inlined from ‘void lean::parser::erase_pos(const lean::expr&)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:342:21:
/usr/include/c++/12/bits/atomic_base.h:488:31: warning: ‘unsigned int __atomic_load_4(const volatile void*, int)’ writing 4 bytes into a region of size 0 overflows the destination [-Wstringop-overflow=]
  488 |         return __atomic_load_n(&_M_i, int(__m));
      |                ~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/compiler/cse.cpp: In member function ‘void lean::cse_fn::collect_common_subexprs(const lean::buffer<lean::expr>&, const lean::expr&, lean::expr_set&)’:
/workspace/lean-example/_target/deps/lean/src/library/compiler/cse.cpp:153:43: warning: loop variable ‘p’ of type ‘lean::pair<lean::expr, unsigned int>&’ {aka ‘const std::pair<lean::expr, unsigned int>&’} binds to a temporary constructed from type ‘const std::__detail::_Node_const_iterator<std::pair<const lean::expr, unsigned int>, false, true>::value_type’ {aka ‘const std::pair<const lean::expr, unsigned int>’} [-Wrange-loop-construct]
  153 |         for (pair<expr, unsigned> const & p : num_occs_collector.get_num_occs()) {
      |                                           ^
/workspace/lean-example/_target/deps/lean/src/library/compiler/cse.cpp:153:43: note: use non-reference type ‘lean::pair<lean::expr, unsigned int>’ {aka ‘const std::pair<lean::expr, unsigned int>’} to make the copy explicit or ‘const std::__detail::_Node_const_iterator<std::pair<const lean::expr, unsigned int>, false, true>::value_type&’ {aka ‘const std::pair<const lean::expr, unsigned int>&’} to prevent copying
[ 39%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 39%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/inductive_cmds.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 39%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_io.cpp.o
[ 39%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_name.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 39%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_options.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 40%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_format.cpp.o
In member function ‘std::__atomic_base<_IntTp>::__int_type std::__atomic_base<_IntTp>::load(std::memory_order) const [with _ITp = unsigned int]’,
    inlined from ‘std::__atomic_base<_IntTp>::operator __int_type() const [with _ITp = unsigned int]’ at /usr/include/c++/12/bits/atomic_base.h:348:20,
    inlined from ‘lean::tag lean::expr_cell::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:83:34,
    inlined from ‘lean::tag lean::expr::get_tag() const’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:130:48,
    inlined from ‘lean::tag lean::parser::get_tag(lean::expr)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:272:22,
    inlined from ‘void lean::parser::finalize_ast(lean::ast_id, const lean::expr&)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser.cpp:290:21:
/usr/include/c++/12/bits/atomic_base.h:488:31: warning: ‘unsigned int __atomic_load_4(const volatile void*, int)’ writing 4 bytes into a region of size 0 overflows the destination [-Wstringop-overflow=]
  488 |         return __atomic_load_n(&_M_i, int(__m));
      |                ~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 40%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_rb_map.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 41%] Building CXX object library/CMakeFiles/library.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 41%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/dependencies.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 42%] Building CXX object util/CMakeFiles/util.dir/small_object_allocator.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 42%] Building CXX object util/CMakeFiles/util.dir/subscripted_name_set.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 42%] Building CXX object util/CMakeFiles/util.dir/parser_exception.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 42%] Building CXX object util/CMakeFiles/util.dir/name_generator.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 42%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/pp.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 43%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/structure_cmd.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 43%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/structure_instance.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 43%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/init_module.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 43%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_level.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 43%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_expr.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /usr/include/c++/12/bits/shared_ptr_atomic.h:33,
                 from /usr/include/c++/12/memory:78,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/for_each_fn.h:8,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/find_fn.h:8,
                 from /workspace/lean-example/_target/deps/lean/src/library/constructions/injective.cpp:6:
In member function ‘std::__atomic_base<_IntTp>::__int_type std::__atomic_base<_IntTp>::fetch_add(__int_type, std::memory_order) [with _ITp = unsigned int]’,
    inlined from ‘_ITp std::atomic_fetch_add_explicit(atomic<_ITp>*, __atomic_diff_t<_ITp>, memory_order) [with _ITp = unsigned int]’ at /usr/include/c++/12/atomic:1456:28,
    inlined from ‘void lean::expr_cell::inc_ref()’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:65:5,
    inlined from ‘lean::expr::expr(const lean::expr&)’ at /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:112:68,
    inlined from ‘void lean::collect_args(type_context_old&, const expr&, unsigned int, buffer<expr>&, buffer<expr>&, buffer<expr>&, buffer<expr>&)’ at /workspace/lean-example/_target/deps/lean/src/library/constructions/injective.cpp:44:24,
    inlined from ‘lean::expr lean::mk_injective_type_core(const environment&, const name&, const expr&, unsigned int, const level_param_names&, bool)’ at /workspace/lean-example/_target/deps/lean/src/library/constructions/injective.cpp:65:17:
/usr/include/c++/12/bits/atomic_base.h:618:34: warning: ‘unsigned int __atomic_fetch_add_4(volatile void*, unsigned int, int)’ writing 4 bytes into a region of size 0 overflows the destination [-Wstringop-overflow=]
  618 |       { return __atomic_fetch_add(&_M_i, __i, int(__m)); }
      |                ~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~
[ 43%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_exceptional.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 44%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_declaration.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 44%] Building CXX object library/CMakeFiles/library.dir/exception.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 44%] Building CXX object library/CMakeFiles/library.dir/fingerprint.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 44%] Built target constructions
[ 44%] Building CXX object library/CMakeFiles/library.dir/pp_options.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 44%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/type_util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 45%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/decl_attributes.cpp.o
[ 45%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/prenum.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 45%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/print_cmd.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 46%] Building CXX object library/CMakeFiles/library.dir/unfold_macros.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 46%] Building CXX object library/CMakeFiles/library.dir/app_builder.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 46%] Building CXX object library/CMakeFiles/library.dir/projection.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 46%] Building CXX object library/tactic/CMakeFiles/tactic.dir/name_resolution_log.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 46%] Built target compiler
[ 46%] Building CXX object library/CMakeFiles/library.dir/relation_manager.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/CMakeFiles/library.dir/export.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_environment.cpp.o
[ 47%] Building CXX object library/CMakeFiles/library.dir/user_recursors.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/CMakeFiles/library.dir/idx_metavar.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/elaborator.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_list.cpp.o
[ 47%] Built target smt
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_pexpr.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/tactic/CMakeFiles/tactic.dir/intro_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 47%] Building CXX object library/tactic/CMakeFiles/tactic.dir/revert_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 48%] Building CXX object library/tactic/CMakeFiles/tactic.dir/clear_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 48%] Built target util
[ 48%] Building CXX object library/tactic/CMakeFiles/tactic.dir/app_builder_tactics.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 48%] Building CXX object library/tactic/CMakeFiles/tactic.dir/subst_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 48%] Building CXX object library/tactic/CMakeFiles/tactic.dir/exact_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 49%] Building CXX object library/tactic/CMakeFiles/tactic.dir/change_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 49%] Building CXX object checker/CMakeFiles/leanchecker.dir/checker.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 49%] Building CXX object checker/CMakeFiles/leanchecker.dir/text_import.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 50%] Building CXX object checker/CMakeFiles/leanchecker.dir/simple_pp.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 50%] Built target inductive_compiler
[ 50%] Building CXX object library/tactic/CMakeFiles/tactic.dir/assert_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 51%] Building CXX object tests/util/CMakeFiles/name.dir/name.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 51%] Building CXX object tests/util/CMakeFiles/sequence.dir/sequence.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 51%] Building CXX object tests/util/CMakeFiles/sexpr_tst.dir/sexpr.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 51%] Building CXX object library/CMakeFiles/library.dir/noncomputable.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 52%] Building CXX object library/CMakeFiles/library.dir/aux_recursors.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 52%] Building CXX object library/CMakeFiles/library.dir/trace.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 52%] Building CXX object library/CMakeFiles/library.dir/attribute_manager.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 52%] Building CXX object library/CMakeFiles/library.dir/unification_hint.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 52%] Building CXX object library/tactic/CMakeFiles/tactic.dir/apply_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 52%] Building CXX object library/tactic/CMakeFiles/tactic.dir/fun_info_tactics.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 53%] Building CXX object library/tactic/CMakeFiles/tactic.dir/congr_lemma_tactics.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 54%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_task.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 54%] Building CXX object library/tactic/CMakeFiles/tactic.dir/match_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 54%] Building CXX object library/tactic/CMakeFiles/tactic.dir/ac_tactics.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 54%] Building CXX object library/tactic/CMakeFiles/tactic.dir/induction_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 55%] Building CXX object library/tactic/CMakeFiles/tactic.dir/cases_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 55%] Building CXX object library/tactic/CMakeFiles/tactic.dir/generalize_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 55%] Linking CXX executable sequence
In file included from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:15,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr_maps.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/library/replace_visitor.h:8,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/structure_cmd.cpp:12:
/workspace/lean-example/_target/deps/lean/src/util/rc.h: In function ‘lean::optional<std::pair<lean::name, lean::name> > lean::find_method_alias(const environment&, const name&, const name&)’:
/workspace/lean-example/_target/deps/lean/src/util/rc.h:27:47: warning: ‘((lean::name*)((char*)&res + offsetof(lean::optional<std::pair<lean::name, lean::name> >,lean::optional<std::pair<lean::name, lean::name> >::<unnamed>)))[1].lean::name::m_ptr’ may be used uninitialized [-Wmaybe-uninitialized]
   27 | void dec_ref() { if (dec_ref_core()) { dealloc(); } }
      |                                               ^
/workspace/lean-example/_target/deps/lean/src/frontends/lean/structure_cmd.cpp:193:32: note: ‘((lean::name*)((char*)&res + offsetof(lean::optional<std::pair<lean::name, lean::name> >,lean::optional<std::pair<lean::name, lean::name> >::<unnamed>)))[1].lean::name::m_ptr’ was declared here
  193 |     optional<pair<name, name>> res = {};
      |                                ^~~
/workspace/lean-example/_target/deps/lean/src/util/rc.h:27:47: warning: ‘*(lean::name*)((char*)&res + offsetof(lean::optional<std::pair<lean::name, lean::name> >,lean::optional<std::pair<lean::name, lean::name> >::<unnamed>)).lean::name::m_ptr’ may be used uninitialized [-Wmaybe-uninitialized]
   27 | void dec_ref() { if (dec_ref_core()) { dealloc(); } }
      |                                               ^
/workspace/lean-example/_target/deps/lean/src/frontends/lean/structure_cmd.cpp:193:32: note: ‘*(lean::name*)((char*)&res + offsetof(lean::optional<std::pair<lean::name, lean::name> >,lean::optional<std::pair<lean::name, lean::name> >::<unnamed>)).lean::name::m_ptr’ was declared here
  193 |     optional<pair<name, name>> res = {};
      |                                ^~~
In file included from /usr/include/c++/12/bits/stl_algobase.h:64,
                 from /usr/include/c++/12/string:50,
                 from /workspace/lean-example/_target/deps/lean/src/library/relation_manager.cpp:7:
In constructor ‘constexpr std::pair<_T1, _T2>::pair(const _T1&, const _T2&) [with _U1 = lean::name; _U2 = lean::relation_info; typename std::enable_if<(std::_PCC<true, _T1, _T2>::_ConstructiblePair<_U1, _U2>() && std::_PCC<true, _T1, _T2>::_ImplicitlyConvertiblePair<_U1, _U2>()), bool>::type <anonymous> = true; _T1 = lean::name; _T2 = lean::relation_info]’,
    inlined from ‘constexpr std::pair<typename std::__strip_reference_wrapper<typename std::decay<_Tp>::type>::__type, typename std::__strip_reference_wrapper<typename std::decay<_Tp2>::type>::__type> std::make_pair(_T1&&, _T2&&) [with _T1 = const lean::name&; _T2 = const lean::relation_info&]’ at /usr/include/c++/12/bits/stl_pair.h:746:72,
    inlined from ‘lean::pair<T1, T2> lean::mk_pair(const T1&, const T2&) [with T1 = name; T2 = relation_info]’ at /workspace/lean-example/_target/deps/lean/src/util/pair.h:17:33,
    inlined from ‘void lean::rb_map<K, T, CMP>::insert(const K&, const T&) [with K = lean::name; T = lean::relation_info; CMP = lean::name_quick_cmp]’ at /workspace/lean-example/_target/deps/lean/src/util/rb_map.h:34:57,
    inlined from ‘void lean::rel_state::register_rop(const lean::environment&, const lean::name&)’ at /workspace/lean-example/_target/deps/lean/src/library/relation_manager.cpp:101:31:
/usr/include/c++/12/bits/stl_pair.h:412:21: warning: ‘*(unsigned int*)((char*)&rhs_pos + offsetof(lean::optional<unsigned int>,lean::optional<unsigned int>::<unnamed>))’ may be used uninitialized [-Wmaybe-uninitialized]
  412 |       : first(__a), second(__b) { }
      |                     ^~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/relation_manager.cpp: In member function ‘void lean::rel_state::register_rop(const lean::environment&, const lean::name&)’:
/workspace/lean-example/_target/deps/lean/src/library/relation_manager.cpp:83:28: note: ‘*(unsigned int*)((char*)&rhs_pos + offsetof(lean::optional<unsigned int>,lean::optional<unsigned int>::<unnamed>))’ was declared here
   83 |         optional<unsigned> rhs_pos;
      |                            ^~~~~~~
[ 55%] Built target sequence
[ 55%] Building CXX object tests/util/CMakeFiles/format.dir/format.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 55%] Building CXX object library/CMakeFiles/library.dir/local_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Building CXX object library/CMakeFiles/library.dir/metavar_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Linking CXX executable name
[ 56%] Building CXX object library/CMakeFiles/library.dir/type_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Building CXX object library/CMakeFiles/library.dir/export_decl.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Building CXX object library/CMakeFiles/library.dir/delayed_abstraction.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Built target name
[ 56%] Building CXX object tests/util/CMakeFiles/buffer.dir/buffer.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Building CXX object tests/util/CMakeFiles/list.dir/list.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 56%] Linking CXX executable sexpr_tst
[ 57%] Building CXX object library/CMakeFiles/library.dir/fun_info.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 57%] Built target sexpr_tst
[ 57%] Building CXX object library/CMakeFiles/library.dir/congr_lemma.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 58%] Building CXX object tests/util/CMakeFiles/scoped_set.dir/scoped_set.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 58%] Building CXX object tests/util/CMakeFiles/options.dir/options.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 58%] Linking CXX executable format
[ 58%] Building CXX object tests/util/CMakeFiles/scoped_map.dir/scoped_map.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 58%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_int.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 59%] Linking CXX executable buffer
[ 59%] Linking CXX executable leanchecker
[ 59%] Built target format
[ 59%] Built target buffer
[ 59%] Building CXX object tests/util/CMakeFiles/rb_tree.dir/rb_tree.cpp.o
[ 59%] Building CXX object tests/util/CMakeFiles/rb_map.dir/rb_map.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 60%] Building CXX object tests/util/CMakeFiles/exception.dir/exception.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 60%] Building CXX object library/CMakeFiles/library.dir/defeq_canonizer.cpp.o
[ 60%] Built target leanchecker
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 60%] Building CXX object library/tactic/CMakeFiles/tactic.dir/rewrite_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 60%] Building CXX object tests/util/CMakeFiles/bit_tricks.dir/bit_tricks.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 60%] Building CXX object library/CMakeFiles/library.dir/replace_visitor_with_tc.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:16:
In destructor ‘lean::name::~name()’,
    inlined from ‘lean::optional<T>::~optional() [with T = lean::name]’ at /workspace/lean-example/_target/deps/lean/src/util/optional.h:47:23,
    inlined from ‘void lean::structure_cmd_fn::parse_extends()’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/structure_cmd.cpp:472:13:
/workspace/lean-example/_target/deps/lean/src/util/name.h:87:40: warning: ‘*(lean::name*)((char*)&q + offsetof(lean::optional<lean::name>,lean::optional<lean::name>::<unnamed>)).lean::name::m_ptr’ may be used uninitialized [-Wmaybe-uninitialized]
   87 |     ~name() { if (m_ptr) m_ptr->dec_ref(); }
      |                          ~~~~~~~~~~~~~~^~
/workspace/lean-example/_target/deps/lean/src/frontends/lean/structure_cmd.cpp: In member function ‘void lean::structure_cmd_fn::parse_extends()’:
/workspace/lean-example/_target/deps/lean/src/frontends/lean/structure_cmd.cpp:426:45: note: ‘*(lean::name*)((char*)&q + offsetof(lean::optional<lean::name>,lean::optional<lean::name>::<unnamed>)).lean::name::m_ptr’ was declared here
  426 |                 ast_id q_id; optional<name> q; expr parent;
      |                                             ^
[ 61%] Linking CXX executable bit_tricks
[ 61%] Linking CXX executable scoped_map
[ 61%] Linking CXX executable scoped_set
[ 61%] Built target bit_tricks
[ 62%] Building CXX object library/CMakeFiles/library.dir/aux_definition.cpp.o
[ 62%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/match_expr.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 62%] Built target scoped_set
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 62%] Building CXX object library/tactic/CMakeFiles/tactic.dir/unfold_tactic.cpp.o
[ 62%] Building CXX object library/tactic/CMakeFiles/tactic.dir/hsubstitution.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 62%] Building CXX object tests/util/CMakeFiles/hash.dir/hash.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 62%] Built target scoped_map
[ 62%] Linking CXX executable exception
[ 62%] Building CXX object tests/util/CMakeFiles/safe_arith.dir/safe_arith.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 62%] Built target exception
[ 63%] Building CXX object library/tactic/CMakeFiles/tactic.dir/gexpr.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 64%] Linking CXX executable options
[ 65%] Linking CXX executable rb_map
[ 65%] Linking CXX executable hash
[ 65%] Built target hash
[ 65%] Building CXX object library/tactic/CMakeFiles/tactic.dir/elaborate.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 65%] Built target rb_map
[ 65%] Building CXX object library/tactic/CMakeFiles/tactic.dir/init_module.cpp.o
[ 65%] Built target options
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 65%] Building CXX object library/tactic/CMakeFiles/tactic.dir/simp_result.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 65%] Linking CXX executable list
[ 66%] Building CXX object library/tactic/CMakeFiles/tactic.dir/user_attribute.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 66%] Linking CXX executable safe_arith
[ 66%] Built target list
[ 67%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/local_context_adapter.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 67%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/decl_util.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 67%] Building CXX object library/CMakeFiles/library.dir/inverse.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 67%] Built target safe_arith
[ 67%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/definition_cmds.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 67%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/brackets.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 68%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/tactic_notation.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 68%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/info_manager.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 68%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/json.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 68%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/module_parser.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 69%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/interactive.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 69%] Building CXX object library/vm/CMakeFiles/vm.dir/init_module.cpp.o
[ 69%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/completion.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 69%] Building CXX object library/tactic/CMakeFiles/tactic.dir/eval.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 69%] Building CXX object library/tactic/CMakeFiles/tactic.dir/simp_lemmas.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 69%] Building CXX object library/tactic/CMakeFiles/tactic.dir/eqn_lemmas.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 69%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_parser.cpp.o
[ 70%] Building CXX object library/tactic/CMakeFiles/tactic.dir/dsimplify.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 70%] Linking CXX executable rb_tree
[ 70%] Building CXX object library/tactic/CMakeFiles/tactic.dir/simplify.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 70%] Building CXX object library/tactic/CMakeFiles/tactic.dir/vm_monitor.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 70%] Building CXX object library/tactic/CMakeFiles/tactic.dir/destruct_tactic.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 71%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_array.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 71%] Built target rb_tree
[ 71%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_pos_info.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 71%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_float.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 71%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_module_info.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 72%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_override.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 72%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_eformat.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 73%] Building CXX object library/tactic/CMakeFiles/tactic.dir/hole_command.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 73%] Building CXX object library/vm/CMakeFiles/vm.dir/vm_json.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 73%] Building CXX object library/tactic/CMakeFiles/tactic.dir/elaborator_exception.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 73%] Building CXX object tests/util/CMakeFiles/set.dir/set.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 74%] Building CXX object tests/util/CMakeFiles/serializer.dir/serializer.cpp.o
[ 74%] Building CXX object tests/util/CMakeFiles/stackinfo.dir/stackinfo.cpp.o
[ 74%] Building CXX object tests/util/CMakeFiles/optional.dir/optional.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 74%] Building CXX object tests/util/CMakeFiles/trie.dir/trie.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 75%] Building CXX object tests/util/CMakeFiles/lru_cache.dir/lru_cache.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 76%] Linking CXX executable stackinfo
[ 76%] Linking CXX executable set
[ 76%] Linking CXX executable optional
[ 76%] Built target set
[ 76%] Built target stackinfo
[ 76%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/user_notation.cpp.o
[ 76%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/user_command.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 76%] Building CXX object tests/util/CMakeFiles/worker_queue.dir/worker_queue.cpp.o
[ 76%] Building CXX object tests/util/CMakeFiles/thread.dir/thread.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 76%] Built target optional
[ 77%] Building CXX object frontends/lean/CMakeFiles/lean_frontend.dir/widget.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 77%] Building CXX object library/CMakeFiles/library.dir/pattern_attribute.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 77%] Building CXX object library/CMakeFiles/library.dir/choice.cpp.o
[ 78%] Building CXX object library/CMakeFiles/library.dir/locals.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 78%] Building CXX object library/CMakeFiles/library.dir/normalize.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 78%] Linking CXX executable lru_cache
[ 78%] Building CXX object library/CMakeFiles/library.dir/discr_tree.cpp.o
[ 78%] Building CXX object library/tactic/CMakeFiles/tactic.dir/algebraic_normalizer.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 78%] Building CXX object library/tactic/CMakeFiles/tactic.dir/tactic_evaluator.cpp.o
[ 78%] Building CXX object library/CMakeFiles/library.dir/mt_task_queue.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 79%] Building CXX object library/CMakeFiles/library.dir/st_task_queue.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 79%] Built target lru_cache
[ 79%] Linking CXX executable thread
[ 79%] Building CXX object library/CMakeFiles/library.dir/library_task_builder.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 80%] Linking CXX executable worker_queue
[ 80%] Building CXX object library/CMakeFiles/library.dir/eval_helper.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 80%] Building CXX object library/CMakeFiles/library.dir/feature_search.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 80%] Built target thread
[ 80%] Building CXX object tests/util/CMakeFiles/bitap_fuzzy_search.dir/bitap_fuzzy_search.cpp.o
[ 80%] Built target worker_queue
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 81%] Building CXX object tests/util/numerics/CMakeFiles/mpq.dir/mpq.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 81%] Building CXX object tests/util/numerics/CMakeFiles/mpz.dir/mpz.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 81%] Building CXX object library/CMakeFiles/library.dir/messages.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
In file included from /usr/include/c++/12/bits/new_allocator.h:36,
                 from /usr/include/c++/12/x86_64-redhat-linux/bits/c++allocator.h:33,
                 from /usr/include/c++/12/bits/allocator.h:46,
                 from /usr/include/c++/12/string:41,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/library/vm/vm_json.cpp:8:
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
In file included from /workspace/lean-example/_target/deps/lean/src/util/lean_json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:19,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/environment.h:17,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/json.h:11:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:38: note: ‘<anonymous>’ declared here
 9059 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:34: note: ‘<anonymous>’ declared here
 9113 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:38: note: ‘<anonymous>’ declared here
 9138 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:34: note: ‘<anonymous>’ declared here
 9169 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:24:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:26: note: ‘<anonymous>’ declared here
 9222 |                 result = basic_json(value_t::discarded);
      |                          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[ 81%] Linking CXX executable serializer
[ 81%] Building CXX object library/tactic/CMakeFiles/tactic.dir/vm_local_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 81%] Linking CXX executable bitap_fuzzy_search
[ 81%] Built target serializer
[ 82%] Building CXX object library/tactic/CMakeFiles/tactic.dir/vm_type_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 83%] Building CXX object library/CMakeFiles/library.dir/message_builder.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 83%] Building CXX object library/CMakeFiles/library.dir/module_mgr.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 83%] Building CXX object library/CMakeFiles/library.dir/comp_val.cpp.o
[ 83%] Building CXX object library/CMakeFiles/library.dir/documentation.cpp.o
[ 84%] Linking CXX executable trie
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 84%] Built target bitap_fuzzy_search
[ 85%] Building CXX object library/CMakeFiles/library.dir/check.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 85%] Building CXX object library/CMakeFiles/library.dir/parray.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 85%] Building CXX object library/CMakeFiles/library.dir/process.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 85%] Built target trie
[ 85%] Building CXX object library/CMakeFiles/library.dir/pipe.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 86%] Building CXX object library/CMakeFiles/library.dir/handle.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 86%] Building CXX object library/CMakeFiles/library.dir/profiling.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 86%] Linking CXX executable mpq
[ 86%] Building CXX object library/CMakeFiles/library.dir/time_task.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 86%] Linking CXX executable mpz
[ 86%] Building CXX object library/CMakeFiles/library.dir/abstract_context_cache.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 87%] Building CXX object library/CMakeFiles/library.dir/context_cache.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 87%] Built target mpq
[ 87%] Building CXX object library/CMakeFiles/library.dir/unique_id.cpp.o
[ 87%] Built target mpz
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 87%] Building CXX object library/CMakeFiles/library.dir/persistent_context_cache.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 87%] Building CXX object library/CMakeFiles/library.dir/elab_context.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 87%] Building CXX object library/CMakeFiles/library.dir/expr_address.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 88%] Building CXX object library/CMakeFiles/library.dir/tlean_exporter.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 88%] Building CXX object library/CMakeFiles/library.dir/ast_exporter.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
/workspace/lean-example/_target/deps/lean/src/library/documentation.cpp: In function ‘void lean::rtrim(std::string&)’:
/workspace/lean-example/_target/deps/lean/src/library/documentation.cpp:80:58: warning: ‘std::pointer_to_unary_function<_Arg, _Result> std::ptr_fun(_Result (*)(_Arg)) [with _Arg = int; _Result = int]’ is deprecated: use 'std::function' instead [-Wdeprecated-declarations]
   80 |                          std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end());
      |                                    ~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~
In file included from /usr/include/c++/12/string:48,
                 from /workspace/lean-example/_target/deps/lean/src/library/documentation.cpp:7:
/usr/include/c++/12/bits/stl_function.h:1126:5: note: declared here
 1126 |     ptr_fun(_Result (*__x)(_Arg))
      |     ^~~~~~~
In file included from /workspace/lean-example/_target/deps/lean/src/frontends/lean/widget.cpp:19:
In destructor ‘lean::vdom::~vdom()’,
    inlined from ‘lean::optional<T>::~optional() [with T = lean::vdom]’ at /workspace/lean-example/_target/deps/lean/src/util/optional.h:47:23,
    inlined from ‘lean::vdom lean::render_element(const vm_obj&, std::vector<component_instance*>&, event_handlers&, const list<unsigned int>&)’ at /workspace/lean-example/_target/deps/lean/src/frontends/lean/widget.cpp:479:1:
/workspace/lean-example/_target/deps/lean/src/frontends/lean/widget.h:55:37: warning: ‘*(lean::vdom*)((char*)&tooltip + offsetof(lean::optional<lean::vdom>,lean::optional<lean::vdom>::<unnamed>)).lean::vdom::m_ptr’ may be used uninitialized [-Wmaybe-uninitialized]
   55 |   ~vdom() {if (m_ptr) m_ptr->dec_ref(); }
      |                       ~~~~~~~~~~~~~~^~
/workspace/lean-example/_target/deps/lean/src/frontends/lean/widget.cpp: In function ‘lean::vdom lean::render_element(const vm_obj&, std::vector<component_instance*>&, event_handlers&, const list<unsigned int>&)’:
/workspace/lean-example/_target/deps/lean/src/frontends/lean/widget.cpp:424:20: note: ‘*(lean::vdom*)((char*)&tooltip + offsetof(lean::optional<lean::vdom>,lean::optional<lean::vdom>::<unnamed>)).lean::vdom::m_ptr’ was declared here
  424 |     optional<vdom> tooltip;
      |                    ^~~~~~~
[ 88%] Built target vm
[ 88%] Built target tactic
/workspace/lean-example/_target/deps/lean/src/library/module_mgr.cpp: In member function ‘virtual std::shared_ptr<lean::module_info> lean::fs_module_vfs::load_module(const lean::module_id&, bool)’:
/workspace/lean-example/_target/deps/lean/src/library/module_mgr.cpp:494:40: warning: ‘*(long long unsigned int*)((char*)&src_hash + offsetof(lean::optional<long long unsigned int>,lean::optional<long long unsigned int>::<unnamed>))’ may be used uninitialized [-Wmaybe-uninitialized]
  494 |                 (!src_hash.has_value() || *src_hash == *olean_src_hash)) {
      |                 ~~~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/module_mgr.cpp:478:22: note: ‘*(long long unsigned int*)((char*)&src_hash + offsetof(lean::optional<long long unsigned int>,lean::optional<long long unsigned int>::<unnamed>))’ was declared here
  478 |     optional<uint64> src_hash = {};
      |                      ^~~~~~~~
[ 88%] Built target lean_frontend
[ 88%] Built target library
[ 88%] Building CXX object tests/library/CMakeFiles/head_map.dir/head_map.cpp.o
[ 88%] Building CXX object tests/kernel/CMakeFiles/free_vars.dir/free_vars.cpp.o
[ 88%] Building CXX object tests/kernel/CMakeFiles/instantiate.dir/instantiate.cpp.o
[ 88%] Building CXX object tests/library/CMakeFiles/parray.dir/parray.cpp.o
[ 88%] Linking CXX static library libleanstatic.a
[ 89%] Building CXX object tests/kernel/CMakeFiles/environment.dir/environment.cpp.o
[ 89%] Building CXX object tests/library/CMakeFiles/occurs.dir/occurs.cpp.o
[ 89%] Building CXX object tests/kernel/CMakeFiles/level.dir/level.cpp.o
[ 89%] Building CXX object tests/kernel/CMakeFiles/expr.dir/expr.cpp.o
[ 89%] Building CXX object tests/library/CMakeFiles/expr_lt.dir/expr_lt.cpp.o
[ 89%] Building CXX object tests/kernel/CMakeFiles/max_sharing.dir/max_sharing.cpp.o
[ 89%] Building CXX object tests/kernel/CMakeFiles/replace.dir/replace.cpp.o
[ 90%] Building CXX object tests/frontends/lean/CMakeFiles/lean_scanner.dir/scanner.cpp.o
[ 90%] Building CXX object tests/library/CMakeFiles/phashtable.dir/phashtable.cpp.o
[ 91%] Building CXX object tests/library/CMakeFiles/delayed_abstraction.dir/delayed_abstraction.cpp.o
[ 91%] Building CXX object tests/library/CMakeFiles/deep_copy.dir/deep_copy.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 91%] Built target leanstatic
[ 91%] Building CXX object shell/CMakeFiles/lean.dir/lean.cpp.o
[ 91%] Building CXX object shell/CMakeFiles/lean_js.dir/lean_js_main.cpp.o
[ 91%] Building CXX object shell/CMakeFiles/lean_js.dir/lean_js.cpp.o
[ 91%] Building CXX object shell/CMakeFiles/lean.dir/server.cpp.o
[ 91%] Building CXX object shell/CMakeFiles/lean_js.dir/server.cpp.o
[ 91%] Building CXX object tests/shell/CMakeFiles/shell_test.dir/shell.cpp.o
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
cc1plus: note: disable pass tree-ifcombine for functions in the range of [0, 4294967295]
[ 91%] Linking CXX executable shell_test
[ 91%] Linking CXX executable deep_copy
[ 92%] Linking CXX executable instantiate
[ 92%] Linking CXX executable max_sharing
[ 93%] Linking CXX executable occurs
In file included from /workspace/lean-example/_target/deps/lean/src/library/phashtable.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/tests/library/phashtable.cpp:18:
/workspace/lean-example/_target/deps/lean/src/library/parray.h: In instantiation of ‘static lean::parray<T, ThreadSafe>::cell* lean::parray<T, ThreadSafe>::copy(unsigned int, cell*, const cell_buffer&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true; cell_buffer = lean::buffer<lean::parray<lean::default_map_entry<unsigned int, unsigned int>, true>::cell*, 1024>]’:
/workspace/lean-example/_target/deps/lean/src/library/parray.h:349:32:   required from ‘static void lean::parray<T, ThreadSafe>::reroot(cell*) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true]’
/workspace/lean-example/_target/deps/lean/src/library/parray.h:662:23:   required from ‘lean::parray<T, ThreadSafe>::exclusive_access::exclusive_access(lean::parray<T, ThreadSafe>&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true]’
/workspace/lean-example/_target/deps/lean/src/library/phashtable.h:188:42:   required from ‘void lean::phashtable_core<Entry, HashProc, EqProc, ThreadSafe>::insert(const data&) [with Entry = lean::default_map_entry<unsigned int, unsigned int>; HashProc = lean::phashtable2map<lean::default_map_entry<unsigned int, unsigned int>, std::hash<unsigned int>, std::equal_to<unsigned int>, true>::entry_hash_proc; EqProc = lean::phashtable2map<lean::default_map_entry<unsigned int, unsigned int>, std::hash<unsigned int>, std::equal_to<unsigned int>, true>::entry_eq_proc; bool ThreadSafe = true; data = lean::key_value_pair<unsigned int, unsigned int>]’
/workspace/lean-example/_target/deps/lean/src/library/phash_map.h:86:23:   required from ‘void lean::phashtable2map<Entry, HashProc, EqProc, ThreadSafe>::insert(const key&, const value&) [with Entry = lean::default_map_entry<unsigned int, unsigned int>; HashProc = std::hash<unsigned int>; EqProc = std::equal_to<unsigned int>; bool ThreadSafe = true; key = unsigned int; value = unsigned int]’
/workspace/lean-example/_target/deps/lean/src/tests/library/phashtable.cpp:149:13:   required from here
/workspace/lean-example/_target/deps/lean/src/library/parray.h:290:17: warning: implicitly-declared ‘lean::default_map_entry<unsigned int, unsigned int>::default_map_entry(const lean::default_map_entry<unsigned int, unsigned int>&)’ is deprecated [-Wdeprecated-copy]
  290 |                 new (r->m_values + r->m_size) T(p->elem());
      |                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from /workspace/lean-example/_target/deps/lean/src/tests/library/phashtable.cpp:19:
/workspace/lean-example/_target/deps/lean/src/library/phash_map.h:34:25: note: because ‘lean::default_map_entry<unsigned int, unsigned int>’ has user-provided ‘lean::default_map_entry<Key, Value>& lean::default_map_entry<Key, Value>::operator=(const lean::default_map_entry<Key, Value>&) [with Key = unsigned int; Value = unsigned int]’
   34 |     default_map_entry & operator=(default_map_entry const & src) {
      |                         ^~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/parray.h: In instantiation of ‘static void lean::parray<T, ThreadSafe>::reroot(cell*, cell*, const cell_buffer&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true; cell_buffer = lean::buffer<lean::parray<lean::default_map_entry<unsigned int, unsigned int>, true>::cell*, 1024>]’:
/workspace/lean-example/_target/deps/lean/src/library/parray.h:356:19:   required from ‘static void lean::parray<T, ThreadSafe>::reroot(cell*) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true]’
/workspace/lean-example/_target/deps/lean/src/library/parray.h:662:23:   required from ‘lean::parray<T, ThreadSafe>::exclusive_access::exclusive_access(lean::parray<T, ThreadSafe>&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true]’
/workspace/lean-example/_target/deps/lean/src/library/phashtable.h:188:42:   required from ‘void lean::phashtable_core<Entry, HashProc, EqProc, ThreadSafe>::insert(const data&) [with Entry = lean::default_map_entry<unsigned int, unsigned int>; HashProc = lean::phashtable2map<lean::default_map_entry<unsigned int, unsigned int>, std::hash<unsigned int>, std::equal_to<unsigned int>, true>::entry_hash_proc; EqProc = lean::phashtable2map<lean::default_map_entry<unsigned int, unsigned int>, std::hash<unsigned int>, std::equal_to<unsigned int>, true>::entry_eq_proc; bool ThreadSafe = true; data = lean::key_value_pair<unsigned int, unsigned int>]’
/workspace/lean-example/_target/deps/lean/src/library/phash_map.h:86:23:   required from ‘void lean::phashtable2map<Entry, HashProc, EqProc, ThreadSafe>::insert(const key&, const value&) [with Entry = lean::default_map_entry<unsigned int, unsigned int>; HashProc = std::hash<unsigned int>; EqProc = std::equal_to<unsigned int>; bool ThreadSafe = true; key = unsigned int; value = unsigned int]’
/workspace/lean-example/_target/deps/lean/src/tests/library/phashtable.cpp:149:13:   required from here
/workspace/lean-example/_target/deps/lean/src/library/parray.h:222:17: warning: implicitly-declared ‘lean::default_map_entry<unsigned int, unsigned int>::default_map_entry(const lean::default_map_entry<unsigned int, unsigned int>&)’ is deprecated [-Wdeprecated-copy]
  222 |                 new (vs + sz) T(p->elem());
      |                 ^~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/phash_map.h:34:25: note: because ‘lean::default_map_entry<unsigned int, unsigned int>’ has user-provided ‘lean::default_map_entry<Key, Value>& lean::default_map_entry<Key, Value>::operator=(const lean::default_map_entry<Key, Value>&) [with Key = unsigned int; Value = unsigned int]’
   34 |     default_map_entry & operator=(default_map_entry const & src) {
      |                         ^~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/parray.h: In instantiation of ‘static T* lean::parray<T, ThreadSafe>::mk_elem_copy(const T&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true]’:
/workspace/lean-example/_target/deps/lean/src/library/parray.h:432:49:   required from ‘static lean::parray<T, ThreadSafe>::cell* lean::parray<T, ThreadSafe>::write_aux(cell*, size_t, const T&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true; size_t = long unsigned int]’
/workspace/lean-example/_target/deps/lean/src/library/parray.h:685:39:   required from ‘void lean::parray<T, ThreadSafe>::exclusive_access::set(size_t, const T&) [with T = lean::default_map_entry<unsigned int, unsigned int>; bool ThreadSafe = true; size_t = long unsigned int]’
/workspace/lean-example/_target/deps/lean/src/library/phashtable.h:197:13:   required from ‘void lean::phashtable_core<Entry, HashProc, EqProc, ThreadSafe>::insert(const data&) [with Entry = lean::default_map_entry<unsigned int, unsigned int>; HashProc = lean::phashtable2map<lean::default_map_entry<unsigned int, unsigned int>, std::hash<unsigned int>, std::equal_to<unsigned int>, true>::entry_hash_proc; EqProc = lean::phashtable2map<lean::default_map_entry<unsigned int, unsigned int>, std::hash<unsigned int>, std::equal_to<unsigned int>, true>::entry_eq_proc; bool ThreadSafe = true; data = lean::key_value_pair<unsigned int, unsigned int>]’
/workspace/lean-example/_target/deps/lean/src/library/phash_map.h:86:23:   required from ‘void lean::phashtable2map<Entry, HashProc, EqProc, ThreadSafe>::insert(const key&, const value&) [with Entry = lean::default_map_entry<unsigned int, unsigned int>; HashProc = std::hash<unsigned int>; EqProc = std::equal_to<unsigned int>; bool ThreadSafe = true; key = unsigned int; value = unsigned int]’
/workspace/lean-example/_target/deps/lean/src/tests/library/phashtable.cpp:149:13:   required from here
/workspace/lean-example/_target/deps/lean/src/library/parray.h:174:16: warning: implicitly-declared ‘lean::default_map_entry<unsigned int, unsigned int>::default_map_entry(const lean::default_map_entry<unsigned int, unsigned int>&)’ is deprecated [-Wdeprecated-copy]
  174 |         return new (get_elem_allocator().allocate()) T(e);
      |                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/workspace/lean-example/_target/deps/lean/src/library/phash_map.h:34:25: note: because ‘lean::default_map_entry<unsigned int, unsigned int>’ has user-provided ‘lean::default_map_entry<Key, Value>& lean::default_map_entry<Key, Value>::operator=(const lean::default_map_entry<Key, Value>&) [with Key = unsigned int; Value = unsigned int]’
   34 |     default_map_entry & operator=(default_map_entry const & src) {
      |                         ^~~~~~~~
[ 94%] Linking CXX executable level
[ 95%] Linking CXX executable expr_lt
[ 96%] Linking CXX executable free_vars
[ 97%] Linking CXX executable replace
[ 97%] Built target shell_test
[ 97%] Linking CXX executable delayed_abstraction
[ 97%] Linking CXX executable environment
[ 97%] Linking CXX executable lean_scanner
[ 97%] Built target deep_copy
[ 97%] Built target instantiate
[ 97%] Built target max_sharing
[ 97%] Built target expr_lt
[ 97%] Built target occurs
[ 97%] Built target level
[ 97%] Built target free_vars
[ 97%] Built target replace
[ 98%] Linking CXX executable head_map
[ 98%] Built target delayed_abstraction
[ 98%] Built target environment
[ 98%] Built target lean_scanner
[ 98%] Linking CXX executable parray
[ 98%] Linking CXX executable expr
[ 98%] Built target head_map
In file included from /usr/include/c++/12/bits/new_allocator.h:36,
                 from /usr/include/c++/12/x86_64-redhat-linux/bits/c++allocator.h:33,
                 from /usr/include/c++/12/bits/allocator.h:46,
                 from /usr/include/c++/12/string:41,
                 from /workspace/lean-example/_target/deps/lean/src/shell/lean_js.cpp:7:
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
In file included from /workspace/lean-example/_target/deps/lean/src/util/lean_json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:19,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/pos_info_provider.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/library/abstract_parser.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser_state.h:12,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/module_parser.h:14,
                 from /workspace/lean-example/_target/deps/lean/src/library/module_mgr.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/shell/lean_js.cpp:8:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:38: note: ‘<anonymous>’ declared here
 9059 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:34: note: ‘<anonymous>’ declared here
 9113 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:38: note: ‘<anonymous>’ declared here
 9138 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:34: note: ‘<anonymous>’ declared here
 9169 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:24:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:26: note: ‘<anonymous>’ declared here
 9222 |                 result = basic_json(value_t::discarded);
      |                          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[ 99%] Linking CXX executable phashtable
[ 99%] Built target parray
[ 99%] Built target expr
[ 99%] Built target phashtable
In file included from /usr/include/c++/12/bits/stl_pair.h:61,
                 from /usr/include/c++/12/bits/stl_algobase.h:64,
                 from /usr/include/c++/12/list:60,
                 from /workspace/lean-example/_target/deps/lean/src/shell/server.cpp:14:
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
In file included from /workspace/lean-example/_target/deps/lean/src/util/lean_json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:19,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/pos_info_provider.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/library/abstract_parser.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser_state.h:12,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/module_parser.h:14,
                 from /workspace/lean-example/_target/deps/lean/src/shell/server.cpp:19:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:38: note: ‘<anonymous>’ declared here
 9059 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:34: note: ‘<anonymous>’ declared here
 9113 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:38: note: ‘<anonymous>’ declared here
 9138 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:34: note: ‘<anonymous>’ declared here
 9169 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:24:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:26: note: ‘<anonymous>’ declared here
 9222 |                 result = basic_json(value_t::discarded);
      |                          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from /usr/include/c++/12/bits/stl_pair.h:61,
                 from /usr/include/c++/12/bits/stl_algobase.h:64,
                 from /usr/include/c++/12/list:60,
                 from /workspace/lean-example/_target/deps/lean/src/shell/server.cpp:14:
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
In file included from /workspace/lean-example/_target/deps/lean/src/util/lean_json.h:9,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/expr.h:19,
                 from /workspace/lean-example/_target/deps/lean/src/kernel/pos_info_provider.h:10,
                 from /workspace/lean-example/_target/deps/lean/src/library/abstract_parser.h:13,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/parser_state.h:12,
                 from /workspace/lean-example/_target/deps/lean/src/frontends/lean/module_parser.h:14,
                 from /workspace/lean-example/_target/deps/lean/src/shell/server.cpp:19:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9059:38: note: ‘<anonymous>’ declared here
 9059 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9113:34: note: ‘<anonymous>’ declared here
 9113 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:36:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9138:38: note: ‘<anonymous>’ declared here
 9138 |                             result = basic_json(value_t::discarded);
      |                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:32:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9169:34: note: ‘<anonymous>’ declared here
 9169 |                         result = basic_json(value_t::discarded);
      |                                  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In function ‘std::_Require<std::__not_<std::__is_tuple_like<_Tp> >, std::is_move_constructible<_Tp>, std::is_move_assignable<_Tp> > std::swap(_Tp&, _Tp&) [with _Tp = nlohmann::basic_json<>::json_value]’,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::value_type& nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::operator=(nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:2103:13,
    inlined from ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’ at /workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:24:
/usr/include/c++/12/bits/move.h:205:7: warning: ‘<unnamed>.nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long int, long unsigned int, double, std::allocator>::m_value’ may be used uninitialized [-Wmaybe-uninitialized]
  205 |       __a = _GLIBCXX_MOVE(__b);
      |       ^~~
/workspace/lean-example/_target/deps/lean/src/util/json.hpp: In member function ‘nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType> nlohmann::basic_json<ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType>::parser::parse_internal(bool) [with ObjectType = std::map; ArrayType = std::vector; StringType = std::__cxx11::basic_string<char>; BooleanType = bool; NumberIntegerType = long int; NumberUnsignedType = long unsigned int; NumberFloatType = double; AllocatorType = std::allocator]’:
/workspace/lean-example/_target/deps/lean/src/util/json.hpp:9222:26: note: ‘<anonymous>’ declared here
 9222 |                 result = basic_json(value_t::discarded);
      |                          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
[100%] Linking CXX executable lean
[100%] Linking CXX executable lean_js
[100%] Built target lean
[100%] Built target bin_lean
[100%] Built target lean_js
[100%] Built target standard_lib
[100%] Built target leanpkg
configuring lean-example 0.1
2023-07-08 03:23:21.923 | INFO     | __main__:main:143 - Tracing lean-example
  0%|          | 0/1585 [00:00<?, ?it/s]2023-07-07 20:23:36.927 | DEBUG    | lean_dojo.data_extraction.traced_data:from_traced_files:1199 - Parsing 164 *.ast.json files in /raid/kaiyu/tmp/tmpukon9kz5/lean-example with 31 workers
2023-07-07 20:23:38,901 INFO worker.py:1627 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
100%|████████████████████████████████████████████| 164/164 [00:04<00:00, 35.18it/s]
2023-07-07 20:23:47.883 | DEBUG    | lean_dojo.data_extraction.lean:__post_init__:312 - Querying the commit hash for lean v3.50.3
2023-07-07 20:23:51.952 | DEBUG    | lean_dojo.data_extraction.traced_data:save_to_disk:1246 - Saving 164 traced XML files to /raid/kaiyu/tmp/tmpukon9kz5/lean-example with 31 workers
2023-07-07 20:23:53,705 INFO worker.py:1627 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
100%|████████████████████████████████████████████| 164/164 [00:03<00:00, 53.26it/s]
2023-07-07 20:24:01.839 | INFO     | lean_dojo.data_extraction.trace:trace:164 - Loading the traced repo from /home/kaiyu/.cache/lean_dojo/Some-random-lean-example-4067a13790e7d02af9cda2f4ab249b3f88ff9884/lean-example
2023-07-07 20:24:01.861 | DEBUG    | lean_dojo.data_extraction.traced_data:load_from_disk:1273 - Loading 164 traced XML files from /raid/kaiyu/.cache/lean_dojo/Some-random-lean-example-4067a13790e7d02af9cda2f4ab249b3f88ff9884/lean-example with 31 workers
2023-07-07 20:24:03,616 INFO worker.py:1627 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
100%|████████████████████████████████████████████| 164/164 [00:05<00:00, 28.59it/s]
2023-07-07 20:24:13.873 | DEBUG    | lean_dojo.data_extraction.lean:__post_init__:312 - Querying the commit hash for lean v3.50.3
Out[1]: TracedRepo(repo=LeanGitRepo(url='https://github.com/Some-random/lean-example', commit='4067a13790e7d02af9cda2f4ab249b3f88ff9884'), dependencies={'lean': LeanGitRepo(url='https://github.com/leanprover-community/lean', commit='855e5b74e3a52a40552e8f067169d747d48743fd')}, root_dir=PosixPath('/raid/kaiyu/.cache/lean_dojo/Some-random-lean-example-4067a13790e7d02af9cda2f4ab249b3f88ff9884/lean-example'))
Some-random commented 1 year ago

Thanks for the detailed log! I've actually solved this problem by downgrading python to 3.9 (was using 3.10). Looks like the error might be related to type hints introduced in python 3.9.

yangky11 commented 1 year ago

Hmm.. I'm not sure if that's the problem. I was also using 3.10. But I'm glad it's resolved.