mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
f2cc163998
Once this PR is merged, Github codespaces will be available, facilitating contributions from all kinds. - Juvix Haskell Project CodeSpace [![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=102404734&machine=standardLinux32gb&location=WestEurope) - Juvix Standard Library CodeSpace [![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?hide_repo_select=true&ref=main&repo=455254004) Note that the change here to REAMDE.org only adds a badge that opens the Juvix Standard Lib Open Spaces. Such an environment quickly loads the Juvix binary, examples from anoma/juvix/examples, and all the files from the Standard library. One needs more than 15 GB of memory RAM and more than 15 GB of storage to load the Juvix Haskell project properly. These are requirements that are not included in the free plan offered with GitHub Codespace.
229 lines
8.4 KiB
Org Mode
229 lines
8.4 KiB
Org Mode
* 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/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/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/codespaces/new?hide_repo_select=true&ref=main&repo=455254004">
|
|
<img height="20pt" alt="Open the Juvix Standard Lib in Github Codespace" src="https://github.com/codespaces/badge.svg" />
|
|
</a>
|
|
#+end_html
|
|
|
|
#+begin_html
|
|
<a href="https://github.com/anoma/juvix">
|
|
<img align="right" width="300" height="300" alt="Juvix Mascot" src="assets/images/tara-seating.svg" />
|
|
</a>
|
|
#+end_html
|
|
|
|
|
|
** Description
|
|
|
|
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 language and related tools are documented in [[https://anoma.github.io/juvix/][the Juvix book]]. To write
|
|
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]]
|
|
|
|
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=.
|
|
|
|
** 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.
|
|
|
|
Some of the language features in Juvix include:
|
|
|
|
- unicode syntax
|
|
- parametric polymorphism
|
|
- inductive and parametric data types
|
|
- higher-order functions
|
|
- implicit arguments
|
|
- 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]].
|
|
|
|
|
|
** Community
|
|
|
|
Join us on our [[https://discord.gg/waYhQ2Qr][Discord server]]
|
|
|
|
This project is part of a bigger effort called [[https://anoma.net/][Anoma]].
|
|
Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination.
|
|
Join the [[https://anoma.net/community][Anoma project]].
|