coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Xavier Leroy <xavier.leroy AT college-de-france.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] extract CompCert dependend type
- Date: Fri, 5 Apr 2019 15:41:26 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xavier.leroy AT college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy AT college-de-france.fr; spf=None smtp.helo=postmaster AT smtpout10.partage.renater.fr
On Thu, Apr 4, 2019 at 1:54 PM Fritjof Bornebusch <fritjof AT uni-bremen.de> wrote:
If I extract it to Integer, I got all the additional definitions, like wordsize, add, add_overflow, etc:
https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v.
Does someone know, why these additional definitions are also being extracted? I replaced all definitions I need,
such as *mul* or *divu* with the operations of the target language, Haskell in this case. None of the above
are called explicitly in my code.
In many cases Coq's extraction is able to eliminate definitions that are not referenced. However, in your particular case (application of a parameterized module), I'm afraid extraction is unable to remove those definitions.
Hope this helps,
- Xavier Leroy
regards,
--f.
- [Coq-Club] extract CompCert dependend type, Fritjof Bornebusch, 04/04/2019
- Re: [Coq-Club] extract CompCert dependend type, Xavier Leroy, 04/05/2019
Archive powered by MHonArc 2.6.18.