* Quick Start

#+begin_html
<a href="https://github.com/anoma/juvix">
<img align="left" width="200" height="200" alt="Juvix Mascot" src="assets/images/tara-teaching.svg" />
</a>
#+end_html

To install Juvix, follow the instruction in the [[./howto/installing.md][Installation How-to]].

After installation, run =juvix --help= to see the list of commands.

Run Juvix doctor to check your system setup:

#+begin_src shell
juvix doctor
#+end_src

** CLI Usage Examples

Create a new package:

#+begin_src shell
juvix init
#+end_src

Compile a source file into an executable:

#+begin_src shell
juvix compile path/to/source.juvix
#+end_src

Compile a source file into a WebAssembly binary:

#+begin_src shell
juvix compile -t wasm path/to/source.juvix
#+end_src

Launch the REPL:

#+begin_src shell
juvix repl
#+end_src

Typecheck a source file:

#+begin_src shell
juvix typecheck path/to/source.juvix
#+end_src

Generate HTML representations of a source file and its imports:

#+begin_src shell
juvix html --recursive path/to/source.juvix
#+end_src

** The Hello World example

This is the Juvix source code of the traditional Hello World program.

#+begin_src shell
-- HelloWorld.juvix
module HelloWorld;

open import Stdlib.Prelude;

main : IO;
main := printStringLn "hello world!";

end;
#+end_src

To compile and run a binary generated by Juvix, save the source code to a file
called =HelloWorld.juvix= and run the following command from the directory
containing it:

#+begin_src shell
juvix compile HelloWorld.juvix
./HelloWorld
#+end_src

You should see the output: =hello world!=

The source code can also be compiled to a WebAssembly binary. This requires some additional setup. See the [[https://anoma.github.io/juvix/howto/installing.html][Installation How-to]] for more information. You can also run =juvix doctor= to check your setup.

#+begin_src shell
juvix compile --target wasm HelloWorld.juvix
wasmer HelloWorld.wasm
#+end_src