problem with Prelude

[vfrinken]

The lastest idris build doesn't pass all tests for me. I did git pull && make clean && make && make install and it failed some tests, (idris2/basic029 for example, but also other tests)

...
Building Idris 2 version: 0.1.0-048bce23a
...
... 
...
idris2/basic027: success
idris2/basic028: success
idris2/basic029: FAILURE
Golden value differs from actual value.
diff --git a/tests/idris2/basic029/expected b/tests/idris2/basic029/expected
index c08a343..a81f1cf 100644
--- a/tests/idris2/basic029/expected
+++ b/tests/idris2/basic029/expected
@@ -1,6 +1,7 @@
 1/1: Building Params (Params.idr)
-Main> 2
-Main> 0
-Main> 1
-Main> 1
+Error in TTC file: TTC data is in an older format, file: ["Prelude"], expected version: 21, actual version: 20
+Main> (interactive):1:1--1:8:Undefined name add
+Main> (interactive):1:1--1:8:Undefined name add
+Main> (interactive):1:1--1:8:Undefined name add
+Main> (interactive):1:1--1:8:Undefined name add

[gallais]

Error in TTC file: TTC data is in an older format, file: ["Prelude"], expected version: 21, actual version: 20

You have old ttc files lying around so you should clean them first & then it should work out.

@edwinb: would it make sense to silently recompile a module if the interface file we find is obsolete? Alternatively we could use build/VERSION/ instead of build thus guaranteeing we are never getting tripped over old versions. And if users run multiple versions of Idris 2 (e.g. a released one and a dev one for testing) then they're not constantly rebuilding all of the libraries.

[vfrinken]

but where? shouldn't the make clean part take care of that?

[fabianhjr]

@vfrinken I sometimes have had to run rm **.ttc and rm **.ttm to clean out the repo from stale files.

[vfrinken]

alright, that worked. Thanks

[edwinb]

@gallais It would be nice to do that, yes. I don't think there's any reason not to - I could never make it work in Idris 1 because the design was very odd, but I don't think there's any obstacle in Idris 2.

[FranckS]

Hi there,

I just wanted to update my version of Idris2 from sources, and I'm running into the same problem. Could you please tell me where are located the .ttc files that need to be removed? So far, I have :

• clone again
• removed the previous version of idris2 in ~/idris2/,
• removed all TTC files I could find,
• done make clean
• make install

And I still have the issue (in the test file interface012.idr this time). I'm very surprised that the Travis CI doesn't have the issue when building it. Is guess it's because it's using a docker container. Anyway, I temporarily fixed the installation issue on my side by changing the expected output for this only test that doesn't pass, and I feel a bit dirty by having done that ;) Is there no way we could remove these old files automatically with make clean? And where are they?

Many thanks!

Cheers,

[fabianhjr]

@FranckS, the ttc files for that test file would be under /tests, just do rm **.ttc or git clean -fdx at the project root. (warning, this last command will clean the project of any and all changes)

The CI doesn't run into this issue because it starts in a clean state / fresh clone and doesn't have previous ttc files lying around. (And not per se of it being conteinerized, if there was a TTC cache it could have run into this issue before)

In this thread, gallais and edwinb talked of a possible better workaround of Idris2 recompiling ttc files in older formats. (Not sure if either of them have started on that, if not it could be a good PR if someone has the time/engery to implement it)

[FranckS]

Thanks for your answer @fabianhjr ! But how is my set-up different from what the CI has if I start with a fresh clone too ? I did that yesterday, and I still had the same issue. I'll investigate later :)

[gallais]

It could be because of all of the *.ttc stored in ~/.idris2. I usually use find . -name "*.ttc" to find them. And then you can go nuclear with find . -name "*.ttc" | xargs rm if you want to remove them.

[diakopter]

I had a similar issue; we discussed it in the Idris slack a few days ago, but no resolution/suggestions...

You can invite yourself to the FunctionalProgramming slack here, and join the #idris channel

https://fpchat-invite.herokuapp.com/