juvix/README.org

* MiniJuvix

#+begin_html
<a href="https://github.com/heliaxdev/minijuvix/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/heliaxdev/MiniJuvix/actions/workflows/ci.yml">
<img alt="CI status" src="https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml/badge.svg" />
</a>
#+end_html


** Description

MiniJuvix is a dependently functional programming language for writing
efficient formally-verified
[[https://anoma.network/blog/validity-predicates/][validity
predicates]], which can be deployed to various distributed ledgers. This
is a software released for experimentation and research purposes only.
No warranty is provided or implied.

MiniJuvix addresses many issues that we have experienced while trying to
write and deploy decentralised applications present in the ecosystem of
smart-contracts:

- the difficulty of adequate program verification,
- the ceiling of compositional complexity,
- the illegibility of execution costs, and
- the lock-in to particular backends.

** Quick Start

To install MiniJuvix, you can download its sources using
[[http://git-scm.com/][Git]] from the
[[https://github.com/anoma/juvix.git][Github repository]]. Then, the
program can be downloaded and installed with the following commands. You
will need to have installed [[https://haskellstack.org][Stack]].

#+begin_src shell
   $ git clone https://github.com/heliaxdev/minijuvix.git
   $ cd minijuvix
   $ stack install
#+end_src

If the installation succeeds, you must be able to run the =minijuvix=
command from any location. To get the complete list of commands, please
run =minijuvix --help=.

- How to install [[https://haskellstack.org][Stack]]:? if it's not
  installed.

  - For Ubuntu : =apt install stack=
  - For Debian : =apt install haskell-stack=
  - For Arch Linux : =pacman -S stack=
  - For macOS : =brew install haskell-stack=
  - For Windows, following the instructions
    [[https://docs.haskellstack.org/en/stable/install_and_upgrade/#windows][here]].

It is required at least 8GB RAM for =stack= installation.

- To test everything works correctly, you can run the following command:

#+begin_src shell
  $ stack test
#+end_src

** Emacs mode
  There is an emacs mode available for MiniJuvix. Currently it supports syntax
  highlighting for well-scoped modules. It is a work in progress.

  To install it add the following lines to your emacs configuration file:
  #+begin_src elisp
  (push "/path/to/minijuvix/minijuvix-mode/" load-path)
  (require 'minijuvix-mode)
  #+end_src
  Also, =minijuvix= must be installed in your =PATH=.

  The MiniJuvix major mode will be activated automatically for =.mjuvix= files.
*** Keybindings

  | Key       | Function Name    | Description                                           |
  |-----------+------------------+-------------------------------------------------------|
  | =C-c C-l= | =minijuvix-load= | Runs the scoper and adds semantic syntax highlighting |

** Community

We would love to hear what you think of MiniJuvix! Join us on
[[https://discord.gg/nsGaCZzJ][Discord]]