Cannot compile prelude with latest Idris, file read error

[edwinb]

Issue by andrevidela
Friday Jan 24, 2020 at 23:25 GMT
Originally opened as edwinb/Idris2-boot#187

---

steps to reproduce (on Mac OS 10.15.2)

1. clone the project
2. make install

Expected output

it works

Actual output

make -C libs/prelude install IDRIS2=../../idris2
../../idris2 --install prelude.ipkg
Uncaught error: File error (prelude): File Read Error
make[1]: *** [install] Error 1
make: *** [install-libs] Error 2

I can reproduce the problem with those steps as well:

1. compile Idris with make idris2
2. go to the prelude folder cd libs/prelude
3. compile manually with ../../idris2 --install prelude.ipkg

The error is the same.

I checked my permissions are correct (even with chmod 777) and tried running as sudo and the result is the same.

Any ideas?

[edwinb]

Comment by chrrasmussen
Friday Jan 31, 2020 at 17:37 GMT

---

I believe this problem may occur if make install does not complete succesfully (for example if some tests fail).

Uncaught error: File error (prelude): File Read Error happens because it is looking for the <idris2 install dir>/support/chez/support.ss, which has not been installed yet. If you run make install-support, then it should be possible to install the libraries.

[edwinb]

Comment by edwinb
Thursday Mar 05, 2020 at 10:36 GMT

---

If this is to do with the Mac chez test failures, perhaps it's okay now?

[edwinb]

Comment by andrevidela
Friday Mar 06, 2020 at 21:23 GMT

---

I tried again today and here are my findings:

It now fails at the idris2-fromc step, because sed -i isn't perfectly Multiplatform with Mac OS. I found this PR on Couch-db that fixes it by adding an empty string after the -i option when running on Mac OS.

Of course it works fine if I replace the sed call by gsed which is the gnu version but compiled for Mac OS.

However this fix only creates another, because compilation fail a bit later on compiling the c rts

make -C dist
make -C rts
clang  -O2 -Wall -std=c99 -pipe -fdata-sections -ffunction-sections -D_POSIX_C_SOURCE=200809L  -I/usr/local/include  -DIDRIS_TARGET_OS="\"darwin\"" -DIDRIS_TARGET_TRIPLE="\"x86_64-apple-darwin19.3.0\"" -fPIC   -c -o idris_rts.o idris_rts.c
idris_rts.c:1163:21: error: variable has incomplete type 'struct timespec'
    struct timespec t;
                    ^
idris_rts.c:1163:12: note: forward declaration of 'struct timespec'
    struct timespec t;
           ^
idris_rts.c:1167:12: warning: implicit declaration of function 'nanosleep' is
      invalid in C99 [-Wimplicit-function-declaration]
    return nanosleep(&t, NULL);
           ^
1 warning and 1 error generated.
make[2]: *** [idris_rts.o] Error 1
make[1]: *** [idris2] Error 2
make: *** [idris2-fromc] Error 2

[edwinb]

Comment by ziman
Sunday Mar 08, 2020 at 19:15 GMT

---

For the record, I had the problem described in OP and @chrrasmussen's advice helped, thank you!

[edwinb]

Comment by andrevidela
Sunday Mar 08, 2020 at 20:20 GMT

---

Which commit were you using @ziman ?

[edwinb]

Comment by ziman
Sunday Mar 08, 2020 at 20:22 GMT

---

I'm on the latest master, 25843793c72b96e76f0e4494c49734801b740294.

[edwinb]

Comment by ziman
Sunday Mar 08, 2020 at 20:23 GMT

---

Sorry, I forgot to mention that I'm on Linux; that's probably important.

The part of this issue that manifests also on Linux is fixed by @chrrasmussen's trick.

[edwinb]

Comment by andylokandy
Thursday Apr 09, 2020 at 18:55 GMT

---

I have the same problem on win10. I've found that the prefix generated in dist/idris2.c is incorrect. I fixed the first line and rebuilt the idris2 binary, then I could install the libs.

[edwinb]

Comment by andrevidela
Thursday Apr 09, 2020 at 22:37 GMT

---

Fixed the first line and rebuilt the idris2 binary

What change dud you make?

[edwinb]

Comment by andylokandy
Friday Apr 10, 2020 at 08:21 GMT

---

I hand-wrote the absolute prefix path into dist/idris2.c as:

char* idris2_prefix = "C:\\Users\\Andy\\.idris2";

[edwinb]

Give that this is about Idris2-boot, and so everything is likely to have changed, I'm going to close this.