fd3622a274
* add references to the syntax and cleanup code * [make] add .PHONY to Makefile targets * [parser] add parser / pretty for axiom backends * Pairing progress * [scoper] Add support for Axiom backends * [parser] Fix foreign block parsing * [ app ] adds --no-colors flag for the scope command * [ghc] upgrade to ghc 9.2.2 * use GHC2021 * [doc] Remove out-of-date comment * [test] Add ambiguity tests * [scoper] Improve resolution of local symbols * [error] WIP improving ambiguity error messages * [ clean-up ] new lab folder for experimentation * [ app ] ixes the lint warning * [ Termination ] removes Alga dependency * [error] Add message for ambiguous symbol error * [error] Add ambiguous module message * [scoper] Remove ErrGeneric * [test] Add test to suite * [test] show diff when ast's are different * [ lab ] folder organization * [ Makefile ] add targets with --watch option (stack cmds) and remove unused things * [ app ] add --version flag and fixed warnings and formatting * [test] remove fromRightIO to fix ambiguity error * [test] Add test of shadowing public open * [scoper] Add visibility annotation for Name * prepare buildIntoTable * [ Concrete ] add instance of hashable for refs. * add InfoTableBuilder effect * [ scoper ] add InfoTableBuilder effect * [ CHANGELOG ] updated v0.1.1 * [ README ] org version now * fix package.yaml * fix readme * [microjuvix] implement basic typechecker * add simple test for MicroJuvix type checker * fix checking for constructors apps in patterns * [scope] Move InfoTable to a new module * [abstract] Make Iden use references instead of Name * [abstract] Add InfoTable for abstract syntax * [scoper] Add function clauses to scoped InfoTable * [abstract] Add InfoTableBuilder for scoped to abstract * [main] Fix callsites of translateModule * [doc] Remove empty docs * [scoper] Update emptyInfoTable with missing field * rename some functions * [minihaskell] add compilation to MiniHaskell * [microjuvix] improve wrong type message * Add a validity predicate example written in MiniJuvix * [typecheck] Add error infrastructure for type errors Add a pretty error for mismatched constructor type in a pattern match * [test] Adds negative typecheck test for constructor * [app] Adds microjuvix subcommands for printing / typechecking * [typecheck] Add error message for ctor match args mistmatch * [typecheck] Add descriptive messages for remainng errors * [typecheck] Updates to error message copy * [typecheck] fix merge conflicts: * [highlight] add basic support for highlighting symbols * [minijuvix-mode] add minijuvix-mode and basic description in the readme * [readme] improve formatting * automatically detect the root of the project and add --show-root flag Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com> Co-authored-by: Paul Cadman <git@paulcadman.dev> Co-authored-by: Paul Cadman <pcadman@gmail.com> |
||
|---|---|---|
| .github/workflows | ||
| app | ||
| assets | ||
| lab | ||
| minijuvix-mode | ||
| minijuvix-stdlib@ad8392f76e | ||
| src/MiniJuvix | ||
| test | ||
| tests | ||
| .gitignore | ||
| .gitmodules | ||
| .hlint.yaml | ||
| CHANGELOG.org | ||
| hie.yaml | ||
| LICENSE | ||
| Makefile | ||
| package.yaml | ||
| README.org | ||
| stack.yaml | ||
MiniJuvix
<a href="https://github.com/heliaxdev/minijuvix/blob/main/LICENSE">
<img alt="LICENSE" src="
" />
</a>
<a href="https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml">
<img alt="CI status" src="
" />
</a>
Description
MiniJuvix is a dependently functional programming language for writing efficient formally-verified 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 Git from the Github repository. Then, the program can be downloaded and installed with the following commands. You will need to have installed Stack.
$ git clone https://github.com/heliaxdev/minijuvix.git
$ cd minijuvix
$ stack install
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 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 here.
- For Ubuntu :
It is required at least 8GB RAM for stack installation.
- To test everything works correctly, you can run the following command:
$ stack testEmacs 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:
(push "/path/to/minijuvix/minijuvix-mode/" load-path)
(require 'minijuvix-mode)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 Discord