Skip to content
This repository has been archived by the owner on Mar 26, 2023. It is now read-only.
/ typed-extraction Public archive

Verified coq extraction

License

Notifications You must be signed in to change notification settings

AU-COBRA/typed-extraction

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

This repo is now merged into MetaCoq

The typed-extraction library is now part of MetaCoq.

typed-extraction

Extraction of types, certifying transformations (eta, inlining), type annotations, the dearg optimization and corresponding proofs. The repository is an intermediate step towards moving this functionality to MetaCoq.

Builds with Coq 8.14-8.16 and MetaCoq 1.1.1

How to build

Our development works with Coq 8.16 and depends on MetaCoq and coq-equations. The dependencies can be installed through opam.

To set up a switch with the necessary dependencies run the following commands from the root of the project:

opam switch create . 4.10.2 --repositories default,coq-released=https://coq.inria.fr/opam/released --deps-only
eval $(opam env)

If Coq 8.16 is already installed, run

opam repo add coq-released https://coq.inria.fr/opam/released
opam install ./coq-concert.opam --deps-only

After completing the procedures above, run make to build the development.