Can't build lean due to old libuv

Stream: lean4 dev

[Mario Carneiro]

Currently building lean on ubuntu results in:

$ cmake --preset release
$ make -C build/release
...
/home/mario/Documents/lean/lean4/stage0/src/runtime/uv/system.cpp: In function ‘lean_object* lean::lean_uv_os_get_group(uint64_t, lean::obj_arg)’:
/home/mario/Documents/lean/lean4/stage0/src/runtime/uv/system.cpp:197:5: error: ‘uv_group_t’ was not declared in this scope; did you mean ‘uv_loop_t’?
  197 |     uv_group_t group;
      |     ^~~~~~~~~~
      |     uv_loop_t
/home/mario/Documents/lean/lean4/stage0/src/runtime/uv/system.cpp:198:35: error: ‘group’ was not declared in this scope
  198 |     int result = uv_os_get_group(&group, gid);
      |                                   ^~~~~
/home/mario/Documents/lean/lean4/stage0/src/runtime/uv/system.cpp:198:18: error: ‘uv_os_get_group’ was not declared in this scope; did you mean ‘lean_uv_os_get_group’?
  198 |     int result = uv_os_get_group(&group, gid);
      |                  ^~~~~~~~~~~~~~~
      |                  lean_uv_os_get_group

I traced the issue down to an addition to libuv which is available only in v1.45.0+, while apt only has 1.43:

$ sudo apt install libuv1-dev
Reading package lists... Done
Building dependency tree... Done
Reading state information... Done
libuv1-dev is already the newest version (1.43.0-1ubuntu0.1).
0 upgraded, 0 newly installed, 0 to remove and 108 not upgraded.

[Mario Carneiro]

cc: @Sofia Rodrigues

[Henrik Böving]

When you say "apt only has" I assume you are using ubuntu 22.04 or older as every release after that has compatible versions yes?

[Mario Carneiro]

yep, it's 22.04

[Henrik Böving]

I guess that opens the question of what versions of popular Linux distros Lean wants to support then

[Mario Carneiro]

it wouldn't be that hard to just fail at runtime here in the worst case, the function in question isn't even used

[Markus Himmel]

We already have conditional compilation to support both libuv pre-1.45.0 and post-1.45.0 in at least one other place, so I'll prepare a fix that does the same in this case.

[Markus Himmel]

@Mario Carneiro The fix and the corresponding stage0 update have now landed on master, so please let me know if you're still having problems on the latest master.

[Mario Carneiro]

@Markus Himmel Progress, but it still has problems. It fails at uv_get_available_memory() (also added in 1.45)

[Mario Carneiro]

I added a similar ifdef as in lean4#9644 and it seems to be building

[Markus Himmel]

Thanks for checking. I'm not at a computer right now, but happy to merge a PR that's analogous go 9644

[Mario Carneiro]

did you update stage0? The changes I needed to make are actually to the stage0 versions of the cpp files

[Markus Himmel]

Yes, I triggered a stage0 update after the PR was merged

[Mario Carneiro]

lean4#9652