This is an experimental backend for Agda that targets the OCaml compiler.
This repo is a mirror (and a branch off of) the repo that was used during development. The original repo can be found here:
The major differece is the project structure. And the above repo also contains a report we wrote for the project.
The project layout is designed to mirror suitable locations in
You need to install
malfunction to get up and running. Please refer
to malfunction to see how to get this on your system.
This project has been tested using
stack. Building should be as easy as:
ln -s stack-8.0.2.yaml stack.yaml stack build
stack exec agda-ocaml
stack install agda-ocaml
stack exec agda-ocaml-bench
The benchmarks depend on agda-prelude - so download that and add it to your default libraries.