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 23:31:56 -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-f178.google.com
  • Ironport-phdr: 9a23:TAgG4RPG48uxaZX/Q+gl6mtUPXoX/o7sNwtQ0KIMzox0Ivz8rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzYHPbYGJN/dzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cMI+JYqJP4p1QQqxu+GRGjCvnuyj9Un3P7w6k63P48EQ7bwgMgG88FvXPIo9XtNacSTfy6zK3SwjXecvxZxzP95ZPHchAku/6MXLZwfdDNxkkoEgPIl1OdopHmMTONzukBrXSX4u56We+si2MrsR99riWuy8s2l4XEhIEYxkja+Sh43Io5ONi1RFN4bNOrFZZduDyWOohqTs4nQmxluTg1x78DtJO4fCUHx5QqyhvRa/GJcoWF5hfuWeiPLTd2mX1ofbKyiwio/kWizOD3S9O630xQriVfl9nBrnAN2ALX6siAUvZ9+12u2TeL1wzK8+FEPVw4mbPVK5I8wLM9lYAfsUvEHi/xl0X2iLGZel849eiv7uTrerTmppmCOI9okgzyLLgil8ilDek7MgUCRXaX9fm92bH54EH0QrZHguUzkqbDsZDaIcobprS+Aw9Qyoss9w6/Dza60NsEmXkINk9Fdw+ZgIjtIFzOL/X4Au2+g1Soijtk2/fGPrj5DpXXMnfDiKvhfap660NE1AUzyslf64tIBbEFPfL8QVT8tMfYDx88Kwy72fzrCNR71oMEWGKAGLWVMK3IsQzA2uV6KO6VIYQRpTzVKv4/5veog2Vqt0UaePyC2RoSZXakKcxnPwCyZXPxjtoFWTMBpgsiR+jjlVGPVRZcYn+zW+Q34TRtW9HuNpvKWo342O/J5yy8BJADPjkXWGDJKm/hcsC/Y9lJbSuTJsF7lTldDOquToYg0VelswqokuM7fNqRwTURsNfY7PYw//fazEhg+jl9DsDb2GaIHTktwzE4AgQu1aU6mnRTj1eO1a8i3a5dHN1XoupVCkI0bMGMieN9DN/2V0TKedLbEFs=

On 2018-04-27 19:59, Jim Fehrle wrote:
>> fortunately, my VST proof development is itself much more efficient, so
>>therefore I can do big things with a large collection of .v files that 
>>/each/ take no more than 1 gigabyte (and usually much less) to process with
>>coqc.
>
> Sounds like a memory leak.

1GB actually sounds like a very typical memory footprint for a large Coq
proof, in my experience. It's not uncommon to grow to 10 or 15GB for larger
ones.



Archive powered by MHonArc 2.6.18.

Top of Page