The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Coq is much more complicated for a number of reasons. For one thing, it contains an evaluation strategy that is highly parametrisable. It is clever and efficient (and weighs already about 700loc). It has powerful mutually inductive type families with a non-trivial positivity condition (about 1000loc). It has a feature-rich module system (that's pretty hard, though it only seem to weigh about 500loc). Other things I fail to mention.

Also, I'm not really familiar with the implementation of Idris, but I suspect that termination checking (and positivity) are not included in the core checker.

Coq has a checker of compiled file (source in checker/) whose implementation of the kernel is about 7000 lines of code (including the code to read the the compiled files). It's less efficient than the actual kernel (20,000 lines of code), which, among other things, has an implementation of a virtual machine for (much) more efficient conversion checking.

Coq has a fairly small kernel, all things considered, but it is bigger than it strictly needs to, for efficiency reason.

On 8 September 2013 16:18, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

I'm not very familiar with the Coq implementation, so I won't comment
on that, but I would like to point out that your link to Idris
verifier is very incomplete. TT.hs defines the formal language of the
kernel (in around 950 lines), but does not implement its verifier,
which should rather be found at:
  https://github.com/edwinb/Idris-dev/blob/master/src/Core/Typecheck.hs
(around 200 lines)
  which depends on
  https://github.com/edwinb/Idris-dev/blob/master/src/Core/Evaluate.hs
(around 800 lines)

The Matita team wrote an article about a compact implementation of a
kernel for CiC, that could be a basis for comparison (and details the
design choices and architecture). "A compact kernel for the calculus
of inductive constructions", by Asperti, Ricciotti, Sacerdoti Coen and
Tassi, in 2009. It says the whole implementation is around 2300 lines,
which is in the same ballpark.

On Sun, Sep 8, 2013 at 1:31 PM, t x <txrev319 AT gmail.com> wrote:
> As a followup to this thread:
> https://sympa.inria.fr/sympa/arc/coq-club/2013-05/msg00071.html
>
> I recently installed the Idris language, and was pleasantly surprised to
> find that it's core verifier is only 1000 LOC:
> https://github.com/edwinb/Idris-dev/blob/a76627e7a62cd0816001017439523d491c4c9e8d/src/Core/TT.hs
>
> In Coq, is there is a corresponding *.ml file that does the checking when I
> type in "Qed." ?
> (and if not, is there some toy project that implements a minimal verifier?)
>
> I'm not looking for unification / inference / notation / ltac. Nor am I
> interested in various proofs -- just the very core "dumb/minimal" verifier
> that verifiers the terms generated.
>
> Thanks!