NetBSD package for lean4 (with patches)

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

I've packaged lean4 4.32.1 for pkgsrc. The resulting lean and lake binaries work on (at least) NetBSD 11.99.7/x86_64.

There were a couple issues:

• the build system didn't know how to handle NetBSD (solution: mostly like Linux)
• one file didn't compile (solution: add minimal platform-specific code)
• rpath issues in the resulting output files (solution: for now, worked around in pkgsrc)

Context

lean4 already nearly compiles on NetBSD. I'll submit a pullup request with the fixes for that shortly.

There is one remaining problem: On NetBSD, there is no /etc/ld.so.conf file like on Linux - instead, the ELF rpath mechanics are used to tell each binary where to look for the libraries it needs (i.e., add something like "-Wl,-R/usr/pkg/lib -Wl,-R/usr/pkg/lib/lean' when linking). This is easy to fix for the build of lean etc. themselves, but then the resulting leanc didn't add rpaths either, leading to non-working executables that didn't find the system GMP library. I don't have a clean mergable solution for that yet, but would like to get the other changes merged for now, and if you have a suggestion on how to add this in an acceptable way, please let me know.

Steps to Reproduce

Try building on NetBSD.

Versions

lean 4.32.1
NetBSD 11.99.7

Additional Information

n/a

Impact

Start by reproducing the Lean 4.32.1 build on NetBSD 11.99.7 and inspect the build-system handling for NetBSD, the platform-specific compilation failure, and the linker settings for generated leanc output. The existing package patches describe the first fixes; done means Lean and lake build successfully and generated executables locate the required GMP library through correct ELF rpaths.