[Agda] compiling Hello.agda

Paul van der Walt paul at denknerd.org
Wed Jul 18 20:48:11 CEST 2012


Hi Serge,

On Wed, Jul 18, 2012 at 22:11:58 +0400, quoth Serge D. Mechveliani:
> I put this file to  $myProjectRoot  and command there
> (in Debian Linux, tcshell)
> 
>  agda -c -i /home/mechvel/.cabal/lib/agda-lib-ffi-0.0.1/ghc-7.4.1 Hello.agda

This all looks good, but I think you should also add "-i ." to
you command - Agda must also search the current directory to be
able to find your module.

I hope this helps, if I'm barking up the wrong tree, my
apologies.

Good luck,

Paul
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120718/6fa93d2d/attachment-0001.bin


More information about the Agda mailing list