Update some docs (#1391)

* Documment a few language features

* Add an example for foreign example

* Fix pre-commit warnings

* remove what-is-org

* Ignore README.org in docs folder

* Add fixes for revisions

.github/workflows/ci.yml

@@ -1,6 +1,7 @@
 name: The Juvix compiler CI
 
 on:
+  workflow_dispatch:
   pull_request:
     branches:
       - main
@@ -183,7 +184,8 @@ jobs:
           make install-shelltest
           make test-shell
   docs:
-    if: github.event.pull_request.merged == true
+    needs: build
+    if: github.event.pull_request.merged == true || github.event_name == 'workflow_dispatch'
     strategy:
       matrix:
         os: [ubuntu-latest]

.gitignore

@@ -74,3 +74,5 @@ docs/md/
 _docs
 docs/**/*.md
 **/html/*
+
+docs/org/README.org

Makefile

@@ -17,9 +17,6 @@ EXAMPLES=ValidityPredicates/SimpleFungibleToken.juvix \
 ORGTOMDPRG ?=pandoc
 ORGOPTS=--from org --to markdown_strict -s -o $@
 
-# ORGTOMDPRG ?=emacs
-# ORGOPTS=--batch -f org-html-export-to-markdown
-
 ifeq ($(UNAME), Darwin)
 	THREADS := $(shell sysctl -n hw.logicalcpu)
 else ifeq ($(UNAME), Linux)
@@ -31,13 +28,17 @@ endif
 all:
 	make pre-commit
 
+docs/md/README.md :
+	@mkdir -p docs/md
+	@${ORGTOMDPRG} README.org ${ORGOPTS}
+
 docs/md/%.md : docs/org/%.org
 	@echo "Processing ...  $@"
 	@mkdir -p $(dir $@)
 	${ORGTOMDPRG} $? ${ORGOPTS}
 
 .PHONY: markdown-docs
-markdown-docs: $(MDFILES)
+markdown-docs: docs/md/README.md $(MDFILES)
 	@echo "copying assets ..."
 	@mkdir -p docs/md/assets
 	@cp -v $(addprefix assets/,$(ASSETS)) docs/md/assets

README.org

@@ -49,7 +49,16 @@ The language features:
 
 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 icludes our [[https://anoma.github.io/juvix/introduction/changelog.html][latest updates]].
 
- [[https://github.com/anoma/juvix/tree/main/examples/milestone][See a few examples of Juvix programs]].
+** [[https://github.com/anoma/juvix/tree/main/examples/milestone][Examples of programs written in Juvix]]
+
+The following links are clickable versions of their corresponding Juvix programs. The HTML output can be generated by running =juvix html --recursive FileName.juvix=.
+
+- [[https://anoma.github.io/juvix-stdlib/][The Juvix standard library]]
+- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]
+- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
+- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
+- [[https://docs.juvix.org/examples/html/MiniTicTacToe/MiniTicTacToe.html][MiniTicTacToe.juvix]]
+
 
 ** Quick Start
 
@@ -65,7 +74,7 @@ cd juvix
 stack install
 #+end_src
 
-If the installation succeeds, you must be able to run the =juvix=
+If the installation succeeds, you must be able to run the Juvix
 command from any location. To get the complete list of commands, please
 run =juvix --help=.
 

docs/org/SUMMARY.org

@@ -1,42 +1,40 @@
 * Summary
 
-- [[./introduction/about/what-is.md][Juvix]]
+- [[./README.md][The Juvix project]]
 - [[./introduction/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][Tutorials]]
-  - [[./examples/backend-specific/minic-hello-world.md][Hello world]]
-  - [[./examples/validity-predicates/PolyFungibleToken.md][A simple fungible token]]
+- [[./examples/README.md][Juvix Examples]]
 
 - [[./language-reference/README.md][Language reference]]
   - [[./language-reference/comments.md][Comments]]
   - [[./language-reference/axiom.md][Axiom]]
   - [[./language-reference/functions.md][Function]]
   - [[./language-reference/modules.md][Module]]
   - [[./language-reference/inductive-data-types.md][Data type]]
-  - [[./language-reference/termination-checking.md][Termination checking]]
   - [[./language-reference/compile-blocks.md][Compile block]]
   - [[./language-reference/foreign-blocks.md][Foreign block]]
-  - [[./backends/README.md][Backends]]
-    - [[./backends/minic.md][MiniC]]
-    - [[./backends/minihaskell.md][MiniHaskell]]
-  - [[./compiler-architecture/README][Compiler architecture]]
-    - [[./compiler-architecture/pipeline.md][Pipeline]]
-    - [[./compiler-architecture/languages.md][Internal languages]]
-      - [[./compiler-architecture/language/abstract.md][Abstract language]]
-      - [[./compiler-architecture/language/concrete.md][Concrete language]]
-      - [[./compiler-architecture/language/microjuvix.md][MicroJuvix]]
+  - [[./language-reference/termination-checking.md][Termination]]
+  # - [[./backends/README.md][Backends]]
+  #   - [[./backends/minic.md][C]]s
+  #   - [[./backends/minihaskell.md][Haskell]]
+  # - [[./compiler-architecture/README][Compiler architecture]]
+  #   - [[./compiler-architecture/pipeline.md][Pipeline]]
+  #   - [[./compiler-architecture/languages.md][Internal languages]]
+  #     - [[./compiler-architecture/language/abstract.md][Abstract language]]
+  #     - [[./compiler-architecture/language/concrete.md][Concrete language]]
+  #     - [[./compiler-architecture/language/microjuvix.md][MicroJuvix]]
 
 - [[./tooling/README.md][Tooling]]
   - [[./tooling/CLI.md][Command line interface]]
   - [[./tooling/emacs-mode.md][Emacs mode]]
   - [[./tooling/testing.md][Haskell test suite]]
 
-- [[./notes/README.md][Blog]]
+- [[./notes/README.md][Notes]]
   - [[./examples/validity-predicates/README.md][Validity predicates]]
   - [[./notes/monomorphization.md][Monomorphization]]
 
 - [[./introduction/about/what-is.md][About]]
-  - [[./introduction/about/team.md][The dev team]]
+  # - [[./introduction/about/team.md][The dev team]]
   - [[./introduction/about/community.md][Community]]

docs/org/examples/README.org

@@ -1,2 +1,9 @@
-- [[./backend-specific/minic-hello-world.md][Hello world]]
-- [[./validity-predicates/PolyFungibleToken.md][Fungible Token]]
+** [[https://github.com/anoma/juvix/tree/main/examples/milestone][Examples of programs written in Juvix]]
+
+The following links are clickable versions of their corresponding Juvix programs. The HTML output can be generated by running =juvix html --recursive FileName.juvix=.
+
+- [[https://anoma.github.io/juvix-stdlib/][The Juvix standard library]]
+- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]]
+- [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]]
+- [[https://docs.juvix.org/examples/html/Fibonacci/Fibonacci.html][Fibonacci.juvix]]
+- [[https://docs.juvix.org/examples/html/MiniTicTacToe/MiniTicTacToe.html][MiniTicTacToe.juvix]]

docs/org/examples/backend-specific/minic-hello-world.org

@@ -1,4 +1,4 @@
-* Mini C Hello World
+* Hello World
 
 In the following example a Juvix file is compiled using the C backend.
 

docs/org/getting-started/dependencies.org

@@ -1,6 +1,7 @@
+
 * Installing dependencies
 
-The following dependencies are required for the juvix WASM compiler.
+The following dependencies are only required for compiling to WASM.
 
 - [[https://wasmer.io][wasmer]]
 - [[https://releases.llvm.org/download.html][Clang / LLVM]] version 13 or later (NB: On macOS the preinstalled clang does not support the wasm

docs/org/getting-started/quick-start.org

@@ -19,7 +19,7 @@ cd juvix
 stack install
 #+end_src
 
-If the installation succeeds, you must be able to run the =juvix=
+If the installation succeeds, you must be able to run the Juvix
 command from any location.
 
 

docs/org/language-reference/axiom.org

@@ -1,9 +1,8 @@
 * Axiom
 
-An axiom/postulate can be introduced by using the =axiom= keyword.
+Axioms or postulates can be introduced by using the =axiom= keyword.
 For example, let us imagine one wants to write a program that assumes
-$A$ is a type and there exist a term $x$ that inhabits $A$. Then the program would
-like like the following.
+$A$ is a type, and there exists a term $x$ that inhabits $A$. Then the program would look like the following.
 
 #+begin_src
 -- Example.juvix
@@ -13,6 +12,5 @@ module Example;
 end;
 #+end_src
 
-Terms introduced by the =axiom= keyword lack of any computational content. However,
-it is possible to attach a computational content to an axiom by giving compilation rules,
-see [[./compile-blocks.md][Compile blocks]].
+Terms introduced by the =axiom= keyword lack any computational content. However,
+it is possible to attach computational content to an axiom by giving compilation rules, see [[./compile-blocks.md][the =compile= keyword]].

docs/org/language-reference/builtins.org

@@ -0,0 +1,31 @@
+
+* Built-ins
+
+Juvix has support for the built-in natural type and a few functions that are compiled to efficient primitives.
+
+1. Built-in inductive definitions.
+
+   #+begin_example
+   builtin natural
+   inductive Nat {
+     zero : Nat;
+     suc : Nat → Nat;
+   };
+   #+end_example
+
+2. Builtin function definitions.
+
+   #+begin_example
+   inifl 6 +;
+   builtin natural-plus
+   + : Nat → Nat → Nat;
+   + zero b ≔ b;
+   + (suc a) b ≔ suc (a + b);
+   #+end_example
+
+3. Builtin axiom definitions.
+
+   #+begin_example
+   builtin natural-print
+   axiom printNat : Nat → Action;
+   #+end_example

docs/org/language-reference/comments.org

@@ -1,6 +1,6 @@
 * Comments
 
-A comment is introduced in the same fashion as in Haskell/Agda.
+A comment is introduced in the same fashion as in =Haskell=/=Agda=.
 
 - Inline Comment
 #+begin_src

docs/org/language-reference/compile-blocks.org

@@ -1 +1,65 @@
 * Compile blocks
+
+The compile keyword has two arguments:
+
+- A name of an expression to be compiled.
+- A set of compilation rules using the format (=backend= → =string=)
+  where the string is the text we inline.
+
+This is an example:
+
+#+begin_src haskell
+$ cat tests/positive/HelloWorld
+...
+axiom Action : Type;
+compile Action {
+ ghc ↦ "IO ()";
+};
+...
+#+end_src
+
+The following Juvix examples are NOT valid.
+
+- One can not repeat backend inside a =compile= block.
+
+#+begin_src haskell
+...
+axiom Action : Type;
+compile Action {
+ ghc ↦ "IO ()";
+ ghc ↦ "IO ()";  --
+};
+...
+#+end_src
+
+- One name, one compile block, no more.
+
+#+begin_src haskell
+...
+axiom Action : Type;
+compile Action {
+ ghc ↦ "IO ()";
+};
+compile Action {
+ ghc ↦ "IO ()";
+};
+...
+#+end_src
+
+- A compile block must be in the same module as their name definition.
+
+#+begin_src haskell
+$ cat A.mjuvix
+...
+axiom Action : Type;
+...
+#+end_src
+
+#+begin_src haskell
+$ cat B.mjuvix
+...
+compile Action {
+ ghc ↦ "IO ()";
+};
+...
+#+end_src

docs/org/language-reference/foreign-blocks.org

@@ -1 +1,36 @@
 * Foreign blocks
+
+The =foreign= blocks give the developer the ability to introduce any piece of
+code in the compiled file. In addition, every foreign block specifies the
+backend's name that will include the given code in the body of the foreign
+block.
+
+The following is an example taken from the Juvix standard library.
+
+#+begin_example
+module Integers;
+
+axiom Int : Type;
+compile Int {  c ↦ "int" };
+
+foreign c {
+   bool lessThan(int l, int r) {
+     return l < r;
+   \}
+};
+
+inductive Bool {
+    true : Bool;
+    false : Bool;
+};
+
+infix 4 <';
+axiom <' : Int → Int → Bool;
+compile <' {
+  c ↦ "lessThan";
+};
+
+infix 4 <;
+< : Int → Int → Bool;
+< a b ≔ from-backend-bool (a <' b);
+#+end_example