The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

>Because otherwise, according to the semantics of “Require Import”, the size 
of vo of a top level function with very deep nesting of sub function calls will 
be very large.

Require Import shouldn't change vo size by much, are you sure this is the 
problem?

Gaëtan Gilbert

On 18/01/2021 13:29, 刘坚 wrote:
> Hi all,
>
> Currently we are developing a formal verification tool based on coq.
>
> Here is the background:
>
> There exist many .v files for a project, one for each C function. So when we 
> were generating proof of a C function, it is reasonably needed to “Require 
> Import” all proofs of its calling functions.
>
> Suppose that: each proof script contains both the definition of a C function 
> and the definition of its proof term.
>
> The problem is that: in practice, when we are “Require Import”ing a proof, 
> all we want to import is the proof term defined, not the C function 
> definition. Because otherwise, according to the semantics of “Require 
> Import”, the size of vo of a top level function with very deep nesting of sub 
> function calls will be very large. We want to import the necessary constants 
> only.
>
> Here is the question:
>
> Is there any way to import constants in an selective way? If not, could you 
> please introduce me some materials about the libobject module in the src of 
> coq? Because I am currently reading the source code but got stuck on this 
> module. As far as I know, it will be very helpful to understand libobject 
> before I can solve my problem.
>
> Could you please give me some suggestions?
>
> Thank you!
>
> Best,
> Jian