coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Petar Maksimovic <petar.maksimovic AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Speeding up inversion on large inductives
- Date: Thu, 10 Sep 2015 11:56:22 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=petar.maksimovic AT gmail.com; spf=Pass smtp.mailfrom=petar.maksimovic AT gmail.com; spf=None smtp.helo=postmaster AT mail-la0-f42.google.com
- Ironport-phdr: 9a23:GK4pZxcXPuRPnCmISdTLK7uXlGMj4u6mDksu8pMizoh2WeGdxc6+ZB7h7PlgxGXEQZ/co6odzbGG7+a5BSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTrkbnus7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDOC+nIGGkAfkQFJBg/b7RqyCo/8riLg8O902zKbOMroTLscVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy
Hi Michael and Pierre,
Actually, it was impossible to put all the Derive Inversion principles
in one file, the compilation would never have finished (at least on my
machine). There are 18 separate files, each holding ~25 Derive
Inversions, and each, when compiled, being of a size of around 450mb.
Cheers,
Petar
On 10 September 2015 at 11:47, Pierre Courtieu
<pierre.courtieu AT gmail.com>
wrote:
> 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
- [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/07/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/08/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Xavier Leroy, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
- RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Pierre Courtieu, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Enrico Tassi, 09/10/2015
- RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
- RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Robbert Krebbers, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Thomas Braibant, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/11/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Alan Schmitt, 09/15/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Thomas Braibant, 09/10/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Xavier Leroy, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Vladimir Voevodsky, 09/09/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/08/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/09/2015
Archive powered by MHonArc 2.6.18.