lean-sys update

Stream: lean4

[Jad Ghalayini]

Hello! After a lengthy disappearance caused by my PhD catching up with me, I've recently updated lean-sys to version 0.3.0 to track the latest changes to lean.h. The version bump from 0.2.0 is due to the breaking change of removing the fixpoint family of functions, as in Lean 4 commit f9f074d. Hopefully I'll have times to continue my project by publishing some higher-level bindings to Lean, with the end goal of seamless integration between Lean 4 and Rust code, as I'll need for my planned thesis. If anyone has any ideas/feature requests/found bugs/etc, I'd be happy to hear!

[Arthur Paulino]

Hello, is the Rust crate up to date with Lean v4.16.0?

Also, is there an example for how to use this crate?

[Mario Carneiro]

No, I think it hasn't been bumped since around 4.8.0

[Mario Carneiro]

I would really prefer if the FRO took over maintenance of it, no one ever pings me when lean.h changes so it's really difficult to keep it afloat without people using it and relying on it

[Kim Morrison]

I'm not at all sure how the crate works, but at least for Lean projects I would love if lean-action could produce reminders/automation in some form to bump to the next toolchain.

[Mario Carneiro]

lean-sys is basically a collection of rust bindings, the FFI partner to lean.h. It needs to be changed whenever anything in lean.h changes, usually to just write the rust version of the type signature, and possibly also the implementation if it's a static inline method

[Kim Morrison]

Mac would be the person to speak to about this, then.

But at your end, maybe you could add a CI step the periodically tries to build against the latest toolchain or nightly?

[Mario Carneiro]

I am not sure we have anything which would detect a mismatch

[Mario Carneiro]

it will build even if there are changes, it will just segfault if you use the bad functions

[Mario Carneiro]

the only thing I can think of is to just ping a human whenever the text of lean.h changes

[Mario Carneiro]

there do exist automatic tools for building the bindings (bindgen), but I think they don't work well enough to be usable in practice - in particular I think it won't know about the lean ownership encoding with borrowed and owned object pointers (which aren't actually pointers sometimes)

[Mario Carneiro]

so lean-sys is much closer to a manual port

[Arthur Paulino]

Thanks, we've taken a different approach. We're mimicking the memory layout of the Lean objects "manually". That's pretty much reimplementing lean.h in Rust. But we only need a subset of it.

As far as detecting changes in lean.h goes, I can provide an idea. Keep a lean-toolchain file in the project specifying the toolchain version lean-sys targets. And also keep a lean.h.hash file containing the hash of the lean.h file. Then, on CI, force that hash to match the hash of lean.h that gets downloaded (based on lean-toolchain). This is probably the way I'm gonna set it up on our end.

[Mario Carneiro]

I just pushed lean-sys v0.0.8, which is up to date with lean v4.16.0

[Arthur Paulino]

Sharing in case it's useful to someone in the future.
This check turns out to be much better as a Lake script (if your project is also a Lake project) because there's already getLeanIncludeDir:

script check_lean_h_hash := do
  let cachedLeanHHash ← IO.FS.readFile "lean.h.hash"

  let leanIncludeDir ← getLeanIncludeDir
  let includedLeanHPath := leanIncludeDir / "lean" / "lean.h"
  let includedLeanHBytes ← IO.FS.readBinFile includedLeanHPath
  let includedLeanHHash := toString includedLeanHBytes.hash

  if cachedLeanHHash ≠ includedLeanHHash then
    IO.eprintln   "Mismatching lean/lean.h hash"
    IO.eprintln   "  1. Double-check changes made to lean/lean.h"
    IO.eprintln s!"  2. Cache {includedLeanHHash} instead"
    return 1
  return 0

Then run check_lean_h_hash on CI