coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library
Date: Thu, 31 Oct 2019 15:17:22 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f172.google.com
Ironport-phdr: 9a23:mOifdxPrZ+et+GwFy6ol6mtUPXoX/o7sNwtQ0KIMzox0Iv35rarrMEGX3/hxlliBBdydt6sfzbOO7uu5AzRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfL1/IA+roQnNtsQajpZuJrgtxhDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuA+vqQJxw4DUY4+bOvRxcazfctwGSmRMRdpRWi9bD4+gc4cCAegMMOBFpIf9vVsOqh6+CBGyCePr0DhIg2H53asm0+s5Cw/G3RAgE8sQvXTQttr1KbodXv6xzKLVyjjMc+tW2Tbh6IfUdhAuu+yMUq9ufsrV0kQvGAbFgU+RqYzhJT+ayuMNs22C4udmSOmhhWknqwRrrTiuwMchkozJh4INylDA6CV5z4c1JduiREFheNKkEZ1dvDyZOYtuWs4uXX1ktSIgxrAFuZO3ZjUGxZU7yxLFdvCKcZaE7gr+WOqPIjp0nnxodK6lixu2/0Ws0OPxW8uy3V1XtCRKiMPMuWoI1xHL6siIVP99/kC51DaKzQ/T6+VELVktlarHNpIt27AwmocRvEjdBCP2l0L2jKiZdkUg5Oek8fjoYrLjppOENo90jB/xMrg2l8ChHeg1NhICUmub9OimybHu/FH1TK9XgvA0jKXVqJXaKt4apq69DQ9VyIEj6xOnAji6yNQYnGUHI05BeB2dkojmJk/BIPTjAPewhlSjijZrx/TcMrL9BZXNK2DPkK39crZl905c1A0zwMhD6JJTE7ENOe78WkvstNPDFRI5KAy1w+P/CNpnzI8eWGSPArWYMKzIq1OI6PgvcKGwY9oevy+4IPw47dbvi2U4kBkTZ/qHx5wSPVu8n/FrJVmuWXvwx/wFGHoGsw52GOfyiUGJVTdOa3u2d6057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXUSCu6R8C/Q/4JLRmqDIp5iDVdDOquToYg0Velswqok+M2fNqRwTURsNfY7PYw4uTSkR8o8jktVpaS1miMSyd/mWZaHmZrjpA6mlR0zxK46YY9g/FcEoYNtfZAUwN/LIKFiuIjVIq0VQXGcdOEDl2hR4f+DA==

On 2019-10-31 13:32, Matthieu Sozeau wrote:
> We do something like this in the MetaCoq project: using `Separate
> Extraction` or `Extraction Library` to extract module B, knowing that I
> have an mlpack implementing A on which B depends, and then calling `ocamlc
> -open Myplugin.A -I …/user-contrib/myplugin B.ml` to compile the «
> extension » code. With `Separate Extraction`, it’s a matter of removing all
> the generated code for `A` and its dependencies that is produced by
> extraction. With `Extraction Library` the user has to be careful that he
> extracts all the libraries he needs but doesn’t need . No unsafe type casts
> are inserted this way.

Hi Matthieu,

Thanks, that's very interesting feedback.
How do you handle dependencies on part of the standard library of Coq? Do you
make sure to include it all in the mlpack for A? More generally, how do you
distinguish between modules that you need to keep in B and modules that are
already in A?

Clément.

[Coq-Club] Separate/incremental extraction of parts of a Coq library, Clément Pit-Claudel, 10/30/2019
- Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Xavier Leroy, 10/30/2019
  - Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Clément Pit-Claudel, 10/30/2019
    - Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Xavier Leroy, 10/31/2019
  - Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Stefan Monnier, 10/30/2019
    - Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Erik Martin-Dorel, 10/30/2019
- Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Matthieu Sozeau, 10/31/2019
  - Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Clément Pit-Claudel, 10/31/2019
    - Re: [Coq-Club] Separate/incremental extraction of parts of a Coq library, Matthieu Sozeau, 10/31/2019