Re: Packaging Idris2

["Philip McGrath" <philip@philipmcgrath.com>]

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