The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

We are pleased to announce version 1.0 of UniCoq.  In essence, UniCoq
is a plugin that, upon request, replaces the current unification
algorithm for Coq with our own.

A question that many of you are probably thinking right now is: why
would anyone want to do this?  We believe that the current algorithm
suffers from two main issues: it lacks proper documentation of the
heuristics incorporated in it, and it includes certain heuristics that
are problematic.  UniCoq is our solution to these two issues.

We invite the members of this community to read the accompanying
paper, carefully documenting with examples the many features of the
algorithm [1] (an extended version of [2]).  We also recommend giving
UniCoq a try, which can be easily installed via Opam (see [3]).

We welcome any bug or enhancement report.  We must be honest and say
upfront that the algorithm's performance is poorer w.r.t. the current
algorithm in Coq (*). We plan to take performance seriously as soon as
we feel we are certain that the algorithm is not missing any critical
component. For the moment, the algorithm is coded as close as possible
to the mathematical description given in [1].

Best regards,
Beta and Matthieu

[1] A Comprehensible Guide to a New Unifier for CIC Including Universe
Polymorphism and Overloading.
B. Ziliani, M. Sozeau
Under submission.
http://www.mpi-sws.org/~beta/papers/unicoq-journal.pdf

[2] A Unification Algorithm for Coq Featuring Universe Polymorphism
and Overloading.
B. Ziliani, M. Sozeau
In International Conference of Functional Programming (ICFP 2015).
http://www.mpi-sws.org/~beta/papers/unif.pdf

[3] http://github.com/unicoq/unicoq/

(*) Compiling the entire Mathcomp library currently takes about 20%
more time with UniCoq.