Problems when writing a socket package

Stream: lean4

[Xubai Wang]

In the past few days, I was trying to make a package for socket programming, but some problems arise immediately.

1. We cannot write platform-specific and feature-specific code in Lean 4 now. I'm referring to something like#ifdef in C/C++ and #[cfg(...)] in Rust. For example, some address families are not available on every platform, it would be useful to specify the platform like this (may be in other formats):

inductive AddressFamily
  | net
  | inet6
  | @[feature = "unix"] @[platform "windows ≥ 10" "unix" "macos"] unix

Is it possible to do such things in the Lean elaboration process? (I'm not familiar with it. Any learning resources that I can start from?)

[Xubai Wang]

(deleted)

[Xubai Wang]

2. Lean does not have a low level data representation that can interoperate with C. In Rust, the #[repr(C)] can be used, and we can directly pass the struct to C functions.

#[repr(C)]
pub struct sockaddr {
    pub sa_family: u16,
    pub sa_data: [c_char; 14],
}

In Lean, we have to write a wrapper for every structure and every function to make them "boxed", which involves a bunch of lean_ctor functions, which is quite frustrating and inconvenient for quick exploration.

[Xubai Wang]

By the way, the usage of Task and AsyncList is a bit confusing for me. Could anyone brief me about how to write multithreading or coroutine program in Lean? :D