coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Typechecker is running for 20 minutes, with 100% cpu and without any output

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Typechecker is running for 20 minutes, with 100% cpu and without any output
Date: Fri, 22 Oct 2021 15:49:13 +1100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f54.google.com
Ironport-hdrordr: A9a23:N8EhM6j41/pXlXG0qgCtdJ38x3BQXuMji2hC6mlwRA09TyVXra+TdZUgpHrJYVkqMk3I9ersBEDEexLhHP1OkOss1NWZMjUO0VHAROpfBMnZowEIcBeOldK1oJ0QCpSWf+eAa2SS4/yX3ODBKadG/DDRytHNudvj
Ironport-phdr: A9a23:SoYYhRaEP30bB7xDzbO0O9X/LTHn0IqcDmcuAnoPtbtCf+yZ8oj4OwSHvLMx1gePDNyQtq0MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YHfbx9MiTagbr9/LBe7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+TbxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8qVlRwLyiCofODE38G/ZhM9tgqxFvB2svBl/z5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5u5b4sSDOoOI/1Yr4ngrFsSrBu/CxOjBPnuyjRVgXL22LA60+c/HgHd3AwgA9MOsXrOo9XvNaceS+G1zKjJzTXfavNbwjj96I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1qfp5D/MTyPyuQNr3aU7/BmVe+3lmIrtwF/rDexy8oxiofEiIIYx0zZ+Shnw4s7Jdm1RVNnbNO4H5Vdti+XOpVyT84iXm1mtyk0x7wYtZOlciYEyJIqzAPRZfyAdoiH+BPjVOCJLDd3hXJlZLK/hwup/kS61uL8Ucy03VBXpSRGitnBrm4B2wDX58SdSfZw/l2t1SiT2w3Q8O1JIU85mKzGIJA72LEwjIAcsUHbEy/2hkr2iKiWe10h+uey6uTnZqzqqYGBOINpkw3+PKQjl8OlDeQ3NQgOWGeb+eCi27H54UL5R7BKguU3kqnfrp/aOdwWqrClDwJRyIou6BayAy243NgEnnQLNlJIdR2fg4jsIV7OIfT4Dfmlg1SrlTdm3/XGPqDiAprTNXjDkKvhfbdz6kFG0gozzMpT55NVCrEAPPLzX1T8tNPdDhAjMgy0x/zrB8l61oMbQW6PGLOWMLvOsV+U4eIiO/WDZIgMuDrkN/cl4+PugmQilF8Gfaip2IMXZ2qiEvRnJUWZe3vsjc0bHWcEpAptBNDt3VaFSHtYY2u4d6M6/DAyToy8XqnZQYX4haGC0Ty7VoFXeWlcCxjYFGrrep6ER/YTYTiTZM5gkyABfbekQo4lkxqpsVmpmPJcMuPI93hA5trY399v6riL/fnX3TNxBsWZlWqKSjMs9ovnbzAz1aF750d6zwXauUCZq/lRFNgW6v8QFwlnadjTyOt1D920UQXELI/hdQ==

I am encoding Sha256 but the typechecker can't get past this Defined [1], it's running
for more than 20 minutes on my system (sorry, I don't have a small example and it requires coq-color library [3]). Can someone tell me what is wrong with the W function [2]?

(base) ➜ ~ coqtop -v
The Coq Proof Assistant, version 8.13.2 (August 2021)
compiled on Aug 31 2021 6:26:53 with OCaml 4.09.1
(base) ➜ ~

Best,

Mukesh

[1] https://gist.github.com/mukeshtiwari/fd5abb764a0de870f2cb00b275a017af#file-sha256-v-L725

[2] https://gist.github.com/mukeshtiwari/fd5abb764a0de870f2cb00b275a017af#file-sha256-v-L694

[3] https://github.com/fblanqui/color

Attachment: Screen Shot 2021-10-22 at 3.39.39 pm.png
Description: PNG image

[Coq-Club] Typechecker is running for 20 minutes, with 100% cpu and without any output, mukesh tiwari, 10/22/2021