A tiny language to explore efficient verified implementations of functional languages in Idris2.
We also include scripts to generate a reproducible artefact.
Please consult the following project to generate the base virtual box image required, and how we approach the building of the artefact.
https://github.com/jfdm/packer-idris
You will also need to have working installations of Katla to facilitate source code highlighting.
Once you have generated the image you can generate the artefact as follows:
SOURCE_VM="<location of the base ovf>" make artefact
This will generate in artefact
the following files:
velo.box
:: A Virtual Box virtual machine that contains Velo's source code & test suite;velo.tar.gz
:: A copy of Velo's source code, and generated IdrisDoc;velo_doc.tar.gz
:: A copy of the IdrisDoc for the coding project;velo_html.tar.gz
:: A copy of the katla generated html showing semantically highlighted code;velo.pdf
:: A copy of the submitted paper;