diff mbox series

[bug#46124] Idris 2

Message ID 20210429204317.7e3a707c@riseup.net
State New
Headers show
Series [bug#46124] Idris 2 | expand

Checks

Context Check Description
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue

Commit Message

Csepp April 29, 2021, 6:43 p.m. UTC 
On Mon, 26 Apr 2021 23:27:39 +0200
Maxime Devos <maximedevos@telenet.be> wrote:

> raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> > There hasn't been a tagged release since then, so I'm sending my
> > original patch, but I should note that in my channel I've been
> > tracking the latest commit, which does seem to work, although it's
> > been a while since I used Idris for anything complicated.
> > 
> > +                     ;; TODO detect toolchain
> > +                     "CC=gcc")))  
> 
> Unless idris has a compiler built in that uses gcc for compiling
> idris to machine code, this should likely be
> ,(string-append "CC=" (cc-for-target)) instead, such that the
> cross-compiler is used when cross-compiling.
> 
> Teaching (cc-for-target) to detect which toolchain should be used
> is a separate matter.  Maybe it could be a macro that looks at
> (package-native-inputs this-package) or something.
> 
> Greetings,
> Maxime.

Oh, that's a leftover, I was using clang for a while, since it's
said to use less RAM. I switched back to gcc and left that in.

Here is the updated patch. No idea if this actually works cross
compiled, but I don't have much time to test it. My suspicion is that
it's likely broken and requires changes to Idris 2's code generators,
because they almost definitely call Chez, GCC, etc, with the wrong
arguments.

Comments

Xinglu Chen April 30, 2021, 8:24 a.m. UTC | #1 
On Thu, Apr 29 2021, raingloom wrote:

> Here is the updated patch. No idea if this actually works cross
> compiled, but I don't have much time to test it. My suspicion is that
> it's likely broken and requires changes to Idris 2's code generators,
> because they almost definitely call Chez, GCC, etc, with the wrong
> arguments.

I noticed that there is an ‘idris2_app’ directory in the ‘bin’ directory

  $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
  idris2*  idris2_app/

What is this used for?
M April 30, 2021, 8:50 a.m. UTC | #2 
raingloom schreef op do 29-04-2021 om 20:43 [+0200]:
> On Mon, 26 Apr 2021 23:27:39 +0200
> Maxime Devos <maximedevos@telenet.be> wrote:
> 
> > raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> > > [...]
> > > 
> > > +                     ;; TODO detect toolchain
> > > +                     "CC=gcc")))  
> > 
> > Unless idris has a compiler built in that uses gcc for compiling
> > idris to machine code, this should likely be
> > ,(string-append "CC=" (cc-for-target)) instead, such that the
> > cross-compiler is used when cross-compiling.
> > 
> > [...]
> Oh, that's a leftover, I was using clang for a while, since it's
> said to use less RAM. I switched back to gcc and left that in.
> 
> Here is the updated patch. No idea if this actually works cross
> compiled, but I don't have much time to test it.

IIUC, cross-compilation is not required to be supported by each
package in guix. It is something nice-to-have, but not strictly
required.

Greetings,
Maxime.
Csepp May 3, 2021, 2:10 a.m. UTC | #3 
On Fri, 30 Apr 2021 10:24:42 +0200
Xinglu Chen <public@yoctocell.xyz> wrote:

> On Thu, Apr 29 2021, raingloom wrote:
> 
> > Here is the updated patch. No idea if this actually works cross
> > compiled, but I don't have much time to test it. My suspicion is
> > that it's likely broken and requires changes to Idris 2's code
> > generators, because they almost definitely call Chez, GCC, etc,
> > with the wrong arguments.  
> 
> I noticed that there is an ‘idris2_app’ directory in the ‘bin’
> directory
> 
>   $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
>   idris2*  idris2_app/
> 
> What is this used for?
> 

If you take a look at $(guix build idris2)/bin/idris2, it's actually
just a wrapper. It contains the supporting dynamically linked shared
objects and the executable itself.

I don't know the details of what each file does or why it's like this,
the codegen seems to use a similar structure for all backends. The
scheme files are probably all for the Chez backend, the shared objects
are either C libraries (for socket support and stuff), or compiled Chez
code. I just noticed the Racket script, that I have no idea about.

Idris 2's build system makes some... uhm... interesting choices, so
it's entirely possible that not all of those are necessary, or could be
moved somewhere more sensible.
Xinglu Chen May 4, 2021, 5:12 p.m. UTC | #4 
On Mon, May 03 2021, raingloom wrote:

> On Fri, 30 Apr 2021 10:24:42 +0200
> Xinglu Chen <public@yoctocell.xyz> wrote:
>
>> On Thu, Apr 29 2021, raingloom wrote:
>> 
>> > Here is the updated patch. No idea if this actually works cross
>> > compiled, but I don't have much time to test it. My suspicion is
>> > that it's likely broken and requires changes to Idris 2's code
>> > generators, because they almost definitely call Chez, GCC, etc,
>> > with the wrong arguments.  
>> 
>> I noticed that there is an ‘idris2_app’ directory in the ‘bin’
>> directory
>> 
>>   $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
>>   idris2*  idris2_app/
>> 
>> What is this used for?
>
> If you take a look at $(guix build idris2)/bin/idris2, it's actually
> just a wrapper. It contains the supporting dynamically linked shared
> objects and the executable itself.
>
> I don't know the details of what each file does or why it's like this,
> the codegen seems to use a similar structure for all backends. The
> scheme files are probably all for the Chez backend, the shared objects
> are either C libraries (for socket support and stuff), or compiled Chez
> code. I just noticed the Racket script, that I have no idea about.
>
> Idris 2's build system makes some... uhm... interesting choices, so
> it's entirely possible that not all of those are necessary, or could be
> moved somewhere more sensible.

Looking at the Nix package, they remove the wrapper and instead move
bin/idris2_app/idris2.so to bin/idris2 and wraps that executable[1].
Perhaps we could do the same thing?  I am not familiar with Idris,
though.

[1]: https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2/default.nix#L41
Csepp May 11, 2021, 9:47 p.m. UTC | #5 
On Tue, 04 May 2021 19:12:18 +0200
Xinglu Chen <public@yoctocell.xyz> wrote:

> On Mon, May 03 2021, raingloom wrote:
> 
> > On Fri, 30 Apr 2021 10:24:42 +0200
> > Xinglu Chen <public@yoctocell.xyz> wrote:
> >  
> >> On Thu, Apr 29 2021, raingloom wrote:
> >>   
> >> > Here is the updated patch. No idea if this actually works cross
> >> > compiled, but I don't have much time to test it. My suspicion is
> >> > that it's likely broken and requires changes to Idris 2's code
> >> > generators, because they almost definitely call Chez, GCC, etc,
> >> > with the wrong arguments.    
> >> 
> >> I noticed that there is an ‘idris2_app’ directory in the ‘bin’
> >> directory
> >> 
> >>   $ ls /gnu/store/va62hzp46c3dp2vlcnqc7fg109axj8rq-idris2-0.3.0/bin
> >>   idris2*  idris2_app/
> >> 
> >> What is this used for?  
> >
> > If you take a look at $(guix build idris2)/bin/idris2, it's actually
> > just a wrapper. It contains the supporting dynamically linked shared
> > objects and the executable itself.
> >
> > I don't know the details of what each file does or why it's like
> > this, the codegen seems to use a similar structure for all
> > backends. The scheme files are probably all for the Chez backend,
> > the shared objects are either C libraries (for socket support and
> > stuff), or compiled Chez code. I just noticed the Racket script,
> > that I have no idea about.
> >
> > Idris 2's build system makes some... uhm... interesting choices, so
> > it's entirely possible that not all of those are necessary, or
> > could be moved somewhere more sensible.  
> 
> Looking at the Nix package, they remove the wrapper and instead move
> bin/idris2_app/idris2.so to bin/idris2 and wraps that executable[1].
> Perhaps we could do the same thing?  I am not familiar with Idris,
> though.
> 
> [1]:
> https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2/default.nix#L41

That link doesn't work.

I have some more pressing projects to work on, but I'll look into it.
Xinglu Chen May 14, 2021, 12:08 p.m. UTC | #6 
On Tue, May 11 2021, raingloom wrote:

>> 
>> [1]:
>> https://github.com/nixos/nixpkgs/blob//pkgs/development/compilers/idris2/default.nix#L41
>
> That link doesn't work.

Sorry, this one should work 

  https://github.com/NixOS/nixpkgs/blob/8284fc30c84ea47e63209d1a892aca1dfcd6bdf3/pkgs/development/compilers/idris2/default.nix#L35
diff mbox series

Patch

From e3c942454af34879393d073be755fa53390891bc Mon Sep 17 00:00:00 2001
From: raingloom <raingloom@riseup.net>
Date: Wed, 27 Jan 2021 06:21:01 +0100
Subject: [PATCH] gnu: Added Idris 2.

* gnu/packages/idris.scm (idris2): New variable.
---
 gnu/packages/idris.scm | 80 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 79 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..da66f7b0d8 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -21,6 +21,8 @@ 
 
 (define-module (gnu packages idris)
   #:use-module (gnu packages)
+  #:use-module (gnu packages bash)
+  #:use-module (gnu packages chez)
   #:use-module (gnu packages haskell-check)
   #:use-module (gnu packages haskell-web)
   #:use-module (gnu packages haskell-xyz)
@@ -28,12 +30,15 @@ 
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ncurses)
   #:use-module (gnu packages perl)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages sphinx)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system haskell)
   #:use-module (guix download)
   #:use-module (guix git-download)
   #:use-module ((guix licenses) #:prefix license:)
-  #:use-module (guix packages))
+  #:use-module (guix packages)
+  #:use-module (ice-9 regex))
 
 (define-public idris
   (package
@@ -150,6 +155,79 @@  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.3.0")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/idris-lang/Idris2")
+                    (commit (string-append "v" version))))
+              (sha256
+               (base32
+                "0sa2lpb7n6xqfknwld9rzm4bnb6qcd0ja1n63cnc5v8wdzr8q7kh"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:tests? #f ;; they are run as part of other targets
+       #:phases
+       (modify-phases
+           %standard-phases
+         (add-after 'unpack 'patch-paths
+           (lambda* (#:key outputs inputs #:allow-other-keys)
+             (substitute* "config.mk"
+               ((,(regexp-quote "PREFIX ?= $(HOME)/.idris2"))
+                (string-append "PREFIX = "
+                               (assoc-ref outputs "out"))))
+             (for-each
+              (lambda (f)
+                (substitute* f
+                  ((,(regexp-quote "#!/bin/sh"))
+                   (string-append "#!" (assoc-ref inputs "sh")
+                                  "/bin/sh"))))
+              (list "src/Compiler/Scheme/Chez.idr"
+                    "src/Compiler/Scheme/Racket.idr"
+                    "bootstrap/idris2_app/idris2.rkt"
+                    "bootstrap/idris2_app/idris2.ss"))))
+         ;; this is not the kind of bootstrap we want to run
+         (delete 'bootstrap)
+         (delete 'configure)
+         (replace 'build
+           (lambda _
+             (invoke "make" "bootstrap"
+                     "SCHEME=scheme"
+                     ;; TODO detect toolchain
+                     ,(string-append "CC=" (cc-for-target)))))
+         (add-after 'build 'build-doc
+           (lambda _
+             (with-directory-excursion
+                 "docs"
+               (invoke "make" "html"))))
+         (add-after 'install 'install-doc
+           (lambda* (#:key outputs #:allow-other-keys)
+             (copy-recursively
+              "docs/build/html"
+              (string-append
+               (assoc-ref outputs "out")
+               "/share/doc/"
+               ,name "-" ,version)))))))
+    (inputs
+     `(("sh" ,bash-minimal)
+       ("chez-scheme" ,chez-scheme)))
+    (native-inputs
+     `(("python-sphinx" ,python-sphinx)
+       ("python-sphinx-rtd-theme" ,python-sphinx-rtd-theme)
+       ("python" ,python)))
+    (home-page "https://idris-lang.org/")
+    (synopsis "A dependently typed programming language, a successor to Idris")
+    (description
+     "Idris 2 is a general purpose language with dependent linear 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.  It can use multiple languages as code
+generation backends.")
+    (license license:bsd-3)))
+
 ;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
 (define (idris-default-arguments name)
   `(#:modules ((guix build gnu-build-system)
-- 
2.31.1