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

From: Divya Ranjan <[email-masked]>
Date: Sat, 07 Dec 2024 22:13:45 +0000

Antero Mejr <[email-masked]> writes:

> Divya Ranjan <[email-masked]> 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