Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit


Chronological Thread 
  • From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] speed of Coq 8.8 vs 8.7, 32-bit vs 64-bit
  • Date: Fri, 27 Apr 2018 18:40:39 -0400
  • Authentication-results: mail3-smtp-sop.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-qt0-f196.google.com
  • Ironport-phdr: 9a23:CwYILhCNs3tqk+1y0cVTUyQJP3N1i/DPJgcQr6AfoPdwSPv+pMbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJKiA38G/XhMJzgqxUrh2uqB5jzIDbe4yVKPlzc7nBcd8GS2dMXMBcXDFBDIOmaIsPCvIMMPhcr47nolsBsx2+BRW0C+31yz9Immb60LM+0+s7DAHJwRIvH9YTu3nTsNr1LKYSUfypw6nM1zrDcu5Z1in56IXTfRAhpOuDXbN0ccbL1UYvEAbFg0yWpIf4PD2VzvwAv3aH4+dkT+6iiG4qpxtvrjSyx8ogkJTFi4YUx1zc6Cl0w5w5KcO5RUJhf9KoCoZcuz+UOoZwX8gsWXtnuDwgxb0DoZO7fDYFyJAgxxPHbvyIaYmI4hb6WOaIPTd0mGtpeLyiixu28EWs0OL8Vs6z0FZFqipKjMPAuWwK1xzW8sSHS/198Vm92TuXyQzf9uVJLVo3mKfbMZIt3KM8m5sJvUjeGiL7mV36jKqMeUUl/uio5f7nYrLjppKEK4B0kgD+Mrgylcy7G+s4LxUBUHaf+emn273j+Ff2QLROjvEsjqbZt5XaKdwBpqGlGw9Vzpoj6xGnAji619QYhGALI05BeBKalIfkIErOIfD9DfenmVugijZrx/bcPr3gGJrBNHbDkK2yNYp6vkVb0U84yc1Vz5NSELAIZvzpCWHrs9mNJRu4NgGy39HfCck4/YcXRG6CBufNO7vTrVSM7/8jLu2ka4ocuTK7IP8gsa29xUQlkEMQKPH6laAcb2q1S6w/chepJEH0i9JEKl8k+w83TejkklqHCGcBaHO7XqZ67TY+Wtv/UdXzA7u1ibnE5x+VW4VMbzkfWF+JGHbsMY6DXqVUMX/AEopaijUBEIOZZcoh2BWp7lGozrNmKq/N5nVdu8uyip564OrckRx0/jtxXZyQ
Hi Andrew,

On 2018-04-26 14:57, Andrew Appel wrote:
> Of course, the same proof script would take exactly twice as much memory in
> 64-bit mode, because every pointer is twice as big.

I'm not too familiar with OCaml's encoding of inductive types, but surely
it's not all pointers, right? How can teh proof script take "exactly twice as
much" memory in 64-bits mode?

Clément.

Archive powered by MHonArc 2.6.18.

Top of Page