Any projects rewriting Lean4 C++ parts in Rust ?

Stream: general

[TongKe Xue]

Hi,

Are there any projects rewriting Lean4 C++ parts in Rust ? [I could not find any on Google].
I know about https://github.com/ammkrn/nanoda_lib
I'm asking about rewriting all the C++ parts in Rust.

To avoid derailing the conversation, let's please put all the "Why do a Rust rewrite" debates into a different thread, and keep the thread focused on "Links (if any) to attempts doing this" / projects advancing this direction beyond nanoda_lib.

Thanks!

[Henrik Böving]

No, the point of nanoda is also not to rewrite anything but to have a second implementation of the type theory at hand so we can test against multiple ones.

[TongKe Xue]

Let us consider two statements:
S1: The purpose of nanoda_lib is to rewrite Lean4 C++ in Rust.
S2: nanoda_lib is useful to efforts trying to rewrite Lean4 C++ in Rust.

I think you believe I am expressing S1. I actually meant to express S2. (In retrospect, I could have been clearer; but given the current feature state of nanoda_lib, I didn't think anyone would consider S1 as a possibility.)

[TongKe Xue]

There's actually this really interesting project: https://fishshell.com/blog/rustport/

where they rewrote the Fish shell from C++ to Rust, basically module by module (with exception of one big part).

With something like https://github.com/google/autocxx , I'm legit wondering if a similar technique can be applied to Lean4. The C++ parts seem to be around 22k loc (according to cloc).

The replacement would be to keep CMake, to gradually introduce .rs files module by module, (using autocxx to call into C++ for the yet un-rewritten parts) and to setup CMake to call rustc. The trickiest part would probably be to figure out the "correct order of modules to rewrite".

[Patrick Massot]

You asked “Are there any projects rewriting Lean4 C++ parts in Rust ?” and insisted you were interested only in that question. I think Henrik’s answer was a very clear no.

[TongKe Xue]

I don't think we are in disagreement.

I cited nanoda_lib as evidence I had done my research (finding all Rust projects remotely close to rewriting Lean4 C++ in Rust); it was not, in anyway, meant as a claim that "nanoda_lib = rewrite Lean4 C++ in Rust".