coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute
Date: Sun, 28 Jan 2018 13:47:21 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 9.mo1.mail-out.ovh.net
Ironport-phdr: 9a23:SNg4sxedGad+pZWth8XPAdhMlGMj4u6mDksu8pMizoh2WeGdxcuyZB7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37X/ZisJwgqxYrhyuqRNwzIzIb4+aL/d+YqDQcMkGSWZdUMtcVSpMCZ68YYsVCOoBOP5VoY7nqFoBrBu+ABejD/7hxDhSgH/xxLY62PkmHAHDxgMgHtYOvW/RrNrvO6YSUOW1w7fVwjrdafNZxyz95JLGchA7uPyBW697f8TWyUkqDQzFj1OQpJTkPzOTzOQNsnKU4/BuVeK1k2InpABxoiSvxscxkYbFnJ4aylfB9Sh/3Y07JsW4RVZmbdOmE5ZcrS+XO5VsTs8/X21luzw2xqAEtJKlZCQHxpYqywTCZ/GFfYWE+A/vWeKeLDtimn5odqyzihCv+ka60OL8TNO70FNSoypFjNbMsncN2gTX58SdT/t9+Vqt1SyK1w/J6+FEJVk4la3GK5492LIwkYQTsUTZEi/whkr2kLeadkQi+ue29+Tqeqjqq52fOoNuhAzyLL4iltGjDek7KAQCQmqW9fqk2L3m50L5QbFKjvMskqnetZDXPcEbqbS4Aw9RyYsj7gywDjin0NQdg3YIMUxKeBSZgIjyIV3OLur4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDGmIG+qSNL7YmV6O/OMmZeeWN6EPvzOoDvE15vvjxVO4n98GNf2s1JoTQHWxDvVjLkmUZ3f3xNkbRzRZ9jEiRfDn3QXRGQVYYGy/Cvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPz4UD1mcEHLle4iCVuxKZjjAe5Y9wAxBbqCoTsoa7T/rrBXzkuQ1K+PE+ygVuZ/l2cMz6feBzUhvpwwxNNyU1iS2d08xnm4MQGVqjvE5pEskjFKK0Kw9hOFEU9tN57VPXxtobZM=

Hi,

On 01/28/2018 01:04 PM, Merlin Göttlinger wrote:
> It the term I run my function on contains a nat which is given as a
> Section Parameter native_compute takes a few seconds and then fails with
> Warning: Native compiler exited with status 127
> [native-compiler-failed,native-compiler]
> Error: Anomaly "Compilation failure."
> Please report at http://coq.inria.fr/bugs/.
>

This looks very much like a native_compute bug. Would you mind opening a
bug report at https://github.com/coq/coq/issues with an example test
case? I'll fix the bug.

Thank you!

Maxime.

[Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Merlin Göttlinger, 01/28/2018
- Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Matthieu Sozeau, 01/28/2018
  - Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Merlin Göttlinger, 01/28/2018
    - Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Maxime Dénès, 01/28/2018
- Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Gaëtan Gilbert, 01/28/2018
  - Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Merlin Göttlinger, 01/28/2018