coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "dapoignyrichard AT yahoo.fr" <dapoignyrichard AT yahoo.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with last version of CoqHammer
- Date: Thu, 8 Sep 2022 09:13:03 +0000 (UTC)
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dapoignyrichard AT yahoo.fr; spf=Pass smtp.mailfrom=dapoignyrichard AT yahoo.fr; spf=None smtp.helo=postmaster AT sonic304-21.consmr.mail.ir2.yahoo.com
- Ironport-data: A9a23:mZaC9a8w8RXoxxKH1yXrDrUDHHiTJUtcMsCJ2f8bNWPcYEJGY0x3y TQdWmjXP//bNDP0Ltkjadyz9kgHvJ7cmNRhQQFvqiFEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9i6mJUqYLhWVnV6 Iui+5S31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z0 98W9qCtTAUSA4rrs7UGQR9jOgtiIvgTkFPHCSDXXc271ErAcnC3m6krVhhwNooe4eNtR2RH9 PheKSpXKAGKh+Wxhrm8T4GAhOx8c4+xZ9NZ4y4xi2iFU57KQribK0nOzdNRxDAxicZfB/fVZ 8MDZRJ+ZRTHZFtBID/7Dbpkx7743iihIlW0rnq0/YZn8XHY5TBIk4a0bsrbIdy0b+FayxPwS mXupD6lW01AaLRz0wGt+XW1w+TLgCnTQ5MXDLT+9/hwgVTVyHZ7NfENfUC8p/iy0RbiHogGb UcT/DErt+43/U2vCNjnBVupqX6DuVgXXN84//AGBB+l0aCPoDqEA2o/cxlmQ409pskNbBY2y Qrc9z/2PgBHvLqQQHOb076bqzKuJCQYRVPugwdbE2PpBPG8/ukOYgLzosVLTfXu1YKlcd3k6 3XU9nVv393/mOZRj82GEUb7byWEh7WhouQdyhjdWmOjhu+STKL9PeREBXD/4PdGN5qUVDG8U JUsgM+Y7etVVc3IznXLS+ILB7SzofOMMTmagEQ1WYgo9zOqvXWkeOi8AQ2Sxm82Yq7omhezO ic/XD+9ArcOZRNGiocqOeqM5zwCl/SIKDgcfqm8giBySpZwbhSb2ypleFSd2Wvg+GB1z/9lZ MjGLZ32UipHYUiC8NZQb7lCuVPM7n5urV4/ubiip/ha+eHFOy/PIVv7GAfeNIjVE59oUC2Oq YoGa5HWo/muePz3Yi7QuMYOLhgRIGIlBJv7sIRTd+uCPgdqcFzN+NeOqY7Nj7dNxvwP/s+Rp i/VchYBlDLX2CObQS3XNSgLQO21Af5X8ylgVQRyZgbA5pTWSdzwhEvpX8BnI+dPGS0K5aIcc sTpjO3cUq8RG22cq2t1gFuUhNUKSSlHTDmmZ0KNCAXTtbY7L+AQ0tO7LAbp6gcUCS+76Zk3r 7G6hlHKSJoEQEJsFp+OOv6oylqwu1kbmf5zDxeTe4YLJB20/dg4MTH1g982P9oIdUfJyAyc2 lvEGhwfv+TM/9I4/YCR16CJpoukCcVkGU9eEzWJ5Lq6L3mI72OjxogGXvzRJWLRU2b9+aODY +RJzqGga6RYxAoS64clSuRl16Mz4dfrtoR29AU8ESWZdUmvB5NhPmKCgZtFuJpLy+ILogCxQ E+OpoRXNLjVasPoFFkdeFgsYuiZjq5GgT7U7P9ueBm/vnYx972BSkBIeRyFiSgbLaEvdpIsw eAm/sUR7lXn2BYtN9+HiAFS9niNcS1YD/167MlCDd+5kBcvx3FDfYfYVX377ZSJXNNGbRsnL zqSs6zdiukO3UHFaXcySSPA0LYPn5gIoxwWnlYOK07SxYjegfk210YJrXFtF0JeyRNc1vg1P 2FqMwt0P//I7j5og88FVGepQlkTCBqc80336l0IiGyGHhH0DjGXdDUwabSX4UQU02NAZTwEr ryVzWDSVzy1Lsz82y0FX1Fo9q74Rttr+wyew82qEqxpxXXhjeYJX0NvWYYJl/cjKdg2gkzM/ rE2ubwpL6b8MzUVues+Aoiek7UKElaVLWxFRrdq+6Zh8aQwvt2t8WDmFqxzUpolyz/2HYuQG sVuIcUJWQ7WOOOmsGUAHaBVS1NrtKdB2TfBE48H4UYXuruYqXxnqvo8M8Q4aHADG71TrCr2F m8dm/9u3IBdabu4VlIhdPV5B1c=
- Ironport-hdrordr: A9a23:pMckK6vm0YIqylhwkSKLRhiP7skDv9V00zEX/kB9WHVpW+afkN 2jm+le8BPyhisRMUtQ4exoWZPwJ080kKQf3WB/B9mftWXd2VdAabsSj7cKoAeQfBEWlNQttp uIGpIWYLLN5BpB/KPHCWKDYrIdKbe8kJxA/d2utktFfEVRTYZBxUNVKCa+VndXai4uP/AEPa vZ3MxBpzDlXVt/VKiG7i1sZYX+m+E=
- Ironport-phdr: A9a23:v7eILxF+Dwy0v+hn4vTXh51GfyRGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmSBd+QsqkMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9GiTahf79+I wi6oAvMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9 LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyJPDIOiY YUMDeUBM/tWoIbhqFUJthaxHxWgC/j0xTJSmnP736s32PkhHwHc2wwgGsoDvHrJo9rvLKcSV uG1zKbOzTTDdfNW2Cvy6IjSfRA7vP6BRrJxftDRyUkoEAPJlFuQqZbrMziI0ekCrnKU7/JnV eKuhG4nrQFwoiKuxsgwionGnJgVxU3f+CR52ok1Jdq4SElhbd6qCptdrieXPJZ5Tc0+WW9no jo6yqEYtp6heigH0JoqygPRZvCaboSF4hLtWeWNLTpmh39oZK+yiRiy/EWh1ODyVsm53llXo idZktTBqmwB2hzS58WESvZw41qt1zaJ2gvO6e9EOVg5mKjZJpI73LI9mJkevV7eEiL0nEj6l rKae0ol9+Wu9u/peK/ppoWGOI9xkgz+Mrohmsi4AekgKQgOWG6b+eWg27Dt4UH0T6xGguMrn qXDrJ/aIsIbprW8Aw9PyIoj7gywDzai0NgCnHkHNkxJdAiHjofzO1HOJ/f4Ae2jjFSrlTdn3 /HGPrv/DZXRNnXOkrXscaxj50NSywc/181T6pBQB70bPf7+VU78uMTdDhAjMgy0x+jnCM961 oMbQW+AH7WWMLvVsV+J6eIvJemNZJUUuDnhK/gq/eTugmIilF4dZ6ap3ZwXaHeiEvRoOUWVe XzsjcwZHmcQogU+VPDqiEGFUTNLenq+R7g86S0jCIK6EYfDQZigj6CG3CeiB5FZemRGCk2XH nrzbIWFW/IMaDqILcN7kzwEU6KhS4472h20ug/60ekvEu2B0SoB/bnnydI9s+bUjFQ58SF+J 8WbyWCECW9uyDAmXTgziepzqFR6y1iFwLJ5iPxRD9B79vpJVQB8O4SWh7h2Asj1Ww3Hb82IQ 1avWNmOEDgxSdV3zcVYMBU1IMmrkh2Wh3niOLQSjbHeQcVsqso0vlD0Lsd5kDPd0bU5ykIhW o1JPHGngah2807SAZTImgOXjfXibrwSiQjK8mrL1m+SpAdASgclXazdWnEQYFrMrN/571nOZ 66nCbMgdAVbmoaZMqUfUtTylh1dQev7ftHXYma/gWC1UBqB3rSNY4z7YWQW3CzHBGAVmgAU+ jCIL1t2HT+v9kTZCjEmDlfzewXs/O15/Wu8VVMxxhqWYldJzL2z+xVO3aDZEapV1bUCoyI77 TB9HVL73siMTcuJpw1mOq5bZLvR+X9h0mTU/0x4N52kdOV5g0IGNh9wpwXo3gl2DYNJlY4rq mkrxUx8M/DQ1lQJbD6e0Z3qX9+fYmDv4BCibbLX0VDCwZ6X/KkI8vExt1TkukmgCEMj93xt1 9Qd3WGb493GCw8bUJS5VUhSlVAyq7jCZSgy4ZLO1HZsOLO4mi7L29UuQuU/i16hc9pZLKKYB VrqCcRJYqrmYOcumlWvclcFJLUNq+huZJPgLqTXnvf3YrUF/nrul2lM7YFj31jZ8iN9TrWNx JMZ27SD2RPBUT7gjVCnu8SxmIZeZDhUEHDsrEqsTINXeKB2ep4GTGm0JMjijNl3n5nsVHhJ7 l+oB1oc1Oe4cBqVaBrzx0cDsCZf6Wzigia+wzFuxnslp7KY3SPI0v7jfxoOIGJjVWBiilCqL 5L+3LV4FAC4KgMukhWi/0PzwaNW8b9+I2fkSkBNZyHqLmtmX8Ncr5K6atVUoNMtuCRTC6GnZ EyCD6X6u10c2j/iGG1XwHY6cSurs9P3hU4yhGWYJXd15H3XHKM4jRvW/NvdSvhAxDsNRCBih RHGD1i7OJ+n552YmozCvea3S2+6HsIMN3OwncXZ63r9vDE0SRSk+pL70sXqCw07zTP225FxW CPEoQy9Kojn2qKmMP52K0xhBVvy8c1/SeQc2sM7gJAd32Rfh43AoiVByzyjd4wEiOSnMCReI FxDi8TY6wXkxkB5e3eAxoaiE26Y3tMkfN6iJGUfxiM66clOTqaS9r1N2yVv8T/a5UrcZ+Zwm jAFxL4g8nkf1qsFsRIqzyqbE6oTFklRJyDEhh2I6Nf4or8dNwPNOfCgkVFzm9ysFuTIrghEX 3f2fIY4HCRw599zGEPF0Hr0rI/+Moq1D5pbpliflBHOiPJQIZQ6m68RhCZpDmn6uGUs1+8xi RE9lYH/poWMLH9hub6oGhMNfCOgfNsdo3u+6MQW1tbTxY2kGY9tXykGTIe9B+z9Cyoc7Lz/K xzcATQ8rXDdEr3aVReD8hV3pnLIFNatOm3fc3AdyZ8KqAC1AktZjUhUWTw7msV8DQW23In6d 18/4DkN51n+ox8Ky+RyNhC5XH2N7AGvIiw5TpSSNn80pklL+lvVPMqC7+lyAzAQ/5uvqxaII 3CaYAIABH8AW0iNDVTudre04tyI/++dD+u4Z/zABNfG4fRZTOuNzImz35FO5DGKN87UZiUnV aR90U1FRnVjXcHQmjFJSjZN0TPEb8mc4hy7/2wSzIj38fjmXh7u+ZraC7ZWNoYn8BS3jKGfc u+I0Xkmb2wDhtVVmi6OkeRBjztww2l0ejKgEKoNr3vIRaPUwepMCgIDLjh0LI1O5r492Q9EP YjajMn03/h2lK1QaR8NWFr/l8WufcFPLXu6MQaNCE+TM7WJIyzRwsr3aLmwYaxZjOJT8ROq8 2X+cQerLnGYmj/lWgr6e/lLlz2eNQdCtZuVaRFrCGO4FI6jMET9O9hxljgsh7g9h3eMNHRGd yl1c0RK6LaX6GkL55c3U3wE5X1jI+6eni+f5OSNMZcav8xgBSFsnv5b6nA3o1O6xDBNRPty3 iXI/IcGS7SOg+CPzT0hXgAc8l6jZaqQukNjMv6BqtwaADDP+xQW6H/WDh0Lo51kEIepqqlQz d+Jn6X2em8qzg==
- Ironport-sdr: kNzertgCVrAGYSJU1Mr7ccz5RfOlo+vZm/F4RuG2OrQ50Ij/KdZqboa3cUMiBjBUuVNeN7j2zL 7LCE1k4zuY35D1XWf7tS9lu+jOPE0kMgLLdqfLCxS0UAnfPLdy3IBh4Wp524IV0HudKJpY3ywp kFSr2r9lUuk0KQ6z1jUrQlfZyck5+d1cKYNh/o1oGMAnh85bb+N588/2JYOZVnQhCCAHfPSgoK CiziPr44kH6qyO4iWkbIzrlQWQKlCBxOeXojkQWYMvw600enybhuZVvVfkYM6Qaz6ukBlF/VKk Ctv5bZ/MVvfMbcHorD3areU/
Yes, i notice that it is a bit slower, essentially for big theorems. Btw, some lemmas that i have not be able to prove in an earlier version are now proved (e.g., with Eprover). Perhaps it results from some improvement in the software?
Thanks for your concern.
Le jeudi 8 septembre 2022 à 08:07:13 UTC+2, Łukasz Czajka <lukaszcz AT mimuw.edu.pl> a écrit :
> - srun eauto use: indeed gives a syntax error whatever the version of
> Coq (I've just tested this with Coq 8.12-8.15 and an appropriate
> CoqHammer for each of these versions).
>
> - However, sauto use: does exist. I haven't been able to test your
> particular example since you didn't give specific instructions to
> reproduce it, but I suggest that you try that instead.
> Coq (I've just tested this with Coq 8.12-8.15 and an appropriate
> CoqHammer for each of these versions).
>
> - However, sauto use: does exist. I haven't been able to test your
> particular example since you didn't give specific instructions to
> reproduce it, but I suggest that you try that instead.
"sauto use:" should be able to do almost anything "srun eauto use:"
can, but may be slower.
It seems something must've changed in Coq parsing in earlier Coq
versions before 8.12 and I didn't notice.
I'll look into this once I find some time in my busy schedule.
- [Coq-Club] Problem with last version of CoqHammer, dapoignyrichard AT yahoo.fr, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, Théo Zimmermann, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, dapoignyrichard AT yahoo.fr, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, Łukasz Czajka, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, dapoignyrichard AT yahoo.fr, 09/08/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, Théo Zimmermann, 09/07/2022
Archive powered by MHonArc 2.6.19+.