Buidling "Hello World" in Idris

Help
1

I have a simple “Hello World” program.

$ cat helloIdris.idr
module Main

import Data.Vect

main : IO ()
main = putStrLn "Hello world"

$ cat helloIdris.ipkg
package helloIdris

modules = helloIdris

main = helloIdris
executable = helloIdris

I can build it directly using Idris.

$ idris --build helloIdris.ipkg
Type checking ./helloIdris.idr
$ ./helloIdris
Hello world

But now I’m trying to build it the Nix way, using this as a guide.

$ cat default.nix
with import <nixpkgs> {};

{
  helloIdris = idrisPackages.callPackage ./helloIdris.nix {};
}

$ cat helloIdris.nix
{ build-idris-package
, lib
}:
build-idris-package  {
  name = "helloIdris";
  version = "0.0.1";

  src = ./.;

  meta = {
    description = "Simple Idris program";
  };
}

I get a warning about an empty or non-existent namespace:

$ nix-build -A helloIdris
these derivations will be built:
  /nix/store/b3a9n28nkdkh3cn6yrz0m0bqv7a2djzs-idris-helloIdris-0.0.1.drv
building '/nix/store/b3a9n28nkdkh3cn6yrz0m0bqv7a2djzs-idris-helloIdris-0.0.1.drv'...
unpacking sources
unpacking source archive /nix/store/15936mdds4hgvn9bcfsmpfsvh3p3njfh-helloIdris
source root is helloIdris
patching sources
configuring
no configure script, doing nothing
building
Type checking ./helloIdris.idr
installing
Attempting to install IdrisDocs for helloIdris in: /nix/store/zbjnz39xh9j23s3ikh8cwp45gfd3hkf0-idris-helloIdris-0.0.1/doc/helloidris
Warning: Ignoring empty or non-existing namespace 'helloIdris'
No namespaces to generate documentation for
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/zbjnz39xh9j23s3ikh8cwp45gfd3hkf0-idris-helloIdris-0.0.1
strip is /nix/store/5vyv136pqs75pj0b8vcpdyc03dmn9p0n-binutils-2.30/bin/strip
patching script interpreter paths in /nix/store/zbjnz39xh9j23s3ikh8cwp45gfd3hkf0-idris-helloIdris-0.0.1
checking for references to /build in /nix/store/zbjnz39xh9j23s3ikh8cwp45gfd3hkf0-idris-helloIdris-0.0.1...
/nix/store/zbjnz39xh9j23s3ikh8cwp45gfd3hkf0-idris-helloIdris-0.0.1

And no executable is created:

$ tree result
result
├── libs
│   └── 00helloidris-idx.ibc
└── nix-support
    └── propagated-build-inputs

2 directories, 2 files

I’m on NixOS 18.09.

2

I tried to figure out why this warning would appear, but now I’m pretty convinced that that’s an Idris bug in the doc generation for modules that define a different namespace than their module name.

The executable not installing is something build-idris-package doesn’t have built-in support for yet. I’ll make a PR to fix this (edit: idrisPackages.build-idris-package: Install binaries by infinisil · Pull Request #60373 · NixOS/nixpkgs · GitHub). In the meantime you can just install it manually:

{ build-idris-package
, lib
}:
build-idris-package  {
  name = "helloIdris";
  version = "0.0.1";

  src = ./.;

  postInstall = ''
    mkdir -p $out/bin
    mv helloIdris $out/bin
  '';

  meta = {
    description = "Simple Idris program";
  };
}
1 Like