[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Packaging Idris2
From: |
Philip McGrath |
Subject: |
Re: Packaging Idris2 |
Date: |
Sun, 21 Aug 2022 19:40:20 -0400 |
User-agent: |
Cyrus-JMAP/3.7.0-alpha0-841-g7899e99a45-fm-20220811.002-g7899e99a |
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
- Re: Packaging Idris2, (continued)
- Re: Packaging Idris2, (, 2022/08/19
- Re: Packaging Idris2, Pierre-Henry Fröhring, 2022/08/20
- Re: Packaging Idris2, Csepp, 2022/08/20
- Re: Packaging Idris2, Andreas Reuleaux, 2022/08/20
- Re: Packaging Idris2, (, 2022/08/21
- Re: Packaging Idris2, Csepp, 2022/08/21
- Re: Packaging Idris2, Andreas Reuleaux, 2022/08/21
- Re: Packaging Idris2, (, 2022/08/21
- Re: Packaging Idris2, (, 2022/08/21
- Re: Packaging Idris2, zimoun, 2022/08/21
- Re: Packaging Idris2,
Philip McGrath <=
- Re: Packaging Idris2, contact, 2022/08/23
- Re: Packaging Idris2, Csepp, 2022/08/23
- Re: Packaging Idris2, contact, 2022/08/23