Commit 3963d3d8 authored by Danil's avatar Danil

Update readme

parent 603dced9
Pipeline #20004 failed with stage
in 10 minutes and 17 seconds
......@@ -19,7 +19,6 @@ Then MetaCoq and bignums:
```bash
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-metacoq.1.0~alpha+8.11
opam install coq-bignums
```
And std++:
......@@ -29,6 +28,8 @@ opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-stdpp
```
Install MetaCoq from this [MetaCoq's fork](https://github.com/annenkov/template-coq/tree/coq-8.11-erase-annotated). Follow the instructions from the [official MetaCoq repo](https://github.com/MetaCoq/metacoq#installing-from-github-repository-for-developers).
After completing the procedures above, run `make` to build the development, and
`make html` to build the documentation. The documentation will be located in the
docs folder after `make html`.
......@@ -40,7 +41,7 @@ The [embedding](embedding/) folder contains the development of the embedding.
The [execution](execution/) folder contains the formalization of the smart
contract execution layer, which allows reasoning about interacting contracts.
The [extraction](extraction/) folder contains a printing procedure for the deep embedding into the Liquidity syntax. For extraction using MetaCoq's **certified erasure** see the [extract-cert](https://github.com/AU-COBRA/ConCert/tree/extract-cert) branch (requires [MetaCoq's fork](https://github.com/annenkov/template-coq) to compile).
The [extraction](extraction/) folder contains two versions of extraction. The first one is a printing procedure from the deep embedding into the Liquidity syntax. The second one is based on MetaCoq's **certified erasure**.
## Notes for developers
......
# Extraction prototype
# Extraction
A prototype implementation of the extraction procedure from the deep embedding (essentially, just by printing). Currently, implements simplistic extraction to Liquidity. We also try to set use the standard Coq extraction to OCaml as a substitute for the Liquidity extraction, since the two languages are very close syntactically.
Contains two implementations:
* pretty-printing procedure from the deep embedding into the Liquidity syntax. Smart contracts have to be written in ``λsmart`` using the notations.
* extraction using MetaCoq's certified erasure. Extracts smart contracts impelemted in Gallina. Can handle some form of dependent types. Currently supports Liquidity as a target language.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment