Re: Packaging Idris2

[Philip McGrath]

Hi,

On Sun, Aug 21, 2022, at 8:31 AM, zimoun wrote:
> Hi,
>
> Some quick comments. :-)
>
> On Sun, 21 Aug 2022 at 11:39, "(" <paren@disroot.org> wrote:
>
>> 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, 
>
> [...]
>
> b) «it does seem to be possible» but it had not been done since 1.5
> years.  Maybe it would be better to have something now instead than
> never; then it would be still possible to improve the situation.  IMHO.
>

I strongly agree with this.

The emphasis Guix places on bootstrapping and the incredible work the community 
has put into finding or creating bootstrapping tools are extremely valuable. 
Even so, I think it would be counterproductive for Guix to make a barrier to 
entry out of bootstrapping things that no one actually knows how to bootstrap. 
I think that applies also in this case, where it seems like there's a possible 
path to bootstrapping, but it isn't working yet despite reasonable effort: 
indeed, more than reasonable effort. (I can only imagine the frustration of 
having patches in limbo for 1.5 years.)

I've seen this come up with other compilers (e.g. 
https://lists.gnu.org/archive/html/help-guix/2021-11/msg00037.html), so maybe 
it's worth specifying and documenting Guix's policy.

In particular, because this issue primarily affects compilers (there are also 
related issues with e.g. build tools), there is a vicious cycle: if some 
language is not supported in Guix, people who specialize in that language 
probably won't use Guix, and those are precisely the people whose expertise 
might help improve the bootstrap situation.

AIUI, many of the impressive bootstrapping stories in Guix have come about this 
way, with incremental improvement over time.

I think it's better for Guix to package Idris2 in the best way we actually know 
how to do today than to leave the whole Idris2 universe bereft of all of the 
benefits of Guix.

Another factor that weighs in favor of accepting Idris2 for me is that the 
upstream community has mitigated at least some of the worst problems of 
bootstrapping. While the generated Racket or Scheme code is not especially 
readable, neither is it an opaque binary blob, and it is not "minified" or 
obfuscated: it would be quite hard to hide a "trusting trust" attack here. And 
of course there are many dimensions to reliability: I can understand why a 
community that's developed a language with the advanced correctness guarantees 
of Idris2 would want to take advantage of those guarantees in their compiler.

It's a bit of a tangent, but I also wanted to highlight the discrepancy between 
the bootstrapping limitation blocking Idris2 and the current state of some of 
its backends:

1) Upstream Chez Scheme (i.e. our 'chez-scheme', as opposed to 
'chez-scheme-for-racket') is not bootstrappable. It relies on pre-generated 
machine code "bootfiles" that can only be built by essentially the same version 
of Chez Scheme. The first release of Chez as free software in 2016 relied on 
bootfiles generated by its non-free ancestors dating back to 1985 (before 
GCC!). The only reasonable path to bootstrapping Chez is to adapt the 
bootstrapping code from the Racket variant (which simulates enough of Chez in 
Racket to slowly compile the Chez Scheme compiler): it may be as simple as 
finding a version in the Git history before Racket's Chez diverged too much 
from upstream, but I haven't found one yet, and it's not my top priority.

2) Compiled Chez Scheme code is not bit-for-bit reproducible due to the use of 
type 4 UUIDs for gensyms. (It is reproducible with respect to the Scheme 
function '#%$fasl-file-equal?'.) See 
https://github.com/cisco/ChezScheme/issues/585#issuecomment-955408143 for 
details and my thoughts on a possible solution.

3) Racket is mostly bootstrappable, but it relies on generated code (R6RS 
Scheme or primitive "linklets") for the expander (which implements the reader 
and module system in addition to macro expansion per se). See the comments at 
the top of '(gnu packages racket)' or https://racket.discourse.group/t/951/4 
for more discussion. I think it might be possible to write a bootstrap shim in 
Guile analogous to the way Racket bootstraps Chez. Sam Tobin-Hochstadt has 
suggested that it might be easier to adapt the C expander implementation from 
before Racket 7.0. (The C implementation was completely replaced with a Racket 
implementation based on the "sets of scopes" model from 
https://www.cs.utah.edu/plt/scope-sets/ rather than "marks" and "renamings".) 
Extreme care has been taken to make the generated code readable and editable, 
including indentation and preserving variable names: anecdotally, I have 
sometimes read even tens of lines of diff before realizing I was looking at the 
generated file rather than the source.

4) I'm less involved in Node.js, but there are some limitations there, too. Our 
'node' package bundles NPM and its dependencies, some of which include 
generated code (for Unicode, at least) or cyclic dependencies. One thing I 
think would help would be to avoid NPM in 'node-build-system' (somewhat like 
the antioxidant effort for Rust/Cargo) and instead implement some of the ideas 
from https://pnpm.io in Guile or another language with a good bootstrapping 
story.

For Idris2, I hope that puts the bootstrapping situation in perspective: Guix 
tries hard to avoid generated code, and we try to remove limitations over time, 
but the generated code in Idris2 is well within the bounds of what Guix has 
accepted in existing packages.

-Philip