Subject: grafting breaks package idris2

From: Stefan Karrmann <[email-masked]>
Date: Sun, 4 May 2025 09:17:43 +0000

Dear all,

I'm working on the package idris2 [1]. ~guix install -L my-packages
--no-grafts idris2~ works and gives me a runnable idris2, c.f. irdis2
session below. If I do the same without --no-grafts, I get another
package. Moreover, during the build ~make check~ reports no error. But
if I run it, I get the error: 

    Exception in fasl-read: uncompressed size 45800616 for #vu8(240 41 16 132 198 40 ...) is smaller than expected size 45800676

[1] https://github.com/idris-lang/Idris2

I suspect that a grafted package provides some data which is slighlty
(60 bytes) smaller than in the original package.

How can I write a package definition which either avoids beeing
grafted at all or avoids a specific graft for a specific package?

Why does this fresh build needs any grafts in the first place?
Since we build it anew, it could use all packages in their newest
grafted version. Then we do not need to graft it in the end.

Well, maybe I can answer the last question by myself:
1. I specified the ungrafted version of a package. Therefore,
   ~guix build~ uses it.
2. Using the normally named package version, i.e. glibc instead of
   glibc/fixed, is more robust against future updates of
   guix. I.e. glibc/fixed may vanish if glibc needs no graft.
3. Using the normally named package version, is the base for future
   grafts. I.e. if we have idris2 for non-grafted needed packages, we
   can graft it to future grafts more easily.
   Well replacing one graft by another is just replacing one hash by
   another. Of course, we need to get the correct hash codes.
   I.e. we have to remember the original package version, its used
   grafted version. Based on this, we could take the newest graft of
   the original package version as the new target graft.

NB: I solved [2] with my package definition. I.e. I sucessfully
replaced /bin/sh everywhere where needed with a store sh.

[2] https://www.reddit.com/r/GUIX/comments/uy57xc/how_to_deal_with_unpatchable_shebang/

Kind regards,
S. Karrmann

** idris2 session
 idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> 1 + 2
3
Main> :exit
Bye for now!

** channels
I provide my channels, such that we can call
~guix pull -C channels.scm~ to work with the same guix.
#+begin_src scheme
  (list (channel
        (name 'nonguix) ; sorry gnu, but this laptop needs some non-free drivers
        (url "https://gitlab.com/nonguix/nonguix")
        (branch "master")
        (commit
          "e899121adbaa13cfcaeae7a5c24921bffa645771")
        (introduction
          (make-channel-introduction
            "897c1a470da759236cc11798f4e0a5f7d4d59fbc"
            (openpgp-fingerprint
              "2A39 3FFF 68F4 EF7A 3D29  12AF 6F51 20A0 22FB B2D5"))))
      (channel
        (name 'guix)
        (url "https://git.savannah.gnu.org/git/guix.git")
        (branch "master")
        (commit
          "7ff20b9e94c429f1160bd8f0db86b153a03e4683")
        (introduction
          (make-channel-introduction
            "9edb3f66fd807b096b48283debdcddccfea34bad"
            (openpgp-fingerprint
              "BBB0 2DDF 2CEA F6A8 0D1D  E643 A2A0 6DF2 A33A 54FA")))))
#+end_src

** idris2 package definition
#+begin_src scheme
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2025 Dr. Stefan Karrmann <[email-masked]>
;;; Licence: AGPL-2

;; (define-module (gnu packages idris2)
(define-module (skix packages idris2)) ; local additions 
(use-modules
 ((guix licenses) #:prefix license:)
 (gnu packages)
 (gnu)
 (guix build utils)
 (guix build-system gnu)
 (guix download)
 (guix gexp)
 (guix git-download)
 (guix packages)
 (guix utils)
 (srfi srfi-1)
 )

(use-package-modules
 bash
 chez
 commencement
 gawk
 gcc
 multiprecision
 python
 )

(define-public idris2-bootstrap
  (package
    (name "idris2-bootstrap")
    (version "0.7.0")
    (source
     (origin
       (method git-fetch)
       (uri (git-reference
             (url "https://github.com/idris-lang/Idris2")
             (commit (string-append "v" version))))
       (file-name (git-file-name name version))
       (sha256
        (base32
         "0qxfwsm2gxjxwzni85jb5b4snvjf77knqs9bnd2bqznrfxgxw2sp"))))
    (build-system gnu-build-system)
    (native-inputs                      ;For tests
     (list
      gawk python))
    (inputs
     (list
      chez-scheme
      gcc-toolchain
      coreutils
      gmp))
    (arguments
     (list
      #:tests? #f
      #:phases
      #~(modify-phases
            %standard-phases
          (add-before
              'configure 'config.mk
            (lambda* (#:key outputs #:allow-other-keys)
              (peek 'idris-boot outputs)
              (let* ((out (assoc-ref outputs "out"))
                     (sh (string-append #$bash "/bin/sh"))
                     (bin-sh (string-append "#!" sh))
                     )
                (for-each
                 (lambda (file)
                   (peek 'forall-file-subst file #$bash)
                   (substitute*
                       file
                     (("#!/bin/sh")
                      bin-sh)))
                 (append
                  (find-files "bootstrap/idris2_app" "idris2\\..*")
                  (find-files "src/Compiler/Scheme" "\\.idr$")))
                (substitute*
                    "support/c/idris_file.c"
                  (("/bin/sh") sh))
                (substitute*
                    "config.mk"
                  (("PREFIX.*=.*")
                   ;;(string-append "PREFIX=" out)
                   (string-append
                    "PREFIX=" #$output "\n"
                    "CC=" #$gcc "/bin/gcc" "\n"
                    "IDRIS2_BOOT=${CURDIR}/build/exec/idris2")
                   ))
                )))
          (delete 'configure)
          (replace
              'build
            (lambda _
              (invoke "make" "distclean")
              (invoke "make" "bootstrap" "SCHEME=chez-scheme")
              )
            )
          )))
    (native-search-paths
     (list (search-path-specification
            (variable "IDRIS_LIBRARY_PATH")
            (files '("lib/idris")))))
    (home-page "https://www.idris-lang.org")
    (synopsis "General purpose language with full dependent types")
    (description "Idris2 is a general purpose language with full dependent
types.  It is compiled, with eager evaluation.  Dependent types allow types to
be predicated on values, meaning that some aspects of a program's behaviour
can be specified precisely in the type.  The language is closely related to
Epigram and Agda.")
    (license license:bsd-3)))

(define-public idris2
  (package
   (name "idris2")
   (version "0.7.0")
   (source (origin
            (method git-fetch)
            (uri (git-reference
                  (url "https://github.com/idris-lang/Idris2")
                  (commit (string-append "v" version))))
            (file-name (git-file-name name version))
            (sha256
             (base32
              "0qxfwsm2gxjxwzni85jb5b4snvjf77knqs9bnd2bqznrfxgxw2sp"))
            #;(patches (search-patches "idris-test-ffi008.patch"))))
   (build-system gnu-build-system)
   (native-inputs                       ;For tests
    (list
     gawk
     python
     idris2-bootstrap))
   (inputs
   (list
     chez-scheme
     gcc-toolchain
     gcc
     coreutils
     gmp))
   (arguments
    (list
     #:test-target "test"
     #:phases
     #~(modify-phases
        %standard-phases
        (add-before
         'configure 'config.mk
         (lambda* (#:key outputs #:allow-other-keys)
           (invoke "make" "distclean")
           (peek 'idris2-ouputs outputs)
           (let* ((out (assoc-ref outputs "out"))
                  (sh (string-append #$bash "/bin/sh"))
                  (bin-sh (string-append "#!" sh))
                  )
             (for-each
              (lambda (file)
                (peek 'forall-file-subst file #$bash)
                (substitute*
                    file
                  (("#!/bin/sh")
                   bin-sh)))
              (append
               (find-files "bootstrap/idris2_app" "idris2\\..*")
               (find-files "src/Compiler/Scheme" "\\.idr$")))
             (substitute*
                 "support/c/idris_file.c"
               (("/bin/sh") sh))
             (substitute*
                 "config.mk"
               (("PREFIX.*=.*")
                ;;(string-append "PREFIX=" out)
                (string-append
                 "PREFIX=" #$output "\n"
                 "CC=" #$gcc "/bin/gcc" "\n"
                 )
                ))
             )))
        (delete 'configure)
        (replace
         'install
         (lambda _
           (invoke "make" "install")
           (invoke "make" "install-libdocs")
           ))
        )))
   (native-search-paths
    (list (search-path-specification
           (variable "IDRIS_LIBRARY_PATH")
           (files '("lib/idris")))))
   (home-page "https://www.idris-lang.org")
   (synopsis "General purpose language with full dependent types")
   (description "Idris2 is a general purpose language with full dependent
types.  It is compiled, with eager evaluation.  Dependent types allow types to
be predicated on values, meaning that some aspects of a program's behaviour
can be specified precisely in the type.  The language is closely related to
Epigram and Agda.")
   (license license:bsd-3)))
  
#+end_src