idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.5k stars 375 forks source link

Runtime exception with contrib function. Linking problem? #1221

Closed ysangkok closed 3 years ago

ysangkok commented 3 years ago

Steps to Reproduce

test.ipkg:

package test

authors    = "Janus"
version    = "0.1"
readme     = "README.md"

modules = Test

sourcedir = "src"

depends = base, contrib

src/Test.idr:

module Test

import Language.JSON

p : Maybe JSON
p = parse "{}"

export
main : IO ()
main = case p of Just per => print "hi"; _ => print "no"

Expected Behavior

The program prints "hi".

Observed Behavior

% idris2 --repl test.ipkg
Warning: Deprecation warning: version numbers must now be of the form x.y.z
1/1: Building Test (src/Test.idr)
Test> :exec main
Exception: variable LanguageC-45JSONC-45Lexer-lexJSON is not bound

And if I rerun the idris2 --repl command:

Error: Undefined name unsafePerformIO.

gallais commented 3 years ago

You seem to have a broken install. A fresh install generally solves these kind of issues.

Or it may be that you need to import more of the Language.* modules. Cf #1086 for a similar issue.

ysangkok commented 3 years ago

I don't think it could be a broken install since I wiped the installation and used make clean:

cd ~/idris2
rm -rf ~/.idris2/
git pull
make clean
sudo apt install chezscheme
make bootstrap SCHEME=chezscheme
make install
cd ../bug
idris2 --repl test.ipkg
Test> :exec main
Exception: variable LanguageC-45JSONC-45Lexer-lexJSON is not bound

I will now try to experiment with imports.

ysangkok commented 3 years ago

Ok, by sequentially adding the modules mentioned in the errors, the program now runs. These are the modules I had to add:

import Language.JSON.Lexer
import Text.Lexer
import Language.JSON.String
import Language.JSON.String.Lexer
import Data.String
import Data.List
import Language.JSON.Parser
import Text.Parser
gallais commented 3 years ago

Right I really think it's #1086 again then. We seem to have scoping issues when compiling code that transitively relies on the content of some modules. Which is strange because Idris itself does have this kind of structure too and I don't think we've hit that bug working on Idris proper yet!

ysangkok commented 3 years ago

Ok, I'll close this then, since it is a duplicate.