Hello world/Newbie: Difference between revisions
→{{header|Agda}}: added Agda
m (→{{header|Coq}}) |
(→{{header|Agda}}: added Agda) |
||
Line 100:
The output will appear in the command prompt/terminal.
=={{header|Agda}}==
This tutorial is to install Agda-2.6.2, the most recent version as of October 2021, and run the "Hello world" program. The snippet is based on the [https://agda.readthedocs.io/en/v2.6.2/getting-started/hello-world.html Hello world example] given in the Agda documentation, although using less Unicode symbols. More detailed explanations can be found in the [https://agda.readthedocs.io/en/v2.6.2/getting-started/installation.html installation instructions].
Although Agda developers suggest using [https://en.wikipedia.org/wiki/Emacs Emacs], this tutorial does not assume having Emacs installed.
# Install [https://en.wikipedia.org/wiki/Cabal_(software) Cabal]. On Linux run: <lang bash>sudo apt install cabal-install</lang>
# From the command line, execute: <lang bash>cabal update</lang> which outputs ''Downloading the latest package list from hackage.haskell.org''
# Install Agda with: <lang bash>cabal install Agda</lang> This downloads the packages and then outputs ''Building Agda-2.6.2''. The building process can take several minutes.
# After that, Cabal creates two binaries. On Linux these are <pre>~/.cabal/bin/agda</pre> and <pre>~/.cabal/bin/agda-mode</pre> Make those binaries reachable by the ''PATH'' variable.
# Create the file ''helloworld.agda'' with any editor and paste this snippet: <lang agda>module helloworld where
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit renaming (⊤ to Unit)
open import Agda.Builtin.String using (String)
postulate putStrLn : String -> IO Unit
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
main : IO Unit
main = putStrLn "Hello world!"
</lang> (Note that "⊤" is not a capital T, but the [https://en.wikipedia.org/wiki/Tee_(symbol) top symbol]).
# Run <lang bash>agda --compile helloworld.agda</lang> This creates the binary ''helloworld''
# Execute the binary. For example, on Linux run <lang bash>./helloworld</lang> The execution outputs ''Hello world!''
=={{header|ARM Assembly}}==
| |||