Formalizing Coq extraction in Coq
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Authors:
  Bruno Barras (LIX - École Polytechnique),
  Stéphane Glondu (PPS - Université Paris Diderot),
  Pierre Letouzey (PPS - Université Paris Diderot)

Tested with Coq trunk r14626 (Oct 29, 2011, between v8.3 and v8.4) and
OCaml 3.12.1. To compile the whole Coq-in-Coq development, run:

  make

To compile the proof system based on extracted kernel and extraction,
run:

  make bcoq/bcoq

It can then be run with:

  ./bcoq/bcoq

Examples are given in bcoq/{prelude,examples}.v.

To compile the xcoq plugin based on the extracted kernel, run:

  make -C xcoq

Examples are given in xcoq/sandbox.v.

The file sandbox.el can give suggestions on how to run interactively
.v files inside Proof General (the version used for the development
was the CVS HEAD of July 29, 2011).

To pass the whole development through the standalone checker and make
a list of axioms, run:

  make axioms.txt

Axioms should be documented in proof scripts, so have a look at .v
files!

Directory layout:

  Library/      support libraries
  PtsMeta/      development on PTS with operators
  CicMeta/      development on CIC
  Extraction/   development on extraction
  bcoq/         proof system based on the extraction kernel
  xcoq/         Coq plugin running the extracted kernel

Directories Library, PtsMeta, CicMeta and bcoq are mostly Bruno
Barras's work, with tuning by Pierre Letouzey and heavy refactoring
(mostly to make it more friendly to interactive use) by
myself. Directories Extraction and xcoq are mostly my work.

 -- Stéphane Glondu <Stephane.Glondu@pps.jussieu.fr>  Fri, 18 Nov 2011 15:36:47 +0100
