can't test because can't find contrib

[shmish111]

After running make install I manage to build Idris and seemingly all the libs however when it gets to testing I get

➜  Idris2 git:(2a0e5a4) ✗ make test
idris --build tests.ipkg
Entering directory `./tests'
The following packages were specified but cannot be found:
- contrib
make: *** [test] Error 1

[shmish111]

I did make clean && make install again to make sure and to show the end of the logs here which shows that contrib is built

network library tests SUCCESS
make -C libs/contrib IDRIS2=../../idris2
../../idris2 --build contrib.ipkg
1/13: Building Syntax.WithProof (Syntax/WithProof.idr)
2/13: Building Syntax.PreorderReasoning (Syntax/PreorderReasoning.idr)
3/13: Building Data.List.TailRec (Data/List/TailRec.idr)
4/13: Building Data.Bool.Extra (Data/Bool/Extra.idr)
5/13: Building Data.SortedMap (Data/SortedMap.idr)
6/13: Building Data.SortedSet (Data/SortedSet.idr)
7/13: Building Text.Token (Text/Token.idr)
8/13: Building Text.Quantity (Text/Quantity.idr)
9/13: Building Control.Delayed (Control/Delayed.idr)
10/13: Building Text.Parser.Core (Text/Parser/Core.idr)
11/13: Building Text.Parser (Text/Parser.idr)
12/13: Building Text.Lexer.Core (Text/Lexer/Core.idr)
13/13: Building Text.Lexer (Text/Lexer.idr)
idris --build tests.ipkg
Entering directory `./tests'
The following packages were specified but cannot be found:
- contrib
make: *** [test] Error 1

[ziman]

Perhaps try make install-libs first and then make install?

This should install the libs before running the tests.

[gallais]

Is it contrib for idris2 or contrib for idris that is missing? Given it happens during idris --build tests.ipkg, I would suspect the latter.

[edwinb]

Most likely we need to add contrib to IDRIS2_PATH in the Makefile. It won't be looking anywhere for it as things stand, and the tests therefore only work by chance. I'm surprised travis doesn't catch this though...

[shmish111]

I;ve tried make install-libs with no success @ziman I changed the following, also with no success @edwinb

export IDRIS2_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc:${CURDIR}/libs/network/build/ttc:${CURDIR}/libs/contrib/build/ttc

export IDRIS2_LIBS = ${CURDIR}/libs/network:${CURDIR}/libs/contrib

Unfortunately the same error

[shmish111]

tests.ipkg seems to be the only place in the project that actually explicitly imports a package. What I don't get is how it seems to work for everyone else.

[fabianhjr]

It didnt work for me at first so I read the Makefile install / install-all and went step by step skipping tests. After installing everything it fixed itself.

[shmish111]

FYI I also checked that the ttc files exist on contrib and indeed they do

[shmish111]

oh, tests are built using idris 1, is this correct?

[fabianhjr]

Oh wait, I remember what I did, just remove the contrib package dependency from tests.ipkg, it isn't needed.

[shmish111]

ok, that seems to work @fabianhjr however I'm very confused, are the tests running with idris 1, it seems from the makefile that they are and this is why contrib couldn't be found (it was looking for idris 1 contrib which I haven't installed). @edwinb do you want a PR with the contrib dep removed from the tests.ipkg?

[gallais]

however I'm very confused, are the tests running with idris 1

idris 1 is used to compile the test runner. The runner uses idris 2 on all of the test cases it is tasked with.