Zulip Chat Archive

Stream: lean4

Topic: build issue


view this post on Zulip Reid Barton (Jan 25 2021 at 21:33):

I'm getting this error when I try to build the current version:

/home/rwbarton/math/lean/lean4/stage0/src/runtime/io.cpp: In function ‘lean::object* lean::lean_io_get_num_heartbeats(lean::obj_arg)’:
/home/rwbarton/math/lean/lean4/stage0/src/runtime/io.cpp:416:47: error: ‘get_num_heartbeats’ was not declared in this scope; did you mean ‘lean_io_get_num_heartbeats’?
  416 |     return io_result_mk_ok(lean_uint64_to_nat(get_num_heartbeats()));
      |                                               ^~~~~~~~~~~~~~~~~~
      |                                               lean_io_get_num_heartbeats

Is this some bootstrapping issue?

view this post on Zulip Reid Barton (Jan 25 2021 at 21:36):

I'm going to see if it persists after make clean

view this post on Zulip Reid Barton (Jan 25 2021 at 21:39):

ok, seems like make clean fixed it


Last updated: May 18 2021 at 23:14 UTC