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,13 +1,11 @@
 * 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]]
@@ -15,28 +13,28 @@
   - [[./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/examples/validity-predicates/README.org

@@ -1 +0,0 @@
-* Validity predicates

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/introduction/about/what-is.org

@@ -1,48 +0,0 @@
-* Juvix
-
-#+begin_html
-<a href="https://github.com/anoma/juvix/actions/workflows/ci.yml">
-<img alt="CI status" src="https://github.com/anoma/juvix/actions/workflows/ci.yml/badge.svg" />
-</a>
-#+end_html
-
-#+begin_html
-<a href="https://github.com/anoma/juvix/tags">
-<img alt="" src="https://img.shields.io/github/v/release/anoma/juvix?include_prereleases" />
-</a>
-#+end_html
-
-#+begin_html
-<a href="https://github.com/anoma/juvix/blob/main/LICENSE">
-<img alt="LICENSE" src="https://img.shields.io/badge/license-GPL--3.0--only-blue.svg" />
-</a>
-#+end_html
-
-#+begin_html
-<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img
-src="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment/badge.svg"
-alt="pages-build-deployment" /></a>
-#+end_html
-
-#+begin_html
-<a href="https://github.com/anoma/juvix">
-<img align="right" width="300" height="300" alt="Juvix Mascot" src="../assets/seating-mascot.051c86a.svg" />
-</a>
-#+end_html
-
-
-Juvix is a research programming language created by [[https://heliax.dev/][Heliax]] as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages. The Juvix language is constantly evolving, open-source, functional, and statically typed with special support for compiling [[https://anoma.network/blog/validity-predicates/][validity predicates]] to the =C= language, which can be deployed to various distributed ledgers including [[https://anoma.net/][Anoma]].
-
-The Juvix programming language allows developers to write programs with a high degree of assurance that they will meet specific standards. This is due to the fact that several static analyses are performed during compilation, including, for example, scope, termination, arity, and type checking. As a result, functional programs, especially validity predicates, can be written with greater confidence that they will be free of runtime errors. [[https://github.com/anoma/juvix/tree/main/examples/milestone][Here are some examples of Juvix programs]].
-
-The language features:
-
-- [X] Unicode syntax
-- [X] parametric polymorphism
-- [X] inductive and parametric data types
-- [X] higher-order functions
-- [X] implicit arguments
-- [X] holes in programs
-- [X] 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 icludes our [[https://anoma.github.io/juvix/introduction/changelog.html][latest updates]].

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

docs/org/language-reference/inductive-data-types.org

@@ -1 +1,57 @@
 * Inductive data types
+
+The =inductive= keyword is reserved for declaring inductive data types. An
+inductive type declaration requires a unique name for its type and its
+constructors, functions for building its terms. Constructors can be used as
+normal identifiers and also in patterns. As shown later, one can also provide
+type parameters to widen the family of inductive types one can define in Juvix.
+
+The simplest inductive type is the =Empty= type with no constructors.
+
+#+begin_example
+inductive Empty {};
+#+end_example
+
+In the following example, we declare the inductive type =Nat=, the unary
+representation of natural numbers. This type comes with two data constructors,
+namely =zero= and =suc=. A term of the type =Nat= is the number one, represented
+by =suc zero= or the number two represented by =suc (suc zero)=, etc.
+
+#+begin_example
+inductive Nat {
+    zero : Nat;
+    suc : Nat → Nat;
+};
+#+end_example
+
+The way to use inductive types is by declaring functions by pattern matching.
+Let us define, for example, the function for adding two natural numbers.
+
+#+begin_src text
+inifl 6 +;
++ : Nat → Nat → Nat;
++ zero b ≔ b;
++ (suc a) b ≔ suc (a + b);
+#+end_src
+
+As mentioned earlier, an inductive type may have type parameters. The canonical
+example is the polymorphic type =List=. The type =List=s the inductive type that
+considers the type of the elements in the list as a parameter. A constructor to
+build the empty list, that is the base case, and another constructor to enlarge
+the list, we usually called it =cons=. One possible definition for this type is
+the following type taken from the Juvix standard library:
+
+#+begin_example
+infixr 5 ∷;
+inductive List (A : Type) {
+  nil : List A;
+  ∷ : A → List A → List A;
+};
+
+elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
+elem _ _ nil ≔ false;
+elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs;
+#+end_example
+
+To see more examples of inductive types and how to use them, please check out
+[[https://anoma.github.io/juvix-stdlib/][the Juvix standard library]]

docs/org/language-reference/modules.org

@@ -1 +1,173 @@
 * Module system
+
+** Defining a module
+
+A module is of the following form. The =module= keyword stars the declaration of
+a module followed by its name and its body. The module declaration ends after
+seeing the =end= keyword.
+
+#+begin_example
+-- ModuleName.juvix
+module ModuleName;
+
+end;
+#+end_example
+
+A _Juvix project_ is a collection of Juvix modules inside one main project
+folder containing a metadata file named =juvix.yaml=. Each Juvix file has to
+define a _module_ of the same name. The name of the module must coincide with
+the path of the its file respect to its project. For example, if the file is
+=root/Data/List.juvix= then the module must be called =Data.List=, assumming
+=root= is the project's folder.
+
+To check that Juvix is correctly detecting your project's root, one can run the
+command =juvix internal root File.juvix=.
+
+# - Inside a module, other (sub) modules can be declared.
+
+# #+begin_example
+# -- Example.juvix
+# module Example;
+#     module A;
+#     end;
+# end;
+# #+end_example
+
+** Importing modules
+
+To bring into the current scope all module definitions from other external
+modules, one can use the =import= keyword along with the corresponding module
+name. This way, one gets all the imported names qualified.
+
+#+begin_example
+-- A.juvix
+module A;
+   axiom Nat : Type;
+   axiom zero : Nat;
+end;
+
+-- B.juvix
+module B;
+    import A;
+    x : A.Nat;
+    x := A.zero;
+#+end_example
+
+Additionally, one can _open_ an imported module making available all its
+names by their unqualified name.
+
+#+begin_example
+-- A.juvix
+module A;
+   axiom Nat : Type;
+   axiom zero : Nat;
+end;
+
+-- B.juvix
+module B;
+    import A;
+    open A;
+    x : Nat;
+    x := zero;
+#+end_example
+
+However, opening modules may create name collisions if you already have the
+imported names as definitions in the current module. In this case, Juvix will
+complain with an error, letting you know which symbols are ambiguous. For
+example, in module =B= below, the name =a= is ambiguous.
+
+#+begin_example
+-- A.juvix
+module A;
+axiom A : Type;
+axiom a : A;
+end;
+
+-- B.juvix
+module B;
+import A;
+open A;
+axiom a : A;
+
+x := a;
+end;
+#+end_example
+
+One alternative here is hiding the name =a= as follows.
+
+#+begin_example
+-- B.juvix
+module B;
+import A;
+open A hiding {a};
+
+axiom a : A;
+x := a;
+
+end;
+#+end_example
+
+Now, we can use the =open import= syntax to simplify the =import-open= statements.
+
+Instead of having:
+
+#+begin_example
+import Prelude;
+open Prelude;
+#+end_example
+
+We simplify it by the expression:
+
+#+begin_example
+open import Prelude;
+#+end_example
+
+The =hiding= keyword can be used within an =open-import= statement.
+
+#+begin_example
+-- B.juvix
+module A;
+open import A hiding {a};
+axiom a : A;
+x := a;
+end;
+#+end_example
+
+** Exporting symbols
+
+The module =C= below does not typecheck. Both symbols, originally defined in
+module =A=, are not visible in module =C= after importing =B=. The symbols =A=
+and =a= are not exported by the module =B=. To export symbols from an imported
+module, one can use the =public= keyword at the end of the corresponing =open=
+statement. For example, in module =B=, after marking the import of =A= as
+=public=, the module =C= typechecks.
+
+#+begin_example
+-- A.juvix
+module A;
+axiom A : Type;
+axiom a : A;
+end;
+
+-- B.juvix
+module B;
+open import A;
+end;
+
+-- C.juvix
+module C;
+open import B;
+
+x : A;
+x := a;
+end;
+#+end_example
+
+Fix:
+
+#+begin_example
+-- B.juvix
+module B;
+open import A public;
+end;
+#+end_example

docs/org/language-reference/termination-checking.org

@@ -1,26 +1,26 @@
-* Termination checking
+* Termination
 
 To not bring inconsistencies by function declarations, Juvix
-requires that all function pass the termination checker.
-This check is called before the typechecking in the compilation pipeline.
+requires that every function passes its termination checker.
+However, since this is a strong requirement, often tricky to fulfill,
+we give the user the possibility to skip this check in two different ways:
 
-
-Since the former requirement is vital but often tricky to fulfill for programs
-in a total language like Juvix. It is convenient to have
-a way to bypass the termination checking. The user may be certain  their
-programs are terminating even when our termination checker algorithm can not
-see it. The termination checker is limited as it only accepts a subset
-of recursion functions. Our termination checker algorithm is a slightly modification
-of the algorithm for checking terminationg of the Foetus's language.
-
-
-To skip the termination checker, we introduced  the =terminating= keyword
-to annotate a type signature as terminating. The syntax is the following.
+- Using the =terminating= keyword to annotate function type signatures as terminating. The syntax is the following.
 
 #+begin_example
 terminating fun : A → B;
 #+end_example
 
-Annotating a function as =terminating= means that /all/ its function clauses pass the termination
-checker's criterion. To skip the termination checker for mutual recursive functions, all the functions
-involved must be annotated as =terminating=, otherwise, the checker will complain.
+Note that annotating a function as =terminating= means that /all/ its function
+clauses pass the termination checker's criterion. To skip the termination
+checker for mutual recursive functions, all the functions involved must be
+annotated as =terminating=.
+
+- Using the CLI global flag =--no=terminating=.
+
+
+#+begin_example
+juvix typecheck --no-termination MyProgram.juvix
+#+end_example
+
+In any case, be aware that our termination checker is limited as it only accepts a subset of recursion functions. The termination checker algorithm is a slightly modification of the algorithm for checking termination in the Foetus's language.

docs/org/tooling/CLI.org

@@ -27,14 +27,27 @@ juvix [Global options]  ((-v|--version) | --show-root | COMMAND)
   Only print errors in a uniform format (used by
                           juvix-mode)
 
-** Commands
+** Main Commands
+
+- =html=
+  Generate HTML output from a Juvix file
+
+- =typecheck=
+  Typecheck a Juvix file
+
+- =compile=
+  Compile a Juvix file
+
+** Internal Commands
+
+#+begin_src shell
+juvix internal COMMAND
+#+end_src
 
 - =parse=
   Parse a Juvix file
 - =scope=
   Parse and scope a Juvix file
-- =html=
-  Generate HTML for a Juvix file
 - =termination=
   Subcommands related to termination checking
 - =monojuvix=
@@ -45,9 +58,6 @@ juvix [Global options]  ((-v|--version) | --show-root | COMMAND)
   Translate a Juvix file to MiniHaskell
 - =minic=
   Translate a Juvix file to MiniC
-- =highlight=
-  Highlight a Juvix file
-
 
 ** CLI Auto-completion Scripts
 

docs/org/tooling/emacs-mode.org

@@ -11,7 +11,7 @@ To install it add the following lines to your Emacs configuration file:
 (require 'juvix-mode)
 #+end_src
 
-Make sure that =juvix= is installed in your =PATH=.
+Make sure that Juvix is installed in your =PATH=.
 
 The Juvix major mode will be activated automatically for =.juvix= files.