[bug#72755] [WIP][PATCH] guix: Add lean-build-system.

[Divya Ranjan]

Antero Mejr <mail@antr.me> writes:

> Divya Ranjan <divya@subvertising.org> writes:
>> I’ve also been involved in packaging Lean4, have you had any more progress on
>> this? I tried to build guix from your patch, but `./pre-inst-env guix build
>> lean` gets stuck at some point after trying to compile things for ~7 hours. I
>> believe it gets stuck at compiling gash. Any clue?
>
> You shouldn't have to rebuild the entire dependency chain (and things
> like gash) to use the above patch - maybe someone on IRC or a maintainer
> can help with fixing that?

Okay, I’ll ask them about it.

> The above patches should work for building Lean4, but packaging any Lean
> library with dependencies (like mathlib) won't work until the lean
> developers resolve this issue:
> https://github.com/leanprover/lean4/issues/5122
>
> Unfortunately the devs marked it as low priority and seem to be pushing
> back against reproducible packaging, which is disappointing. I am
> unlikely to continue work on this patch series, as I have switched over
> to Coq.

Indeed, I saw that. Is there any way around it? How is Nix packaging mathlib 
et.al?

Regards,

Divya Ranjan