Buidling "Hello World" in Idris

Help
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