summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a4b.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/3a4b.md')
-rw-r--r--content/zettel/3a4b.md13
1 files changed, 13 insertions, 0 deletions
diff --git a/content/zettel/3a4b.md b/content/zettel/3a4b.md
new file mode 100644
index 0000000..faa053d
--- /dev/null
+++ b/content/zettel/3a4b.md
@@ -0,0 +1,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.