interval tree

Stream: batteries

[Paige Thomas]

Is there by any chance an existing implementation of an interval tree that someone has done? I have an open source project for work where I need to create a local in memory time series cache library that I am considering this for. If not, I'm currently writing algorithms on top of Batteries.RBSet. I need to end up with code in C or Rust, but maybe I can translate it over to Rust when I am done. (I'm not sure I understand the API for interfacing to C, or if it is stable enough?)

[Henrik Böving]

Multiple things:

1. I don't think anyone has implemented an interval tree but I think it's certainly a simple enough structure such that it could be done soon.
2. Am I understanding correctly that you are using Lean for a work project that needs to interface with other code?
3. The C API has not significantly changed since I started doing Lean a couple of years ago, I'd say it's pretty stable.

[Paige Thomas]

2. It is for a work project, but I think all or most of our code is open source. This will be a library that will be used by code written in Rust.

[Paige Thomas]

Code that needs a time series cache.

[Paige Thomas]

Part of the approach is to assume that all of the intervals in the tree are disjoint, so that should make it simpler.

[Paige Thomas]

But that means that inserts will have to maintain the disjointness property.

[Paige Thomas]

I'm starting with sorting the intervals in the RBSet by the starting time, and then writing algorithms to traverse the underlying tree to do the various operations.

[Paige Thomas]

For the C API I have found
https://lean-lang.org/lean4/doc/dev/ffi.html
and
https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi
Is there more out there?

[Henrik Böving]

https://github.com/tydeu/lean4-alloy is pretty nice

[Paige Thomas]

"Alloy is a Lean 4 library that allows one to embed external FFI code (currently just C) directly within Lean"
If I understand correctly, I think I want to go the other way around.

[Henrik Böving]

You can also write normal C code in Lean with it and don't have to care about all of the linking and compilation setup when interacting with the lean part of your code

[Paige Thomas]

I see. Unfortunately I don't think they will be willing to take that approach. I also forgot that it will need to be called from Python, so I need to make a Python binding to the C code.

[James Gallicchio]

not sure if this helps, but i'm currently working on a CapnProto implementation for Lean, which would allow for some more complex typesafe interfaces between Lean and Rust/Python

[Paige Thomas]

That is interesting. How would that work? Would the Lean code be in a separate running process that handles RPC calls?

[Paige Thomas]

I see this, but I don't know enough about FFI to understand it in this context

Inter-language communication: Calling C++ code from, say, Java or Python tends to be painful or slow. With Cap’n Proto, the two languages can easily operate on the same in-memory data structure.

[James Gallicchio]

Yeah; I think if you could get Lean and Rust code linked together, you could just pass the buffer with the capnproto message to a Lean FFI endpoint (maybe using lean-sys to properly construct a ByteArray object for the Lean runtime) and have it operate directly on there.

[James Gallicchio]

but that's a lot of engineering effort if you're just looking for an interval tree implementation!

[Paige Thomas]

Yeah, that might be more than I have time to figure out. Thank you though.