Zulip Chat Archive

Stream: lean4

Topic: Problems when writing a socket package


Xubai Wang (Sep 28 2021 at 14:49):

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 (Sep 28 2021 at 14:53):

(deleted)

Xubai Wang (Sep 28 2021 at 15:07):

  1. 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 (Sep 28 2021 at 15:17):

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


Last updated: Dec 20 2023 at 11:08 UTC