Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WSL1 install error #44

Closed
edwinb opened this issue May 20, 2020 · 4 comments
Closed

WSL1 install error #44

edwinb opened this issue May 20, 2020 · 4 comments
Labels
Installation Issue Problem compiling or running Idris os: windows

Comments

@edwinb
Copy link
Collaborator

edwinb commented May 20, 2020

Issue by ice1000
Sunday Apr 05, 2020 at 02:32 GMT
Originally opened as edwinb/Idris2-boot#266


Master version of Idris2, getting this:

Exception: (while loading libcb.so) libcb.so: cannot open shared object file: No such file or directory
chez/chez010: FAILURE
Expected:
"9\nCallback coming\nIn callback\n24\nCallback coming\nIn callback with (1, 2)\n3\n9\n'k'\n1/1: Building CB (CB.idr)\nMain> Main> Bye for now!\n"
Given:
"1/1: Building CB (CB.idr)\nMain> Main> Bye for now!\n"
chez/chez011: success
chez/chez012: success
Exception: (while loading libstruct.so) libstruct.so: cannot open shared object file: No such file or directory
chez/chez013: FAILURE
Expected:
"(40, 30)\n\"Here\": (40, 30)\nMade it!\n1/1: Building Struct (Struct.idr)\nMain> Main> Bye for now!\n"
Given:
"1/1: Building Struct (Struct.idr)\nMain> Main> Bye for now!\n"
chez/chez014: success
200/202 tests successful
Makefile:4: recipe for target 'test' failed
make[1]: *** [test] Error 1
make[1]: Leaving directory '/home/ice1000/git-repos/idris2/tests'
Makefile:123: recipe for target 'test' failed
make: *** [test] Error 2

Where should I obtain libcb.so and libstruct.so? I'm using Chez scheme 9.5

@edwinb edwinb added the Installation Issue Problem compiling or running Idris label May 20, 2020
@edwinb
Copy link
Collaborator Author

edwinb commented May 20, 2020

Comment by timmyjose
Sunday Apr 05, 2020 at 07:10 GMT


@ice1000

I recall a similar issue for macOS which was fixed in this PR - https://github.com/edwinb/Idris2/pull/210/files.

I'm wondering whether the Makefile is getting confused and producing a dll instead of an so file.

Could you check the output of gcc -dumpmachine? Does the output contains cygwin, mingw, or windows? I suspect it might be showing mingw in which case this would need to be taken care of in the Makefile(s).

I think chez is perfectly innocent here!

@edwinb
Copy link
Collaborator Author

edwinb commented May 20, 2020

Comment by ice1000
Monday Apr 06, 2020 at 17:57 GMT


~/git-repos/idris2|master λ> gcc -dumpmachine
x86_64-linux-gnu

@timmyjose

@edwinb
Copy link
Collaborator Author

edwinb commented May 20, 2020

Comment by ice1000
Monday Apr 06, 2020 at 22:53 GMT


With the new test suite it becomes

Exception: (while loading libcb.so) libcb.so: cannot open shared object file: No such file or directory
chez/chez010: FAILURE
Golden value differs from actual value.
Accept actual value as new golden value? [yn]
n
chez/chez011: success
chez/chez012: success
Exception: (while loading libstruct.so) libstruct.so: cannot open shared object file: No such file or directory
chez/chez013: FAILURE
Golden value differs from actual value.
Accept actual value as new golden value? [yn]
n
chez/chez014: success
202/204 tests successful
Makefile:5: recipe for target 'test' failed
make[1]: *** [test] Error 1
make[1]: Leaving directory '/home/ice1000/git-repos/idris2/tests'
Makefile:123: recipe for target 'test' failed
make: *** [test] Error 2

It's still erroring but looks nicer

melted pushed a commit to melted/Idris2 that referenced this issue Jun 1, 2020
Just like all other pi-bound things, if m is an unbound implicit and we
have m ?x = m y as a unification problem, we can conclude ?x = y because
it has to be true for all ms.

This was implemented in Blodwen but I hadn't got around to it yet for
Idris2... fortunately it's a bit easier in Idris2!

Fixes idris-lang#44
@memoryruins
Copy link
Contributor

With WSL2, bd9498c, and the chezscheme9.5 package in Debian Buster, idris2 successfully bootstrapped and installed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Installation Issue Problem compiling or running Idris os: windows
Projects
None yet
Development

No branches or pull requests

3 participants