Skip to content

Commit

Permalink
v0.1.1 (#15)
Browse files Browse the repository at this point in the history
* 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

Co-authored-by: Jan Mas Rovira <[email protected]>
Co-authored-by: Paul Cadman <[email protected]>
  • Loading branch information
3 people authored Mar 25, 2022
1 parent 14ac284 commit de6fabf
Show file tree
Hide file tree
Showing 127 changed files with 3,473 additions and 2,986 deletions.
11 changes: 0 additions & 11 deletions CHANGELOG.md

This file was deleted.

16 changes: 16 additions & 0 deletions CHANGELOG.org
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
* Changelog

MiniJuvix uses [[https://pvp.haskell.org][PVP Versioning]]. The
changelog is available
[[https://github.com/heliaxdev/MiniJuvix/releases][on GitHub]].

** 0.1.1

- Add support in the parser/scoper for Axiom backends
- Add support for =foreign= keyword
- New flag =--no-colors= for the scope command
- Upgrade to GHC 9.2.2
- Improve resolution of local symbols in the scoper
- Several new tests related to ambiguous symbols
- Add =--version= flag
- Add InfoTableBuilder effect for the scoper
72 changes: 29 additions & 43 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,6 @@ PWD=$(CURDIR)
PREFIX="$(PWD)/.stack-work/prefix"
UNAME := $(shell uname)

AGDA_FILES := $(wildcard ./src/MiniJuvix/Syntax/*.agda)
GEN_HS := $(patsubst %.agda, %.hs, $(AGDA_FILES))

ifeq ($(UNAME), Darwin)
THREADS := $(shell sysctl -n hw.logicalcpu)
else ifeq ($(UNAME), Linux)
Expand Down Expand Up @@ -40,25 +37,17 @@ docs :
cd docs ; \
sh conv.sh

.PHONY : cabal
cabal :
cabal build all

.PHONY : stan
stan :
stan check --include --filter-all --directory=src

setup:
stack build --only-dependencies --jobs $(THREADS)

stack:
.PHONY : build
build:
stack build --fast --jobs $(THREADS)

stack-build-watch:
build-watch:
stack build --fast --file-watch

repl:
stack ghci MiniJuvix:lib

.PHONY : cabal
cabal :
cabal build all

clean:
cabal clean
Expand All @@ -67,31 +56,28 @@ clean:
clean-full:
stack clean --full

.PHONY : test
test:
stack test --fast --jobs $(THREADS)

.PHONY : test-watch
test-watch:
stack test --fast --jobs $(THREADS) --file-watch

format:
find ./src/ -name "*.hs" -exec ormolu --mode inplace {} --ghc-opt -XStandaloneDeriving --ghc-opt -XUnicodeSyntax --ghc-opt -XDerivingStrategies --ghc-opt -XMultiParamTypeClasses --ghc-opt -XTemplateHaskell \;
find . -path './src/**/*.hs' -or -path './app/**/*.hs' -exec ormolu --mode inplace {} --ghc-opt -XStandaloneDeriving --ghc-opt -XUnicodeSyntax --ghc-opt -XDerivingStrategies --ghc-opt -XMultiParamTypeClasses --ghc-opt -XTemplateHaskell \;

.PHONY : install
install:
stack install --fast --jobs $(THREADS)

.PHONY : install-watch
install-watch:
stack install --fast --jobs $(THREADS) --file-watch

repl:
stack ghci MiniJuvix:lib


prepare-push:
make checklines && make hlint && make format

.PHONY: install-agda
install-agda:
git clone https://github.com/agda/agda.git
cd agda
cabal update
cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' alex-3.2.6
cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' happy-1.19.12
pwd
cabal install --overwrite-policy=always --ghc-options='-O2 +RTS -M6G -RTS' -foptimise-heavily

.PHONY : install-agda2hs
install-agda2hs:
git clone https://github.com/agda/agda2hs.git
cd agda2hs && cabal new-install --overwrite-policy=always
mkdir -p .agda/
touch .agda/libraries
echo "agda2hs/agda2hs.agda-lib" > ~/.agda/libraries

.PHONY : agda
agda :
agda2hs ./src/MiniJuvix/Syntax/Core.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
agda2hs ./src/MiniJuvix/Syntax/Eval.agda -o src -XUnicodeSyntax -XStandaloneDeriving -XDerivingStrategies -XMultiParamTypeClasses
make checklines && make hlint && make format
63 changes: 63 additions & 0 deletions README.org
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
MiniJuvix
[[file:LICENSE][[[https://img.shields.io/badge/license-GPL--3.0--only-blue.svg]]]]
[[https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml][[[https://github.com/heliaxdev/MiniJuvix/actions/workflows/ci.yml/badge.svg?branch=qtt]]]]
====

** 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

** Community

We would love to hear what you think of MiniJuvix! Join us on
[[https://discord.gg/nsGaCZzJ][Discord]]
4 changes: 0 additions & 4 deletions agda-proofs/minijuvix-proofs.agda-lib

This file was deleted.

16 changes: 0 additions & 16 deletions agda-proofs/proofs/Algebra/Structures/StarSemiring.agda

This file was deleted.

6 changes: 0 additions & 6 deletions agda-proofs/proofs/Base.agda

This file was deleted.

Loading

0 comments on commit de6fabf

Please sign in to comment.