summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a4b.md
blob: faa053d7d0095e159e223ad315d488b7405d65d8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
+++
title = "Compiling CompCert as an external library"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a4a"]
forwardlinks = []
zettelid = "3a4b"
+++

This is fine when only using the CompCert proofs. However, when
extending CompCert, the OCaml files are also needed, which are normally
not available after the CompCert development is installed.