Platform Dependent Conditional Compilation in Lake?

Stream: lean4

[Siddharth Bhat]

I'm wondering how one does conditional compilation in lake for different platforms? In particular, if one wants something like rust's winit to setup platform specific APIs for opening a window ?

[Mac Malone]

I think the current strategy for this is to write some custom logic in a lakefile.lean making use of System.Platform primitives. LeanCopilot's lakefile.lean is a popular example of this (though prehaps not the most concise or modern example).

One of my focus areas for this quarter is FFI papercuts, so I am hoping to improve the experience around here. I would be interest in any ideas or concerns you might have.

[Siddharth Bhat]

I've been looking at writing low-level libraries for graphics programming, so the bottom of stack involves:

• platform dependent code for creating windows, ala winit, where it would be really nice to have rust-like platform-ifdefs and includes for the builds as well as individual definitions.
• openGL binders ala glew, where it would be nice if Lean learnt how to open shared objects / DLLs. I would imagine that having support for something like pkg-config on Linux is far too out of scope, though. I'm not sure how Rust libraries do this to be honest.

[Mac Malone]

@Siddharth Bhat To your two points:

• ifdefs can generally be implemented in Lean via some mixture of metaprogramming, plain conditionals, ifdefs in FFI shims, and opaque definitions.
• There is docs#Lean.loadDynlib, but there is no way to execute a foreign symbol without a compiled @[extern] decalaration.

[Siddharth Bhat]

• ifdefs can generally be implemented in Lean via some mixture of metaprogramming, plain conditionals, ifdefs in FFI shims, and opaque definitions.

Thanks for the thoughts, and I agree.

I do wonder if having a lower-barrier attribute like @[platform("windows")] (and also possibly @[triple("x86-64-unknown-linux")) would be benificial, to expose the metaprogramming necessary behind a stable API interface. Essentially, some form for conditional compilation that is negotiated between Lake and Lean.