[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