UlfNorell
commented
10 years ago From nils.anders.danielsson on November 25, 2013 07:18:27
Failed to find source of module Foreign.Haskell in any of the following locations: [...] /home/mechvel/agda/lib-nov-25-2013/src/Foreign/Haskell.agda [...] And /home/mechvel/agda/lib-nov25-2013/src/Foreign/Haskell.agda does exist:
The directory names don't match.
Status: Invalid
From mech...@botik.ru on November 25, 2013 12:38:44
I am trying to install Agda and Standard library taken from darcs on November 25, 2013.
It (of November 24) works on one Debian Linux machine. And after installing them on another Debian Linux machine , it reports for
Checking AlgTest (/home/mechvel/doconA/0.03/source/demoTest/AlgTest.agda). /home/mechvel/doconA/0.03/source/demoTest/AlgTest.agda:2,13-28 Failed to find source of module Foreign.Haskell in any of the following locations: /home/mechvel/doconA/0.03/source/Foreign/Haskell.agda /home/mechvel/doconA/0.03/source/Foreign/Haskell.lagda /home/mechvel/agda/lib-nov-25-2013/src/Foreign/Haskell.agda /home/mechvel/agda/lib-nov-25-2013/src/Foreign/Haskell.lagda /home/mechvel/doconA/0.03/source/demoTest/Foreign/Haskell.agda /home/mechvel/doconA/0.03/source/demoTest/Foreign/Haskell.lagda /home/mechvel/.cabal/share/i386-linux-ghc-7.6.2/Agda-2.3.3/lib/prim/Foreign/Haskell.agda /home/mechvel/.cabal/share/i386-linux-ghc-7.6.2/Agda-2.3.3/lib/prim/Foreign/Haskell.lagda when scope checking the declaration open import Foreign.Haskell
And /home/mechvel/agda/lib-nov25-2013/src/Foreign/Haskell.agda
does exist:
... module Foreign.Haskell where ... data Unit : Set where
...
Why does not it find this module?
Among `share/' , I see only /home/mechvel/.cabal/share/Agda-2.3.3 : Agda.css agda.sty emacs-mode EpicInclude lib
And there does not exist any ...share/i386-linux-ghc-7.6.2/, why Agda searches there?
The first machine has ghc-7.6.3 istalled, the second -- ghc-7.6.2. But probably, this must not effect ...
What may be the matter, please?
Original issue: http://code.google.com/p/agda/issues/detail?id=979