Packaging Idris2

Packaging Idris2

[Pierre-Henry Fröhring]

[-- Attachment #1: Type: text/plain, Size: 3396 bytes --]

Hello,

I'm trying to package Idris2.
The package so for looks like this:
In a working file `local-idris2.scm' there is:

----

(define-module (local-idris2))

(use-modules
 (gnu)
 (guix gexp)
 (guix utils)
 (guix packages)
 (guix git-download)
 (guix build-system gnu)
 (guix build utils)
 ((guix licenses) #:select (bsd-3)))

(use-package-modules
 gcc
 multiprecision
 bash
 base
 python
 chez)

(define-public idris2
  (package
    (name "idris2")
    (version "0.5.1")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/idris-lang/Idris2")
                    (commit (string-append "v" version))))
              (sha256
               (base32
                "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978"))
              (file-name (git-file-name name version))))
    (build-system gnu-build-system)
    (arguments
     `(#:make-flags
       `("bootstrap"
         "SCHEME=chez-scheme"
         ,(string-append "CC=" ,(cc-for-target))
         ,(string-append "PREFIX=" (assoc-ref %outputs "out")))
       #:phases (modify-phases %standard-phases
                  (delete 'configure))
       #:parallel-build? #f))
    (inputs (list gcc-12 chez-scheme gmp coreutils bash python))
    (home-page "https://www.idris-lang.org/")
    (synopsis "Programming language designed to encourage Type-Driven Development")
    (description
     "Idris is a programming language designed to encourage Type-Driven Development.

In type-driven development, types are tools for constructing programs. We
treat the type as the plan for a program, and use the compiler and type
checker as our assistant, guiding us to a complete program that satisfies the
type. The more expressive the type is that we give up front, the more
confidence we can have that the resulting program will be correct.")
    (license bsd-3)))

----

But if fails with the following:

----
...
make -C libs/prelude IDRIS2=/tmp/guix-build-idris2-0.5.1.drv-0/source/build/exec/idris2
IDRIS2_INC_CGS=chez IDRIS2_PATH="/tmp/guix-build-idris2-0.5.1.drv-
0/source/libs/prelude/build/ttc:/tmp/guix-build-idris2-0.5.1.drv-
0/source/libs/base/build/ttc:/tmp/guix-build-idris2-0.5.1.drv-
0/source/libs/contrib/build/ttc:/tmp/guix-build-idris2-0.5.1.drv-
0/source/libs/network/build/ttc:/tmp/guix-build-idris2-0.5.1.drv-
0/source/libs/test/build/ttc"
make[2]: Entering directory '/tmp/guix-build-idris2-0.5.1.drv-0/source/libs/prelude'
/tmp/guix-build-idris2-0.5.1.drv-0/source/build/exec/idris2 --build prelude.ipkg
make[2]: /tmp/guix-build-idris2-0.5.1.drv-0/source/build/exec/idris2: No such file or
directory
make[2]: *** [Makefile:2: all] Error 127
make[2]: Leaving directory '/tmp/guix-build-idris2-0.5.1.drv-0/source/libs/prelude'
make[1]: *** [Makefile:76: prelude] Error 2
make[1]: Leaving directory '/tmp/guix-build-idris2-0.5.1.drv-0/source'
make: *** [Makefile:233: bootstrap] Error 2
error: in phase 'build': uncaught exception:
%exception #<&invoke-error program: "make" arguments: ("bootstrap" "SCHEME=chez-scheme"
"CC=gcc" "PREFIX=/gnu/store/nrknvng9561kap38rpvd9j3y93b4nadd-idris2-0.5.1") exit-status: 2
term-signal: #f stop-signal: #f> 
phase `build' failed after 257.9 seconds
---- 

I tried `guix build -K idris2' and executing `make bootstrap ...' in the `/tmp/...' dir
and it works no problem.

How to make that work?

Thank you,
PHF


[-- Attachment #2: awwjk3xxccddskhhrz6mmx9wa649fb-idris2-0.5.1.drv.gz --]
[-- Type: application/gzip, Size: 39489 bytes --]

Re: Packaging Idris2

[(]

Hi Pierre-Henry,

On Fri Aug 19, 2022 at 4:42 PM BST, Pierre-Henry Fröhring wrote:
> The package so for looks like this:

I'm afraid I can't answer your specific question, but I do know that
Idris2 contains pregenerated Scheme code; you'll want to figure out
how to build it from Idris1, which is already packaged in Guix.

    -- (

Re: Packaging Idris2

[Pierre-Henry Fröhring]

Well, I went from a `guix shell --container' up to `make test' passing ;
assuming a `chez-scheme' backend (no `node' nor `racket'). It boils down
to a shell session looking like:

┌────
│ $ cd ~/src/
│ $ git clone git@github.com:idris-lang/Idris2.git
│ $ cd Idris2
│ $ ./build_idris
└────
Listing 1: session

I guess that an idea would be to « translate » this session into a Guix
Package. What's the best option here? To torture the `gnu-build-system'
until it accepts to build Idris2 or should I take the
`trivial-build-system' route?
Thank you.
― PHF

┌────
│ #! /usr/bin/env bash
│ set -euo pipefail
│ IFS=$'\n\t'
│ 
│ cat <<'EOF' >manifest.scm
│ (specifications->manifest
│  '("gcc@12.1.0"
│    "chez-scheme"
│    "gmp"
│    "coreutils"
│    "bash"
│    "make"
│    "findutils"
│    "git"
│    "diffutils"
│    "glibc"
│    "sed"
│    "gawk"
│    "binutils"))
│ EOF
│ 
│ cat <<'EOF' >build_idris_in_container
│ set -euo pipefail
│ IFS=$'\n\t'
│ 
│ echo 'Idris build configuration'
│ set -x
│ export PREFIX=/tmp/idris2
│ export SCHEME=chez-scheme
│ export CC=gcc
│ export INTERACTIVE=''
│ set +x
│ echo
│ 
│ echo 'PATHS configuration'
│ set -x
│ export LD_LIBRARY_PATH=$GUIX_ENVIRONMENT/lib:$PREFIX/lib
│ export PATH=$PATH:$PREFIX/bin
│ set +x
│ echo
│ 
│ echo 'Bootstrap'
│ make bootstrap
│ echo
│ 
│ echo 'Install'
│ make install
│ echo
│ 
│ echo 'Self-host'
│ make clean
│ make all
│ make install
│ echo
│ 
│ echo 'Test'
│ make test
│ echo
│ 
│ echo 'Clean'
│ rm -v manifest.scm
│ rm -v build_idris_in_container
│ echo
│ EOF
│ 
│ guix shell -C -m manifest.scm -- bash ./build_idris_in_container
└────
Listing 2: build_idris

Re: Packaging Idris2

[Csepp]

Pierre-Henry Fröhring <contact@phfrohring.com> writes:

> Well, I went from a `guix shell --container' up to `make test' passing ;
> assuming a `chez-scheme' backend (no `node' nor `racket'). It boils down
> to a shell session looking like:
>
> ┌────
> │ $ cd ~/src/
> │ $ git clone git@github.com:idris-lang/Idris2.git
> │ $ cd Idris2
> │ $ ./build_idris
> └────
> Listing 1: session
>
> I guess that an idea would be to « translate » this session into a Guix
> Package. What's the best option here? To torture the `gnu-build-system'
> until it accepts to build Idris2 or should I take the
> `trivial-build-system' route?
> Thank you.
> ― PHF
>
> ┌────
> │ #! /usr/bin/env bash
> │ set -euo pipefail
> │ IFS=$'\n\t'
> │ 
> │ cat <<'EOF' >manifest.scm
> │ (specifications->manifest
> │  '("gcc@12.1.0"
> │    "chez-scheme"
> │    "gmp"
> │    "coreutils"
> │    "bash"
> │    "make"
> │    "findutils"
> │    "git"
> │    "diffutils"
> │    "glibc"
> │    "sed"
> │    "gawk"
> │    "binutils"))
> │ EOF
> │ 
> │ cat <<'EOF' >build_idris_in_container
> │ set -euo pipefail
> │ IFS=$'\n\t'
> │ 
> │ echo 'Idris build configuration'
> │ set -x
> │ export PREFIX=/tmp/idris2
> │ export SCHEME=chez-scheme
> │ export CC=gcc
> │ export INTERACTIVE=''
> │ set +x
> │ echo
> │ 
> │ echo 'PATHS configuration'
> │ set -x
> │ export LD_LIBRARY_PATH=$GUIX_ENVIRONMENT/lib:$PREFIX/lib
> │ export PATH=$PATH:$PREFIX/bin
> │ set +x
> │ echo
> │ 
> │ echo 'Bootstrap'
> │ make bootstrap
> │ echo
> │ 
> │ echo 'Install'
> │ make install
> │ echo
> │ 
> │ echo 'Self-host'
> │ make clean
> │ make all
> │ make install
> │ echo
> │ 
> │ echo 'Test'
> │ make test
> │ echo
> │ 
> │ echo 'Clean'
> │ rm -v manifest.scm
> │ rm -v build_idris_in_container
> │ echo
> │ EOF
> │ 
> │ guix shell -C -m manifest.scm -- bash ./build_idris_in_container
> └────
> Listing 2: build_idris

I'm pretty sure Lendvai Attila has a WIP package that was supposed to be
submitted as a patch "soon", which was like a year ago.

Anyways, there are definitely already Idris 2 patches floating around
the mailing list so I'd prefer if discussion was moved there.
I'm also interested in getting it packaged, but building it takes a lot
of time.
The Scheme bootstrap seed can be generated with Idris 1, true.  But
compiling Idris 2 with Idris 1 takes such an ungodly amount of time and
RAM that expecting people to do so is maybe not a great idea.  I
certainly will not be working on that.  Last time I built it I needed at
least 16 gigs of swap.  I have better use cases for my SSD.

Re: Packaging Idris2

[Andreas Reuleaux]

Csepp <raingloom@riseup.net> writes:

> Pierre-Henry Fröhring <contact@phfrohring.com> writes:
>
>> Well, I went from a `guix shell --container' up to `make test' passing ;
>> assuming a `chez-scheme' backend (no `node' nor `racket'). It boils down
>> to a shell session looking like:
>>
>> ┌────
>> │ $ cd ~/src/
>> │ $ git clone git@github.com:idris-lang/Idris2.git
>> │ $ cd Idris2
>> │ $ ./build_idris
>> └────
>> Listing 1: session
>>
>> I guess that an idea would be to « translate » this session into a Guix
>> Package. What's the best option here? To torture the `gnu-build-system'
>> until it accepts to build Idris2 or should I take the
>> `trivial-build-system' route?
>> Thank you.
>> ― PHF
>>
>> ┌────
>> │ #! /usr/bin/env bash
>> │ set -euo pipefail
>> │ IFS=$'\n\t'
>> │ 
>> │ cat <<'EOF' >manifest.scm
>> │ (specifications->manifest
>> │  '("gcc@12.1.0"
>> │    "chez-scheme"
>> │    "gmp"
>> │    "coreutils"
>> │    "bash"
>> │    "make"
>> │    "findutils"
>> │    "git"
>> │    "diffutils"
>> │    "glibc"
>> │    "sed"
>> │    "gawk"
>> │    "binutils"))
>> │ EOF
>> │ 
>> │ cat <<'EOF' >build_idris_in_container
>> │ set -euo pipefail
>> │ IFS=$'\n\t'
>> │ 
>> │ echo 'Idris build configuration'
>> │ set -x
>> │ export PREFIX=/tmp/idris2
>> │ export SCHEME=chez-scheme
>> │ export CC=gcc
>> │ export INTERACTIVE=''
>> │ set +x
>> │ echo
>> │ 
>> │ echo 'PATHS configuration'
>> │ set -x
>> │ export LD_LIBRARY_PATH=$GUIX_ENVIRONMENT/lib:$PREFIX/lib
>> │ export PATH=$PATH:$PREFIX/bin
>> │ set +x
>> │ echo
>> │ 
>> │ echo 'Bootstrap'
>> │ make bootstrap
>> │ echo
>> │ 
>> │ echo 'Install'
>> │ make install
>> │ echo
>> │ 
>> │ echo 'Self-host'
>> │ make clean
>> │ make all
>> │ make install
>> │ echo
>> │ 
>> │ echo 'Test'
>> │ make test
>> │ echo
>> │ 
>> │ echo 'Clean'
>> │ rm -v manifest.scm
>> │ rm -v build_idris_in_container
>> │ echo
>> │ EOF
>> │ 
>> │ guix shell -C -m manifest.scm -- bash ./build_idris_in_container
>> └────
>> Listing 2: build_idris
>




> I'm pretty sure Lendvai Attila has a WIP package that was supposed to be
> submitted as a patch "soon", which was like a year ago.
>
> Anyways, there are definitely already Idris 2 patches floating around
> the mailing list so I'd prefer if discussion was moved there.
> I'm also interested in getting it packaged, but building it takes a lot
> of time.


Sorry for intercepting: It does *NOT* take that much time:

Just following the INSTALL instruction as in the package
idris2-0.5.1.tgz (unpacked as  Idris2-0.5.1 )
takes me 8 min + 25 sec roughly

(bootstrapping with racket in my case / chez scheme would do as well)


time make bootstrap-racket


real    8m20.490s
user    8m13.197s
sys     0m6.841s



time make install

real    0m4.796s
user    0m4.267s
sys     0m0.532s




> The Scheme bootstrap seed can be generated with Idris 1, true.  But
> compiling Idris 2 with Idris 1 takes such an ungodly amount of time and
> RAM that expecting people to do so is maybe not a great idea.  I
> certainly will not be working on that.  Last time I built it I needed at
> least 16 gigs of swap.  I have better use cases for my SSD.



Sorry this is wrong: Idris2 is *NOT* built from Idris1 any more:

You either build from an existing Idris2 (that means you had it successfully built/installed
at least once - and are by now experienced enough, to know what's going on in your
build chain), or - probably more relevant for the packaging here:

  You bootstrap it from scheme (chez or racket), as comes within the Idris2 tarball
  (and built with Idris 2 itself: Idris2 -> Chez Scheme / Racket).


I am not that super familiar with Guix packaging (well have done some little bits before),
but at least I got Idris 2 installed and running (well I guess you have, too [?]).

But I may be able to step in with more detailed installation steps, if needed.

Thanks,
 -A

Re: Packaging Idris2

[(]

Hi Andreas,

On Sat Aug 20, 2022 at 11:01 PM BST, Andreas Reuleaux wrote:
>   You bootstrap it from scheme (chez or racket), as comes within the Idris2 tarball
>   (and built with Idris 2 itself: Idris2 -> Chez Scheme / Racket).

Since this Scheme is pregenerated, it cannot really count as source code. So
we need to find a version of Idris2 that can still be built with Idris1, then
try to build a later version with that Idris2, and keep going until we get to
the latest version, like our rustc bootstrap process.

    -- (

Re: Packaging Idris2

[Csepp]

"(" <paren@disroot.org> writes:

> Hi Andreas,
>
> On Sat Aug 20, 2022 at 11:01 PM BST, Andreas Reuleaux wrote:
>>   You bootstrap it from scheme (chez or racket), as comes within the Idris2 tarball
>>   (and built with Idris 2 itself: Idris2 -> Chez Scheme / Racket).
>
> Since this Scheme is pregenerated, it cannot really count as source code. So
> we need to find a version of Idris2 that can still be built with Idris1, then
> try to build a later version with that Idris2, and keep going until we get to
> the latest version, like our rustc bootstrap process.
>
>     -- (

Yup.

And there are already patches and channels floating around that do that.
Anyways, if you want to work on Idris 2, I highly recommend looking at
them.  Otherwise you are doing work that has already been done.  Which
is fine if you are only doing this as an exercise, but if you are
serious about packaging Idris 2, you should know about the issues that
have come up with it.

ps.: pls no benchmarks without hardware info. :)
I know what I'm talking about when I say it takes too many resources on
my machine and I'm aware that more powerful computers exist and that Idris
2 compiles itself faster than Idris 1 does.

Re: Packaging Idris2

[Andreas Reuleaux]

"(" <paren@disroot.org> writes:

> Hi Andreas,
>
> On Sat Aug 20, 2022 at 11:01 PM BST, Andreas Reuleaux wrote:
>>   You bootstrap it from scheme (chez or racket), as comes within the Idris2 tarball
>>   (and built with Idris 2 itself: Idris2 -> Chez Scheme / Racket).
>
> Since this Scheme is pregenerated, it cannot really count as source code. So
> we need to find a version of Idris2 that can still be built with Idris1, then
> try to build a later version with that Idris2, and keep going until we get to
> the latest version, like our rustc bootstrap process.
>
>     -- (


OK, thanks for getting back to me, and I am learning...

Nevertheless: this sounds terribly complicated to me.

Why would I use a package manager then (the guix package manager i.e.) in the
first place, if I can install idris2 in just simple three steps:


step 1
download https://www.idris-lang.org/idris2-src/idris2-0.5.1.tgz
and unpack it.

step 2
adjust PREFIX in config.mk therein ($(HOME)/opt/idris2 in my case)
and set PATH, and LD_LIBRARY_PATH accordingly:

  export PATH=$PATH:$HOME/opt/idris2/bin
  export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$HOME/opt/idris2/lib

step 3
(assuming racket is installed - as in my case):

  make bootstrap-racket
  make install


And In particular: there is no Idris1 involved.

(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).

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!

But apparently: you are more experienced in these packaging matters
then me.

So thanks - in any case.

And by the way: my bench marks were on a 8 core
Intel(R) Core(TM) i7-7700 CPU @ 3.60GHz
running Debian testing)


-A

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>.

    -- (

Re: Packaging Idris2

[(]

On Sun Aug 21, 2022 at 11:39 AM BST, ( 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, 

Oops, left off the end of this sentence -- it should be:

> and Nim) but here, where it does seem to be possible, we should make
> every effort to avoid pregenerated files.

    -- (

Re: Packaging Idris2

[zimoun]

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, 

a) Chicken is not bootstrapped.  See [1,2].

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.

c) For the previous work, see patch#49607 [3].


1: <http://issues.guix.gnu.org/issue/22366>
2: <http://bugs.call-cc.org/ticket/1776>
3: <http://issues.guix.gnu.org/issue/49607>


Cheers,
simon

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

Re: Packaging Idris2

[contact]

Dear Guixers,

I've a working package of `idris2' here: 
<https://paste.debian.net/1251410/>.
It builds on previous work: <https://issues.guix.gnu.org/issue/49607>.
Would it help to send it to `guix-patches@gnu.org'?

—PHF

Re: Packaging Idris2

[Csepp]

contact@phfrohring.com writes:

> Dear Guixers,
>
> I've a working package of `idris2' here:
> <https://paste.debian.net/1251410/>.
> It builds on previous work: <https://issues.guix.gnu.org/issue/49607>.
> Would it help to send it to `guix-patches@gnu.org'?
>
> —PHF

Looks very good IMHO, please do send it.

If the bootstrapping thing is a problem we can always do that later, it
should be as easy as "unvendoring" the scripts.  If I remember
correctly, the precise version they were generated from is documented
and saved somewhere on the project's or Edwin Brady's Github.

Re: Packaging Idris2

[contact]

> Looks very good IMHO, please do send it.

I am not sure if I have sent it correctly.
I have sent the patch to: <mailto:49607@debbugs.gnu.org>.
It resulted in this message: 
<https://issues.guix.gnu.org/issue/49607#16>.

— PHF