search

NixOS / nixpkgs

Nix Packages collection & NixOS
MIT License
17.31k stars 13.54k forks source link

idris2 REPL is broken #130310

Closed fogti closed 3 years ago

fogti commented 3 years ago

Describe the bug

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

Welcome to Idris 2.  Enjoy yourself!
Uncaught error: Error: Module Prelude not found

(Interactive):1:1--1:1
 1 |

executing idris2 terminates with an error. This didn't happen with idris2 Version 0.3.

To Reproduce See above and below.

Expected behavior The REPL should successfully start and present its own prompt

Additional context

Notify maintainers @fabianhjr @wchresta

Metadata

Maintainer information:

attribute:
  - idris2
module:
fabianhjr commented 3 years ago 
~/.nix-profile/bin/idris2                                                                  3177ms  Thu 15 Jul 2021 04:54:56 PM CDT
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.4.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
Main> 10 + 20
30
Main> 
Bye for now!

Could you try setting IDRIS2_{PATH,DATA,LIBS}?

In particular, they should be set here: https://github.com/NixOS/nixpkgs/blob/dbb371403bf3b555d16df01108a8deb0f7c10650/pkgs/development/compilers/idris2/default.nix#L78-L80

fogti commented 3 years ago 
$ bash -x /etc/profiles/per-user/zseri/bin/idris2
+ export CHEZ=/nix/store/69ys5ichqp70bscm9a5nc7p3vs373f0m-chez-scheme-9.5.4/bin/scheme
+ CHEZ=/nix/store/69ys5ichqp70bscm9a5nc7p3vs373f0m-chez-scheme-9.5.4/bin/scheme
+ export IDRIS2_LIBS=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/lib
+ IDRIS2_LIBS=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/lib
+ export IDRIS2_DATA=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/support
+ IDRIS2_DATA=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/support
+ export IDRIS2_PATH=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/base:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/contrib:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/network:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/prelude
+ IDRIS2_PATH=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/base:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/contrib:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/network:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/prelude
+ export LD_LIBRARY_PATH=/nix/store/zxhbjpb1x6xk4kiich46q21hfad54ffp-sane-config/lib/sane:/run/current-system/sw/lib/pipewire:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/lib
+ LD_LIBRARY_PATH=/nix/store/zxhbjpb1x6xk4kiich46q21hfad54ffp-sane-config/lib/sane:/run/current-system/sw/lib/pipewire:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/lib
+ exec -a /etc/profiles/per-user/zseri/bin/idris2 /nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/bin/.idris2-wrapped
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.4.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
Uncaught error: Error: Module Prelude not found

(Interactive):1:1--1:1
 1 | 
$ ls -las /nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0
total 0
0 dr-xr-xr-x 1 root root 160  1. Jan 1970  .
0 dr-xr-xr-x 1 root root  36  1. Jan 1970  ..
0 dr-xr-xr-x 1 root root  98  1. Jan 1970  base-0.4.0
0 dr-xr-xr-x 1 root root 110  1. Jan 1970  contrib-0.4.0
0 dr-xr-xr-x 1 root root 180  1. Jan 1970  include
0 dr-xr-xr-x 1 root root  78  1. Jan 1970  lib
0 dr-xr-xr-x 1 root root  28  1. Jan 1970  network-0.4.0
0 dr-xr-xr-x 1 root root  78  1. Jan 1970  prelude-0.4.0
0 dr-xr-xr-x 1 root root 266  1. Jan 1970  refc
0 dr-xr-xr-x 1 root root  44  1. Jan 1970  support
0 dr-xr-xr-x 1 root root   8  1. Jan 1970  test-0.4.0

The library paths mismatch.

fabianhjr commented 3 years ago

Hey, your ls -las /nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0 seems to be empty. :O

This is what my recent install (nix-env -iA nixos.idris2) looks like:

 l /nix/store/gn1nhwqxhn687acallpaagnwm9yp1knk-idris2-0.4.0/idris2-0.4.0      Thu 15 Jul 2021 05:10:26 PM CDT
total 44K
dr-xr-xr-x 11 root root 4.0K Dec 31  1969 .
dr-xr-xr-x  5 root root 4.0K Dec 31  1969 ..
dr-xr-xr-x  8 root root 4.0K Dec 31  1969 base-0.4.0
dr-xr-xr-x 11 root root 4.0K Dec 31  1969 contrib-0.4.0
dr-xr-xr-x  2 root root 4.0K Dec 31  1969 include
dr-xr-xr-x  2 root root 4.0K Dec 31  1969 lib
dr-xr-xr-x  4 root root 4.0K Dec 31  1969 network-0.4.0
dr-xr-xr-x  3 root root 4.0K Dec 31  1969 prelude-0.4.0
dr-xr-xr-x  2 root root 4.0K Dec 31  1969 refc
dr-xr-xr-x  7 root root 4.0K Dec 31  1969 support
dr-xr-xr-x  3 root root 4.0K Dec 31  1969 test-0.4.0
fogti commented 3 years ago

huh, why does it seems empty, it clearly contains stuff?

nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0
├── base-0.4.0
│   ├── Control
│   │   ├── App
│   │   │   ├── Console.ttc
│   │   │   └── FileIO.ttc
│   │   ├── Applicative
│   │   │   └── Const.ttc
│   │   ├── App.ttc
│   │   ├── Monad
│   │   │   ├── Either.ttc
│   │   │   ├── Error
│   │   │   │   ├── Either.ttc
│   │   │   │   └── Interface.ttc
│   │   │   ├── Identity.ttc
│   │   │   ├── Maybe.ttc
│   │   │   ├── Reader
│   │   │   │   ├── Interface.ttc
│   │   │   │   └── Reader.ttc
│   │   │   ├── Reader.ttc
│   │   │   ├── RWS
│   │   │   │   ├── CPS.ttc
│   │   │   │   └── Interface.ttc
│   │   │   ├── RWS.ttc
│   │   │   ├── State
│   │   │   │   ├── Interface.ttc
│   │   │   │   └── State.ttc
│   │   │   ├── State.ttc
│   │   │   ├── ST.ttc
│   │   │   ├── Trans.ttc
│   │   │   ├── Writer
│   │   │   │   ├── CPS.ttc
│   │   │   │   └── Interface.ttc
│   │   │   └── Writer.ttc
│   │   └── WellFounded.ttc
│   ├── Data
│   │   ├── Bifoldable.ttc
fabianhjr commented 3 years ago

Ah sorry, I misread the columns then.

fabianhjr commented 3 years ago

Can you compile and run execs?

fogti commented 3 years ago

suggestion:

-    packagePaths = builtins.map (l: "$out/${name}/" + l) includedLibs;
+    packagePaths = builtins.map (l: "$out/${name}/" + l + "-${version}") includedLibs;
fogti commented 3 years ago

when I manually adjust the library paths to include the version, it works:

$
  CHEZ=/nix/store/69ys5ichqp70bscm9a5nc7p3vs373f0m-chez-scheme-9.5.4/bin/scheme IDRIS2_LIBS=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/lib
  IDRIS2_DATA=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/support
  IDRIS2_PATH=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/base-0.4.0:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/contrib-0.4.0:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/network-0.4.0:/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/prelude-0.4.0
  LD_LIBRARY_PATH=/nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/idris2-0.4.0/lib
  /nix/store/lbpcl5lkpk881i3rmpqpz9a4h28a0zlv-idris2-0.4.0/bin/.idris2-wrapped
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.4.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
Main> 
Bye for now!
fabianhjr commented 3 years ago 
import Data.List
import System

main : IO ()
main = do
  env <- getEnvironment
  putStrLn . show $ env
  putStrLn . show $ lookup "IDRIS2_PATH" env
  putStrLn . show $ lookup "IDRIS2_LIBS" env
  putStrLn . show $ lookup "IDRIS2_DATA" env

Run with idris2 [file_name.idr] --exec main

fabianhjr commented 3 years ago

suggestion:

-    packagePaths = builtins.map (l: "$out/${name}/" + l) includedLibs;
+    packagePaths = builtins.map (l: "$out/${name}/" + l + "-${version}") includedLibs;

Will apply, though I am now concerned about the different behavior in NixOS, so maybe I am getting the libs from somewhere else DX