coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Łukasz Czajka <lukaszcz AT mimuw.edu.pl>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with last version of CoqHammer
- Date: Wed, 7 Sep 2022 19:38:50 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lukaszcz AT mimuw.edu.pl; spf=Pass smtp.mailfrom=lukaszczz AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg1-f171.google.com
- Ironport-data: A9a23:kBv/qqnAi12hwIU7ksYuAYbo5gytIERdPkR7XQ2eYbSJt1+Wr1Gzt xIbW2CBPqrfZDf8f9ggaoSw8kkDv5aAyYRnQVA+/Hs9QVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09UAbeSRWVvX4 4uj+5KHZDdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1GnLKrQCkSOZbQgcgdDhdyTBldNv1JreqvzXiX6aR/zmXDenrohu1hVQQ4ZNJBvOlwBm5K+ LoTLzVlghKr3brnhuLmDLM124J6c5CD0IA34hmMyRndEPUvWoLIUbfi6tpR3TN2jcdLdRrbT 5dANms/MUiQC/FJEnQKVMphkLrwvVbEUD9qtFiapacswFGGmWSd15C0aIaPEjCQfu1emV/dr Wbb9UziExQCPZqezyCE+zSinIfycTjTXYsTEPig+acvjgTMnyocDxoZUVb9qv684qKjZz5BA 0c91DEng5M1z1CyYtmgUTfnmF2P7hFJDrK8DNYGwA2Kz6PV5SOQCW4FUiNNZbQaWCkeFW1CO rihz4OBONB/jFGGYSnCqerM/FteLQBQfDBSP3ZVJecQy4C7+Nlbs/7Zcjp0/EeIYjDdHDjxx 3WSo3F7iexM1IgE0KK0+V2BiDWpznQocuLXzlWJNo5GxlkhDGJAW2BOwQaBhRqnBNjAJmRtR FBex6CjABkmVPlhbhClTuQXB62O7P2YKjDailMHN8B/qW7xqy/7J94JvmsWyKJV3iAsKW6Bj Kj76VM52XOvFCbCgVJfON/pU5x3lcAM6/y8Dq+OMLKinaSdhCfepH00DaJh92/ql0conMkC1 WSzIK6R4YIhIf0/llKeHr9DuZdyn3xW7T6NGPjTkkv/uZLAPiL9YeleazOmMLtphJ5oVS2Pr L6zwePRm0sBOAA/CwGLmbMuwacidiljXMut9ZQOL4Zu4GNOQQkcNhMY+pt5E6QNokifvr6gE qiVVhAKxVzhq2fALAnWOHlvZKm+D5l6pHM/eycrOA/wiXQkZI+u6oYZdoc2LeF3rrw9kaYsQ qlXYdiED9ROVi/DpGYQYJz7m4poK0amiAeICCy6bWVtZJVnXQHIpoTpc1K3pikDBya6r+Ukp Lik2l+JSJYPXV04XsPXbe+wiV69oD4FnLsqDUfPJ9BSfmTq8ZRrdHyh36FufZlUJEyalDWA1 guQDRMJnsX3otc4oIvTmKSJj4a1CO8iTEBUKHbWsOStPi7A82v9nYIZCLSUfSrQXX/f8bm5Y bkH1On1NfAKkQoYs4d4FLo3n6sy68G1++1fxwVgWW3ENhGlU+w5ZHaB2sZLu+tGwboA4Vm6X UeG+997P7SVOZO6TARAelJ9NunTh+sJnjTy7OguJBmo7iFA+rfaA15ZOAOBiXAAIbYpYpkpx /wt5Jwf5wCl0EZ4N9+HimVM+D3JICVfCuMosZYVBIKtgQ0ukwkQbZvZAy7wwZeOd9QcbRVwc 2HM3PLP1+ZG207PU3svDnyRj+BTspID5UJRx1gYKlXVx9fIi5fbBvGKHejbmuiU8vlG7w63E m1iNkkwParXujkx25EFUGerFAVMQhae/yQdDrfPeHLxFyGVuq7ldQXR+tphOGgW9mtden5Q+ 7TwJKPNT2PxZM+otsctcRcNlhEgJOCdMiXHmcW6AIKIE4R8eT6NbmpCo4YXg0OPPP7dT3Era QWnECicpEE72eMtT3UHNrSn
- Ironport-hdrordr: A9a23:IAGgfKrZFEdASsvcfFQgOvsaV5ooeYIsimQD101hICG9E/bo8f xG885rtyMc5AxhO03I3OrhBEDiex3hHPxOkOws1N6ZNWGMhILrFuBfBODZslnd8kPFh4lgPG RbHpSWyuebMbG3t6rHCcCDfOod/A==
- Ironport-phdr: A9a23:Z+VcYhSDOt05LKTjHDHMMdu5yNpsoqGVAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOAs6oP0rOK+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtGiTanb75+M Am6oQrMusULjoZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQ bNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu8 6FmQwLzhSwZKzA27n3Yis1ojKJavh2hoQB/w5XJa42RLfZyY7/Rcc8fSWdHQ81fVTFOApmkY oQAAeoOP+ZWoYf+qVUTsxWxGRKhBP/zxjJSmnP6wbE23uYnHArb3AIgBdUOsHHModvzKacSU vq6zLLJzDrbcf5X2C3y6IrLch87vPqBWrZwcdfSyUY1DAPEj0mfqI3+MjOQ1+QNtnWb7uR6W e2xlmEntht9oiCrxso1jITCm40axEze+ypj3IY1OcO3SFR9YdO8EpZdtD+WOpZ4T84mTW9lv Ck0x6EJtJO/cyYHypUqyhDfZfGGboSF7A/vWeKQLDpkmH9oeq+yiwis/UWhxeDyWM+520tJo CpditTAqGwB2hjJ5sWESvZx5Fmt1SuP2gzJ9+1JI104mKzGIJA72LEwjIAcsUHbEy/2hkr2i KiWe10h+uey6uTnZqzqpoeTN4Npkw3+PLkil86iDegiPQgOWG+b+eu41LL950H2XLJKjvgun qnYtpDVO9gbq7anDwNJ1osv8RWyAje83NgGgHUKLEhJdA+FgoT0I13OJer3Dfa7g1Siijdrw PXGM6XlApXQLXjMiqzhfLdh5E9dyQs+1t9f55dOBbEAJPL/QFP+tNvdDhMhNQy72P7oCM9h2 YMGRWKPHqiZPbvPvVOQ/OIgP/GMZJMJuDb6M/Uq+/nujWYglVABeampwIAYZWujHvVmJkWZe WDjjs0AEWcMpAo+TfblhEeMUT5JND6OWPcX4ShzI4a7B8+XTYe0xbeFwS2TH5tMZ2kABEraQ lnycIDRf+oPYTmAFeRzmz4HXPD1T5Ii3Aq8vx3SzrtiM/WS9yEF84rngosmr9bPnA0/oGQnR /+W1HuAGiQtxjtgr14e2al+pRY40VKfye1ihPceE9VP5vRPWwN8NJjGzuU8BcqhEhnZcIKvT 1CrCs6jHSl3Vsg4ltsTYE9mCd6wphXC2je1RbIZivqTAM986brSikD4PN010HPazO8khlgiT NFIMDiim6127BrYFZzhnECQlqLsfqMZj2bW7GnW622IsQlDVRJoF6XIWXdKfkzNsdHw/V/PV ZerALUjdxNOkIuMc/QTLNLuilpCSbHoP9G2j3uZvWC2CF7Iw7qNaNCvYGABxGDHD0NClQkP/ HGAPAx4ByG7omuYAiY8XVToK1jh9+VzshbZBgc90h2KYkt91rG05g9dhPqSTOkW164FvyFpo it9HVK01dbbQ9SaoA8pcKJZaNI7qFBJsACR/whgPZW7Patwrlsfdhlo+U7iylNvDsQIkMQnq m8r0BsnMbiRgzYjP3uT2ZH9PKGSK3Gnpkj+Lf6LnAuHjZDPpf5cjZZw40/utwyoCEc4pnBu0 t0PlmCZ+o2PFg0ZF5T4Tkcw8RF+4bDceCg0oY3OhhgOeeG5tCHP39UxCa4r0BGlKp1bLaCND x35Ad8yCM2nKehskF+sJEFhXqga5OsvMsWqeuHTkqq2P+97jjm0pWFG5Z1ilE+A6mxkTqSbu vRNi+Hd1QyBWTDmiV6nuc2igoFIawYZGW+nwDTlDopcDkFrVb4CEnzmY8i+x9EkwoXoR2Yd7 lmoQVUPxM6ufxOWKV37xwxZk0oN8zSrni6xzjo8lD9MzOLX2DHNyv/wfwgVEmFOTWhmy1zrJ MC4gssbU06hcwUy3EH9tACqmu4B/fk5djaKCU5TNzD7NWRjTre9ut/gK4ZU5ZUkvD8WGOWwb FaGS6Ls9h4T0iftBWxbl3gwczCnvIm8ngQv0jrMaiYu6iCAJIcpmk6Mgb6UDeRc1TcHWiRi3 DzeB1zmesKs4c3RjZDI9Oa3S2OmUJRXNyjt14KJ8iWhtggISVWyme6+ntr/HE00yyj+gpNuS CbBtwT3cJvD2KGzMOYhdU5tTgyZiYIyCsRln408iYtFk3wHhZyO73EVg0/8NNxa3eT1a39HF ltpi5bFpQPi3kNkNHeAwYn0A26czsVWbN6/emoK2yg54pMCGOKO4bdDhycwvkugoFebf61mh jlEg6hLijZSk6QTtQEq1CnYHr0CARwSI3n3jxrRp9Gm8PcMOSD2IOD2jhYh24jmVu3KoxkAC iilPM15RmkpsJ05aBWVgRiRosnlYIWCM4xV70XO1U+G168PcNowjqZY23QhYz6s+y19jbZ81 0Qm3Inm7tfdbTwxuvvoWFgAcWSlAqFbsjD10fQBwoDPhd3pRtM5XWxVFJrwEaDxSGJU7Ku4c VbISHpm8z+aAeaNRFDErh438zSXVcjsbi/yRjFRzM0+FkPFdQoP3UZNBmV8xtlgSUir3JCzK h4noG1BoAep8F0Ujbs5fxjnDjWF/VnuMGxlDsPFakIRt1AnhQ+dJ8Wa6qgb8zhw2JqnoUTNL 2WaY14NFmQVQgmeAFulOLCy5N7G+uzeB+ykLvKIb6/c4epZH+yFw56iyO4Et36FK9mPM39+D vY6xlsLXHZ3HN7ckikOTCpfnjzEbsqSrhOxsiNtqcX3/PPuUQPprYyBbtkaec1o4AyziLyfO vS4gS94LXNA2cpJyyaXkf4Q21kdjywofD6oUPwBuSPLUKPMi/pXAhocOEYRfIND66Mx2BUIO NaO0IukkO4lyKRsVhEcCgWy/6PhLdYHKGy8Kl7dUUOCNbDcYCbO39mye6S3D7tZkORTsRS0/ zedCU7qeDqZxFyLH1iiN/9BiCaDMVlQooa4J1xpFGvqV8DteA+TP9p+jDlwyroxzCCvVyZUI X1nfkVBo6fFpztfmel6Endd42BNKOCFn2OB4LCdJM9J6L1kBSN7k+8c63M/gegwjmkMVLl+n y3cqcRrqletn7yUyzZpZxFJry5CmIOBuUgK0UTx85BBXTPc80tI4zzPUlIFoNxqDtCpsKdVm ICnfEfbLTZH7s2S8McBQdDQeprv2JUJPh/gGTqSBwwAH2fDCA==
- Ironport-sdr: 9KGO39+Qonx2nTIHwlaperBlJbGCjKqzd0fJrDMLD6rAxlg6/3CfwwyS5fDQNybLhcDIyP1s2w HcAogkQIdyW7uWuPygihpYx6VQ7q/YFCC/rTGoxiDu18T0sA47ZggfnKIZqcaDBS/8SbpuHTSN 4yTF3IDuS5CIZsSwdMpxKxCFV++XD3lhzznq4CGBoF+ECz67nfmJ99/uH0nNvZY6lgezvuDyy9 4xz3a1XQeAiHMJr9zQWJwyFnHQtjkbn+u0RW+ppb8UEOiSQ9UUAw7p9Jgpsue4EdDjpld16JHa OH5sKCjghyppm/i6IuQ2Z15x
> - 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.
"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+.