diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-09-19 02:41:24 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-09-19 02:41:24 +0100 |
| commit | a2abe3182242953ba5dff5500399def0682fa10e (patch) | |
| tree | 16716ae6fe38e449c4602e8713dfe7d2860875d0 | |
| parent | 8d74fffc72abb3cc20df691d9d40c73fbd1c0c27 (diff) | |
| download | vericert-docs-a2abe3182242953ba5dff5500399def0682fa10e.tar.gz vericert-docs-a2abe3182242953ba5dff5500399def0682fa10e.zip | |
Add headers
| -rw-r--r-- | documentation.org | 5 | ||||
| -rw-r--r-- | setup.org | 5 |
2 files changed, 7 insertions, 3 deletions
diff --git a/documentation.org b/documentation.org index 13b99f0..7503fd5 100644 --- a/documentation.org +++ b/documentation.org @@ -30,10 +30,10 @@ following C features are supported, but are not all proven correct yet: ** Papers - OOPSLA '21 :: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal - Verification of High-Level Synthesis. In /Proc. ACM Program. Lang./ 5, OOPSLA, 2021. [[[/papers/fvhls_oopsla21.pdf][pdf]]] + Verification of High-Level Synthesis. In /Proc. ACM Program. Lang./ 5, OOPSLA, 2021. [{{{link([[/papers/fvhls_oopsla21.pdf][pdf]],[[./static/papers/fvhls_oopsla21.pdf][pdf]])}}}] - LATTE '21 :: Yann Herklotz and John Wickerson. High-level synthesis tools should be proven - correct. In /Workshop on Languages, Tools, and Techniques for Accelerator Design/, 2021. [[[/papers/hlsspc_latte2021.pdf][pdf]]] + correct. In /Workshop on Languages, Tools, and Techniques for Accelerator Design/, 2021. [{{{link([[/papers/hlsspc_latte2021.pdf][pdf]],[[./static/papers/hlsspc_latte2021.pdf][pdf]])}}}] * Index :PROPERTIES: @@ -82,7 +82,6 @@ compiled and executed. The dependencies of this project are the following: - [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool. - [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files. -- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library. - [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. - [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml. @@ -2,3 +2,8 @@ #+hugo_section: ./ #+macro: link src_emacs-lisp[:results raw]{(ymhg/link "$1" "$2")} +#+macro: texinfo_head (eval (if (eq org-export-current-backend 'texinfo) "#+exclude_tags: noexport_texinfo" "")) +#+macro: latex_head (eval (if (eq org-export-current-backend 'latex) "#+exclude_tags: noexport_latex" "")) + +{{{texinfo_head}}} +{{{latex_head}}} |