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

Previous Next

Full log

View this message in rfc822 format

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

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?

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.

Previous Next

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