anoma · jonaprieto · Jan 19, 2023 · Jan 11, 2023 · Jan 11, 2023 · Jan 11, 2023
diff --git a/Makefile b/Makefile
@@ -11,13 +11,15 @@ MDFILES:=$(patsubst docs/org/%,docs/md/%,$(ORGFILES:.org=.md))
 
 EXAMPLEMILESTONE=examples/milestone
 EXAMPLEHTMLOUTPUT=_docs/examples/html
-EXAMPLES= 	HelloWorld/HelloWorld.juvix \
-			Collatz/Collatz.juvix \
-			Fibonacci/Fibonacci.juvix \
-            Hanoi/Hanoi.juvix \
-            PascalsTriangle/PascalsTriangle.juvix \
-			TicTacToe/CLI/TicTacToe.juvix \
-			ValidityPredicates/SimpleFungibleToken.juvix
+EXAMPLES= Collatz/Collatz.juvix \
+	Demo/Demo.juvix \
+	Fibonacci/Fibonacci.juvix \
+	Hanoi/Hanoi.juvix \
+	HelloWorld/HelloWorld.juvix \
+	PascalsTriangle/PascalsTriangle.juvix \
+	TicTacToe/CLI/TicTacToe.juvix \
+	Tutorial/Tutorial.juvix \
+	ValidityPredicates/SimpleFungibleToken.juvix
 
 EXAMPLE_WEBAPP_OUTPUT=_docs/examples/webapp
 WEBAPP_EXAMPLES=TicTacToe/Web/TicTacToe.juvix
@@ -67,7 +69,7 @@ html-examples: $(EXAMPLES)
 $(EXAMPLES):
 	$(eval OUTPUTDIR=$(EXAMPLEHTMLOUTPUT)/$(dir $@))
 	@mkdir -p ${OUTPUTDIR}
-	@juvix html $(EXAMPLEMILESTONE)/$@ --recursive --output-dir=$(CURDIR)/${OUTPUTDIR} --print-metadata
+	@juvix html $(EXAMPLEMILESTONE)/$@ --output-dir=$(CURDIR)/${OUTPUTDIR}
 
 .PHONY: webapp-examples
 webapp-examples: $(WEBAPP_EXAMPLES)

diff --git a/README.org b/README.org
@@ -46,158 +46,18 @@ and test Juvix programs, you can use your favorite text editor, the =juvix=
 command line tool, the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Github Codespace]], and the [[https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope][Juvix Standard Lib Codespace]]. However, we recommend using the =juvix-mode= in [[https://docs.juvix.org/tooling/emacs-mode.html][Emacs]] or the
 plugin in [[https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode][VSCode]].
 
-** [[https://github.com/anoma/juvix/tree/main/examples/milestone][First examples of programs written in Juvix]]
+** Quick start
 
-The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running =juvix html --recursive FileName.juvix=.
-
-- [[https://docs.juvix.org/examples/html/HelloWorld/HelloWorld.html][HelloWorld.juvix]]
-- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
-- [[https://docs.juvix.org/examples/html/Hanoi/Hanoi.html][Hanoi.juvix]]
-- [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]]
-- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
-- [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]]
-- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]
-
-The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains
-common functions that can be used in Juvix programs.
-
-** Installation
-
-*** MacOS
-
-The easiest way to install Juvix on MacOS is by using [[https://brew.sh][Homebrew]].
-
-To install the [[https://github.com/anoma/homebrew-juvix][homebrew-juvix tap]], run:
-
-#+begin_src shell
-brew tap anoma/juvix
-#+end_src
-
-To install Juvix, run:
-
-#+begin_src shell
-brew install juvix
-#+end_src
-
-
-Helpful information on the shell can also be obtained by running:
-
-#+begin_src shell
-brew info juvix
-#+end_src
-
-*** Linux x86_64
-
-A Juvix compiler binary executable for Linux x86_64 is available on the [[https://github.com/anoma/juvix/releases/latest][Juvix release page]].
-
-To install this executable, downlaod and unzip the linked file and add move it
-to a directory on your shell's =PATH=.
-
-For example if =~/.local/bin= is on your shell's =PATH= you can install Juvix as
-follows:
-
-#+begin_src shell
-cd /tmp
-curl -OL https://github.com/anoma/juvix/releases/download/v0.2.8/juvix-linux_x86_64-v0.2.8.zip
-unzip juvix-linux_x86_64-v0.2.8.zip
-mv juvix-linux_x86_64-v0.2.8 ~/.local/bin/juvix
-#+end_src
-
-*** Building Juvix from source
-
-To install Juvix from source you must clone the [[https://github.com/anoma/juvix.git][Github repository]]. Then Juvix
-can be installed with the following commands. We assume you have [[https://haskellstack.org][Stack]]
-installed.
-
-#+begin_src shell
-git clone --recursive https://github.com/anoma/juvix.git
-cd juvix
-stack install
-#+end_src
-
-On MacOS you can alternatively run the following command for Homebrew. The flag
-=--HEAD= used below is optional, use it to build the latest version of Juvix in
-the =main= branch on Github.
-
-#+begin_src shell
-brew install --build-from-source --HEAD juvix --verbose
-#+end_src
-
-**  Quick Start
-
-After installation run =juvix --help= to see the list of commands available. See
-[[https://docs.juvix.org/getting-started/quick-start.html#cli-usage-examples][CLI usage examples]] for descriptions of common tasks.
-
-Run Juvix doctor to check your system setup:
-
-#+begin_src shell
-juvix doctor
-#+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 := putStrLn "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 [[https://anoma.github.io/juvix/getting-started/dependencies.html][Installing dependencies]] in the documentation 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
-
-** LSP support
-
-We provide a sammple =hie.yaml= configuration file for both =cabal= and =stack=.
-
-If you prefer =stack=, run:
-#+begin_src shell
-cp stack.hie.yaml hie.yaml
-#+end_src
-If you prefer =cabal=, run:
-#+begin_src shell
-cp cabal.hie.yaml hie.yaml
-#+end_src
-
-** Building the project with =cabal=
-
-We recommend that contributors use the =stack= build tool with this project.
-
-If you would prefer to use the =cabal= build tool instead then you must generate
-the =juvix.cabal= file using [[https://github.com/sol/hpack][hpack]] before running =cabal build=.
+See [[./quick-start.md][Quick start]] to start with Juvix.
 
 ** The Juvix programming language
 
-Juvix allows us to write programs with a high degree of assurance. The Juvix
-compiler runs several static analyses during the compilation phase to guarantee
-no runtime errors. Analyses permormed during this phase include scope,
-termination, arity, and type checkiqng. As a result, functional programs,
-especially validity predicates, can be written with greater confidence that they
-will be free of runtime errors.
+Juvix provides a high degree of assurance. The Juvix compiler runs
+several static analyses which guarantee the absence of runtime
+errors. Analyses performed include termination, arity, and type
+checking. As a result, functional programs, especially validity
+predicates, can be written with greater confidence in their
+correctness.
 
 Some of the language features in Juvix include:
 
@@ -209,15 +69,11 @@ Some of the language features in Juvix include:
 - holes in expressions
 - axioms for non-computable terms
 
-Additionally, the foreign and compile blocks syntax enable developers to compile
-a program to different backends including the =C= language. The Juvix module
-system further permits splitting programs into several modules to build
-libraries which can be later documented by generating HTML files based on the
-codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the Juvix
-standard library's website]]. For futher details, please refer to
-[[https://anoma.github.io/juvix/][the Juvix book]] which includes our
-[[https://anoma.github.io/juvix/introduction/changelog.html][latest updates]].
-
+The Juvix module system further permits splitting programs into
+several modules to build libraries which can be later documented by
+generating HTML files based on the codebase, see for example, [[https://anoma.github.io/juvix-stdlib/][the
+Juvix standard library's website]]. For further details, please refer to
+[[https://anoma.github.io/juvix/][the Juvix book]] which includes our [[https://anoma.github.io/juvix/changelog.html][latest updates]].
 
 ** Community
 

diff --git a/docs/org/SUMMARY.org b/docs/org/SUMMARY.org
@@ -2,34 +2,44 @@
 
 - [[./README.md][The Juvix project]]
 - [[./changelog.md][Changelog]]
-- [[./getting-started/README.md][Getting started]]
-  - [[./getting-started/quick-start.md][Quick start]]
-  - [[./getting-started/dependencies.md][Installing dependencies]]
-- [[./examples/README.md][Juvix Examples]]
-- [[./tutorials/README.md][Tutorials]]
-  - [[./tutorials/nodejs-interop.md][NodeJS Interop]]
+- [[./quick-start.md][Quick start]]
 
-- [[./language-reference/README.md][Language reference]]
-  - [[./language-reference/comments.md][Comments]]
-  - [[./language-reference/axiom.md][Axiom]]
-  - [[./language-reference/compile-blocks.md][Compile block]]
-  - [[./language-reference/modules.md][Module]]
-  - [[./language-reference/inductive-data-types.md][Data type]]
-  - [[./language-reference/functions.md][Function]]
-  - [[./language-reference/foreign-blocks.md][Foreign block]]
-  - [[./language-reference/termination-checking.md][Termination]]
+* Tutorials
+- [[./tutorials/learn.md][Learn Juvix in minutes]]
+- [[./tutorials/structure.md][Structuring Juvix projects]]
+- [[./tutorials/emacs.md][Juvix Emacs mode]]
+- [[./tutorials/vscode.md][Juvix VSCode extension]]
 
-- [[./tooling/README.md][Tooling]]
-  - [[./tooling/CLI.md][Command line interface]]
-  - [[./tooling/doctor.md][Doctor]]
-  - [[./tooling/emacs-mode.md][Emacs mode]]
-  - [[./tooling/testing.md][Haskell test suite]]
+* How-to guides
+- [[./howto/installing.md][Installing Juvix]]
+- [[./howto/compilation.md][Compiling Juvix programs]]
+- [[./howto/judoc.md][Judoc: Juvix documentation tool]]
 
-- [[./notes/README.md][Notes]]
-  - [[./notes/runtime-benchmark-results.md][Runtime benchmark results]]
-  - [[./notes/monomorphization.md][Monomorphization]]
-  - [[./examples/validity-predicates/README.md][Validity predicates]]
-  - [[./notes/strictly-positive-data-types.md][Strictly positive data types]]
+* Explanations
+- [[./explanations/typetheory.md][Type theory]]
+- [[./explanations/totality/README.md][Totality checking]]
+  - [[./explanations/totality/termination.md][Termination]]
+  - [[./explanations/totality/positive.md][Strictly positive data types]]
+  - [[./explanations/totality/coverage.md][Coverage checking]]
 
-- [[./README.md][About]]
-  - [[./introduction/about/community.md][Community]]
+* Reference
+- [[./reference/stdlib.md][Standard library]]
+- [[./reference/language/README.md][Language reference]]
+  - [[./reference/language/functions.md][Functions]]
+  - [[./reference/language/datatypes.md][Data types]]
+  - [[./reference/language/modules.md][Modules]]
+  - [[./reference/language/comments.md][Comments]]
+  - [[./reference/language/axioms.md][Axioms]]
+  - [[./reference/language/compileblocks.md][Compile blocks]]
+  - [[./reference/language/foreign.md][Foreign blocks]]
+- [[./reference/examples.md][Example programs]]
+- [[./reference/benchmarks.md][Benchmarks]]
+- [[./reference/tooling/README.md][Tooling]]
+  - [[./reference/tooling/CLI.md][Command line interface]]
+  - [[./reference/tooling/doctor.md][Doctor]]
+  - [[./reference/tooling/emacs.md][Emacs mode]]
+  - [[./reference/tooling/testing.md][Haskell test suite]]
+- [[./reference/judoc.md][Judoc reference]]
+
+* About
+- [[./about/community.md][Community]]
diff --git a/docs/org/introduction/about/community.org → docs/org/about/community.org b/docs/org/introduction/about/community.org → docs/org/about/community.org
diff --git a/docs/org/introduction/about/team.org → docs/org/about/team.org b/docs/org/introduction/about/team.org → docs/org/about/team.org
diff --git a/docs/org/backends/README.org b/docs/org/backends/README.org
diff --git a/docs/org/backends/minic.org b/docs/org/backends/minic.org
diff --git a/docs/org/compiler-architecture/language/abstract.org b/docs/org/compiler-architecture/language/abstract.org
diff --git a/docs/org/compiler-architecture/language/concrete.org b/docs/org/compiler-architecture/language/concrete.org
diff --git a/docs/org/compiler-architecture/language/microjuvix.org b/docs/org/compiler-architecture/language/microjuvix.org
diff --git a/docs/org/compiler-architecture/languages.org b/docs/org/compiler-architecture/languages.org
diff --git a/docs/org/compiler-architecture/pipeline.org b/docs/org/compiler-architecture/pipeline.org
diff --git a/docs/org/examples/README.org b/docs/org/examples/README.org
diff --git a/...nguage-reference/termination-checking.org → ...org/explanations/totality/termination.org b/...nguage-reference/termination-checking.org → ...org/explanations/totality/termination.org
diff --git a/docs/org/getting-started/README.org b/docs/org/getting-started/README.org
diff --git a/docs/org/getting-started/dependencies.org b/docs/org/getting-started/dependencies.org