[Agda] Hello World

[Guillaume Yziquel]

Hi.

I finally have found some free time to try out Agda, and I'm having
trouble getting a Hello World to compile properly.

        yziquel at seldon:~/git/agda-learning$ agda -V
        Agda version 2.2.6
        yziquel at seldon:~/git/agda-learning$ cat Main.agda
        module Main where

        data Unit : Set where
          unit : Unit

        {-# COMPILED_DATA Unit () () #-}

        postulate IO : Set -> Set
        {-# COMPILED_TYPE IO IO #-}

        open import Data.String

        postulate
          putStrLn : String -> IO Unit

        {-# COMPILED putStrLn putStrLn #-}

        main : IO Unit
        main = putStrLn "Hello World!"
        yziquel at seldon:~/git/agda-learning$ agda -c Main.agda
        Checking Main (/home/yziquel/git/agda-learning/Main.agda).
        /home/yziquel/git/agda-learning/Main.agda:11,1-24
        Failed to find source of module Data.String in any of the following
        locations:
          /home/yziquel/git/agda-learning/Data/String.agda
          /home/yziquel/git/agda-learning/Data/String.lagda
        when scope checking the declaration
          open import Data.String

However String.agda is locate in /usr/lib/agda-stdblib/Data:

        yziquel at seldon:~/git/agda-learning$ locate String.agda
        /usr/lib/agda-stdlib/Data/String.agda
        /usr/lib/agda-stdlib/Data/String.agdai

How do you get it to link properly?

-- 
     Guillaume Yziquel