Coq plugin for plain dependency extraction
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
.travis-ci.sh
.travis.yml
Depends.v
LICENSE
Makefile
README.md
_CoqProject
depends.ml4
depends.mlpack
descr
opam

README.md

Depends Coq Plugin

Build Status

A Coq plugin for non-recursive extraction of dependencies of terms as globally unique kernel names, derived from coq-dpdgraph.

Requirements

Installation

The easiest way to install the plugin is via OPAM:

opam repo add proofengineering-dev http://opam-dev.proofengineering.org
opam install coq-depends

To build the plugin manually, run make in the root directory. Then, to install it, run make install.

Usage Examples

(* require and import plugin *)
Require Import Depends.Depends.

(* constants to analyze *)
Require Import List.

(* print dependencies as JSON for constants *)
Depends map filter.

(* write dependencies to file as JSON for constants *)
Depends "deps.json" map filter.

(* show dependencies as JSON for the types of constants *)
TypeDepends map filter.

(* write dependencies to file as JSON for the type of constants *)
TypeDepends "typedeps.json" map filter.

(* show dependencies as JSON of all constants in given modules *)
ModuleDepends Logic List.

(* write dependencies as JSON to file for all constants in given modules *)
ModuleDepends "deps.json" Logic List.