The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Michael, I am not sure why -dont-load-proof is slow, but keep in mind that:

1) the statement itself is rather big, and the file is probably
*huge*, even without loading proofs, in may take a while to parse,
even partially, because of its size.

2) "Derive Inversion foo with bar." Does not give a clue on the type
of the generated principle foo. Only after type-checking the generated
term do we know its type. This explains why the v8.5 "lazy"
computation of proofs does not work in this case: the strategy
consisting in only reading the statement and postponing the proofs
cannot be used there: there is no statement. Hence the hackish
copy-paste of the statements as axioms so that the depedency with the
file containing the Derive Inversion is forgotten.

P.




2015-09-10 11:19 GMT+02:00 Soegtrop, Michael 
<michael.soegtrop AT intel.com>:
> Dear Coq Users,
>
> I was following this discussion and I think there is one implied question 
> in the original post which hasn't been answered as yet: Petar wrote that he 
> used coqc with -dont-load-proofs and it still made a speed difference 
> between defining the inversions rules as axioms and deriving them. I 
> thought that the difference between ending a proof with Qed and Defined is 
> that in the first case the proof term remains opaque and only the 
> information that the proof exists may be used in further steps, but not the 
> proof term as such. So I don't understand why the speed difference between 
> axioms and opaque proofs exists and would very much appreciate if someone 
> could explain why this is.
>
> In Coq 8.5 I got the impression that proof terms are not loaded unless 
> really used e.g. in a Print. A Print of an imported proof results in a 
> message that an opaque proof term has been loaded from a library. Also the 
> background proof mechanism of CoqIDE makes the user believe that Coq 8.5 
> can handle opaque proofs.
>
> Finally I wonder what effect it would have to put the proofs into a module 
> and then remove the proof terms by opaque signature ascription. In my 
> experience this makes the proofs more opaque than Qed does, e.g. they are 
> no longer accessible to Print. Would it still be required to load the proof 
> terms when such an opaque module is loaded from a library?
>
> Best regards,
>
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
> Chairperson of the Supervisory Board: Tiffany Doon Silva
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928