Re: Packaging Idris2

[(]

On Sun Aug 21, 2022 at 11:21 AM BST, Andreas Reuleaux wrote:
> (And by the way: the pregenerated scheme in there is not a binary,
> it is readable scheme code after all - well not terribly readable,
> but nevertheless).

Yes, that's true -- however, it's still not the complete, readable
source code. (It presumably doesn't have comments either, which greatly
aid understanding, of course.) We do make exceptions when bootstrapping
is simply impossible with currently existing tools (see Haskell, Pascal,
and Nim) but here, where it does seem to be possile, 

> What is won with the extra step of having an older Idris2 installed
> first, that still compiles with Idris 1 - And then do what with that:
> compile a newer Idris2 from that (that may still not be sufficiant
> to compile the latest Idris2), ... Reproducibility ? - Certainly
> not simplicity!

You can't trust pregenerated source, as it's usually far more difficult
to read (especially in the case where it's a binary), so Guix tries to
build everything from source as much as possible, even when the
generated files are textual. See <https://bootstrappable.org>.

    -- (