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

Previous Next

Full log

Message #14 received at 72755 <at> debbugs.gnu.org (full text, mbox):

From: Divya Ranjan <divya <at> subvertising.org>
To: Antero Mejr <mail <at> antr.me>
Cc: 72755 <at> debbugs.gnu.org
Subject: Re: [bug#72755] [WIP][PATCH] guix: Add lean-build-system.
Date: Sat, 07 Dec 2024 22:13:45 +0000

Antero Mejr <mail <at> antr.me> writes:

> Divya Ranjan <divya <at> 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.