/tacengine

My unfinished and unpolished reflection on designing and implementing a tactic engine

Primary LanguageTeX

Inside the design of a tactic system

Arnaud Spiwack

Abstract

In this article, I started reflecting on my experience designing and implementing a new tactic engine for the Coq proof assistant. Unfortunately I have not finished it and other things took priority. I'm making it available as is hoping it may still contain some useful thoughts.

Sources

Building instructions

To build the article, you need to have a Latex distribution installed, as well as Ocaml (version 3.12 or later) and the melt text processing tool. The command line to run is ocamlbuild tacengine.pdf. You can then find the pdf file in _build/tacengine.pdf

License

The content of this repository is distributed under Creative Commons licence CC BY 3.0.