0ac9eb1ab4
A lambda:
```
\ { v0 := b0 ; v1 := b1 ; ... ; vn := bn }
```
should be translated to:
```
λ? (λ? ... (λ? (match ?$0, ?$1, ... , ?$n with ...)))
```
i.e the de Brujin index of the values in the match always start from 0.
Fixes: https://github.com/anoma/juvix/issues/1695
|
||
|---|---|---|
| .github | ||
| app | ||
| assets | ||
| bench | ||
| c-runtime | ||
| docker | ||
| docs/org | ||
| examples/milestone | ||
| gnuplot | ||
| juvix-mode | ||
| juvix-stdlib@ec28dc811e | ||
| licenses | ||
| runtime | ||
| src/Juvix | ||
| test | ||
| tests | ||
| .clang-format | ||
| .github_changelog_generator | ||
| .gitignore | ||
| .gitmodules | ||
| .hlint.yaml | ||
| .pre-commit-config.yaml | ||
| .pre-commit-hooks.yaml | ||
| book.toml | ||
| cabal.hie.yaml | ||
| cabal.project | ||
| changelog.org | ||
| LICENSE | ||
| Makefile | ||
| package.yaml | ||
| README.org | ||
| stack.hie.yaml | ||
| stack.yaml | ||
Juvix
<a href="https://github.com/anoma/juvix/actions/workflows/ci.yml">
<img alt="CI status" src="
" />
</a>
<a href="https://github.com/anoma/juvix/actions/workflows/pages/pages-build-deployment"><img
src="
"
alt="pages-build-deployment" /></a>
<a href="https://github.com/anoma/juvix/tags"> <img alt="" src="https://img.shields.io/github/v/release/anoma/juvix?include_prereleases" /> </a>
<a href="https://github.com/anoma/juvix/blob/main/LICENSE">
<img alt="LICENSE" src="
" />
</a>
<a href="https://github.com/anoma/juvix"> <img align="right" width="300" height="300" alt="Juvix Mascot" src="assets/seating-mascot.051c86a.svg" /> </a>
Description
Juvix is a research programming language created by 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 validity predicates to the C language, which can be deployed to various distributed ledgers including Anoma.
The Juvix language and related tools are documented in the Juvix book. To write
and test Juvix programs, you can use your favorite text editor and the juvix
command line tool. However, we recommend using the juvix-mode in Emacs or the
plugin in VSCode.
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.
- HelloWorld.juvix
- Fibonacci.juvix
- Hanoi.juvix
- PascalsTriangle.juvix
- Collatz.juvix
- TicTacToe.juvix
- SimpleFungibleToken.juvix
The 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 Homebrew.
To install the homebrew-juvix tap, run:
brew tap anoma/juvixTo install Juvix, run:
brew install juvixHelpful information on the shell can also be obtained by running:
brew info juvixLinux x86_64
A Juvix compiler binary executable for Linux x86_64 is available on the 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:
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/juvixBuilding Juvix from source
To install Juvix from source you must clone the Github repository. Then Juvix can be installed with the following commands. We assume you have Stack installed.
git clone --recursive https://github.com/anoma/juvix.git
cd juvix
stack install
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.
brew install --build-from-source --HEAD juvix --verboseQuick Start
After installation run juvix --help to see the list of commands available. See
CLI usage examples for descriptions of common tasks.
Run Juvix doctor to check your system setup:
juvix doctorThe Hello World example
This is the Juvix source code of the traditional Hello World program.
-- HelloWorld.juvix
module HelloWorld;
open import Stdlib.Prelude;
main : IO;
main := putStrLn "hello world!";
end;
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:
juvix compile HelloWorld.juvix
./HelloWorld
You should see the output: hello world!
The source code can also be compiled to a WebAssembly binary. This requires some
additional setup. See Installing dependencies in the documentation for more
information. You can also run juvix doctor to check your setup.
juvix compile --target wasm HelloWorld.juvix
wasmer HelloWorld.wasmLSP support
We provide a sammple hie.yaml configuration file for both cabal and stack.
If you prefer stack, run:
cp stack.hie.yaml hie.yamlIf you prefer cabal, run:
cp cabal.hie.yaml hie.yaml
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 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, the Juvix
standard library's website. For futher details, please refer to
the Juvix book which includes our
latest updates.
Coming soon
For the language:
- tail call optimization
- compilation to circuits
- coverage checking (i.e. exhaustiveness and useless clauses)
For the compiler:
- Init command
- Better documentation tool:
juvix doc MyFile.juvix
Community
Join us on our Discord server
This project is part of a bigger effort called Anoma. Anoma is a suite of protocols and mechqanisms for self-contained, self-sovereign coordination. Join the Anoma project.