coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Michael Soegtrop <MSoegtrop AT yahoo.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Ltac versus Ltac2
- Date: Mon, 30 May 2022 22:45:50 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=MSoegtrop AT yahoo.de; spf=Pass smtp.mailfrom=msoegtrop AT yahoo.de; spf=None smtp.helo=postmaster AT sonic305-22.consmr.mail.ne1.yahoo.com
- Ironport-data: A9a23:eUZ39a/MrL6bJAYUIziWDrUDC3iTJUtcMsCJ2f8bNWPcYEJGY0x3m GBJC2DXPP7Ya2L1fNx0Yd63p00O7cCBzoA1TAU+riBEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9g6mJUqYLhWVnV5 Iiq+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z5 99Pl52rblgVBu6PieoHfDZTPywjMvgTkFPHCSDXXc271ErAcnC3m6grVhtwNooe4eNtR2RH9 PheLj1UKAGKh+Wxhrm8T4GAhOx9co+yYthZ4yE9i2iFXZ7KQribK0nOzdpD2zo/mtpJBd7Pb soebnxjYXwsZjUUaglKVMtvxY9EgFH6fzB3jQO7+JEw/nmMnAlRwpnsAOf8L4niqcJ9xRzG/ D+fpgwVGCoyP9uGjDGB73iEnf7KhSq9WYQIFbT++OQCvbGI7ncUDhwdDgPm5KPjzEW5XclaM QoR8ysq664/rQq6R9n6WFuzp3vsUgMgt8R4POc4ygCW7fXo20XaF2YeYRFKRNF7u5pjLdA17 WOhk9TsDD1plbSaT3OB67uZxQ9e3wBKcwfuggdbE2M4D8nfTJIb0kuVEI86eEKhppikRGCrn mziQD0W3e17sCId60msEbkraRqLo5HJR2bZDS2JDjv0sWuViGNJDrFEBHDA6vBBJ93BExzb5 j4PnM6F6fpICJiMkGqLTbxLDbip4PHDOzrZ6bKOI3XD32vwk5JAVdoIiN2bGKuPGppVEdMOS BKL0T69HLcJYBOXgVZfOupd8fgCw6n6DsjCXfvJdNdIaZUZXFbZoXo/PhPMhT+2yBVEfUQD1 XGzLpzE4ZEyVv8P8dZKb7t1PUIDm3FhmDuPLXwF50j2ieb2iIGppUctawHQNL1gtctoUS3S+ spff8uNzxleVuLlChQ7AqZMRW3m2UMTXMisw+QOLrDrClM/RAkJVqGMqZt8Jd0Nt/kFx4/go yDmMmcFmQqXrSOcc22iNCszAI4DqL4l/RrXywR3Ygf3s5XiCK7zhJoim2wfJOJ3r7Myka4pE pHouayoW5xyd9gOwBxFBbGVkWCoXE3DadumM3X3bT4hUYRnQgCVqNbochG/pjgHDi2w88cz+ uXy2gTeSJsFZgJjEMePNKPxlQzs5yBFlbIgRVbML/lSZF7orNpgJRv3g6JlOMoLMxjCmmaX2 l/OUxcVrOXAuaEv99zNifzWpoulCbssD0NaGG6d4bvvbXvW+W+qwIlhVueUfGmBBT2up/j4P b1YlqiuPucGkVBGt5tHP4xqla9utcHyo7J6zxh/GCmZZVqcDL49cGKN2tNCt/EQy7JU5Vm2V 0aI9oUIMLmFIpi6QkUWIgsuNbzekKtO3DLV6+8wOgP/7S5zuryKCANDNhmLj2pWK74saNEpx uIoucg37Q2ji0V7aore03oMr2ncfGYdV6gHt40BBNC5hwcuzGZEa8OOByLz5qaJdNgRYFIhJ SWZhfaZirkAlFDOdWE/SSrE0eZH3stcoxdMzVRZfwnMwICDjfgxxxhLtzE+TwATyBgelfN6O m9scUZyIPzWrTtvgcFCWUGqGh1AW0zBphSskQNRmT2LVVSsW0zMMHY5ZrSA8UUfxGRWIWpW8 bSe/2D6XGu4Z8r2xCYzBRVopvGLoQadLeEedB1L3vhpHqXWpRL+hamvbjFQ9l69W4U6g0vco PMs+e9xbev9OHdWsqQ7DI7c3rMVIPxByKquXtk5lJ7l30mFEN1x5dRKA1G4esRKYfDHmaN9I 9I7PdpBDnxSyw7Xxg32xscwz3tcjfcp491Edr6DyavqdVeAhmIBja88PRQSSIPmrxuCXCr9x k7sm+q+L1Gt
- Ironport-hdrordr: A9a23:/iGCoaGWerJ4Qx6tpLqEFceALOsnbusQ8zAXPjNKOHhoW+afkN 2jm+le8BPyhisRMUtQ5exoX5PwO080lKQFmrX5WI3IYOCIgguVxe1ZnPLfKnjbalXDH41mpM RdmspFaeEYZGIS5amV3OD7KadH/DDtytHMuQ6x9QYLcegnUdAD0+4AMHfnLmRGADNhIroSUL e/xu4CnRqPXh0sBPiTNz0+We/CrZnuu/vdDSLvU3YchTWzsQ==
- Ironport-phdr: A9a23:Xwz6qRcNyEBuAt3cYF13ytRDlGM+atXLVj580XLHo4xHfqnrxZn+J kuXvawr0AWSG9WFoKsY26L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNbQhEnjmwbLJ9I BmrogjctdQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2U bJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5 KptVRTmijoINyQh/W/UhMJ/g6xUrg+/qRxxw4DbYp2aOvV5cK7GYdMXR3BMUtpLWiFPAI6xa ZYEAeobPeZfqonwv1wArRqiCgmsHuzg1DtIjWLr0609zeshHh3G3BYnH9IWrX/Zq9L7OroVU e+rw6nI0S/Db/RO2Trm6InHaBAhofaLXb5qbMXe11AiGgXYhVqftYLrJSma1vgRs2eF9epgU /qihnIlpgxvpjWiycchh4bNi48V1FzK+zl0zZo6KNC2VEN3f9+pHpVRuiyYKYd7Qc0vT311t Sg1yrMLuZ22cDQUxJkh2hXRaOSHfpCJ7x/iTuqdPDZ1iXx/dL6ihBu/8VKsxvDzW8S31ltBs zBLncPWtn8X0hze8siHReV5/kemwTuPzAfT6udFIU8om6fXN54szqcumpYNq0jMAij2mEPtj K+TbEUo4O2o5P7mYrXivJOcMZF7hhzkPqUugMO/AeM4Mg8UU2eH/uS80aXv/Uz/QLpUkv07i qjUvZHAKcgGp6O0DRVZ3psg5hu/FTuqzdsVkHofIFJAYh2HjozpO1/UIPD/CPeym1GskCxsx //YMb3hHo/NLn/bkLr6fbdy8U5cyA00zdxF+p1bFKkNIPToVUDprtzXEgc5MxCow+bgENhxy 5sSWXiTDa+BLKPSrViI6/ozLOmLfY8ZoSryK/w45/H1lnI5gl8cfayx3ZQNcny4H/JmI1+YY XX2mNsBH30K7UICS7nhj0THWjpObV6zWbg973c1EtGIF4DGE6Wsi7yI0SPzJZpbaXxcDUjER VLTcIiLR+0LcAqDK89mlXoIWO7yGMcayRiyuVqimPJcJe3O93hA3XqC/N185umJ0Ao36SQxF cOWlWeEU2BzmGoMAT4wxqF250JnmR+YyaYtpfteGJRI4u9RFB8gPMv59Ot3BMzoXRrpb96JT 1HgTtj1SSopQIcJysQVK114B83kixnC2ySwBLpAkqeMCZMo6KXE92n4J8F6jXrLh+E6l1dzZ MxJOCW9g7JnsQjeA4mci0KCi6OjbrgRxgbW82GCxjHW4QQCCkh7VqPeWGpZY0LXqZL/6xqEX rauDrNhOQxEoSKbAo1NbNChzVBPRfO5fc/bf3r0gWC7QxCB2rKLaoPuPWQbxiTUTkYewUgV+ j6dOA4yCz3EwSqWBSFyFV/pf0Ln8PVv4HK9QEguygiWbkpnn7Or8x8RjPaYRrsdxLUB8Csmr jx1Gh660be0Q5KlnA1sc7lGZssV8V5H0mWfuwE8dp2sIqZ+h0IPJhxtthCm3BF2B4Nc1Mky+ S10ilMscuTBgA4HLm/IjvWScvXNJ2L//Q6icfvT01DaipON/7sXre4/oBPltR2oEUwr9zNm1 cNU2j2S/MavbkJaXJTvX0Iw7xU/qavdZ3x34pjT2HJwK66smi7L29UuQucogEXFHZ8XIOafG Qn+HtdPTe2VL+Elh0KudjoVNeBV8+g4Mon1P+vD06mtMuF6mTughmkS+4Fx3HWH8C9kQ/LJ1 ZIIqx2B9jOOTCy0zFKos8St3JtBeSlXBG20jy7tGI9WYKR2O4cNE2anZcOtlJ1ygJvkWngQ8 1DGZRtO3dSudBWOdVvl9RxZ1UMQ53Cq0Se11D17lTg1o7HXgnKImrq5MkNXZygSGDkqhEykO YWuitEGQEWkCmph3ACo40r33ekTpahyKXXSXVYdeiH3K294Va7j/rGGYsNJ9NYpqXAJDqLlP wvcE+6g5UJGg3CGfSMW3j0wejC0t4+smhV7jDjYN3NvtD/Dfso2wx7D5dvaTPoX3zwcRSA+h yOEYzr0d9Sv49iQkI/O9+6kUGf0HJhIdiTk0ZmHrAOq7G1tBluzkrrg/7+vWRh/yiL929RwA G/NtxHxbZXx0LySIOtneU4uCFK2uIJqX4p5lIU3npQZ33MX046U8XQwmmD2KdxH2Kj6YSloJ 3ZD05vP7QPiwkEmMmORytezSCCG2sU4LYryciYM1yk69cwPFKqE8OkOg35uulTh5RrNe6psl zcazr0l73t/4alBoBY3nDSUArcVW09VIWS7nhCMpbhStY1xY2CiOfi13Ut6x5W6Ca2a5xtbU zD/c4sjGil56oN+NkjN2Tv98NOsft6Ydt8VuhCO9nWIx+FINJI8kOYLjit7KCr8u3Mi0esyk R1p29mzooGGL2xn+K/xDARfM3X5YMYa+zeliqg7/I7ex4e0ApBoASkGRrPzSvSpG2lK6LG9b UCFFzsnr23dHLPeGUmZ5R4gvnvPFJftPHaSZRx7hZ1jSBSbOE1DkVUUUTE9zdYyEgGnwtCkc V8suG5XvwCj7EIcl6Qxa0msNwWX7B2lYTo1VpWFeR9f7wUYolzQLdTb9OV4WSdR4pymqgWJb G2dfQVBS28TCSnmTxjuOKej4d7Y/q2WHO27erHLerKDpvBEUO+g1Juv1Ywg8zvGZaDtdjFyS uY23EZORyUzA8PChzAGUDAajQrWaMiar0zkp2gt9Ia09/LwXRip4IKOD/1UPIwp6hm2hqDFP OmVznUcS34QxtYHwnnGz6Ia1VgZhnR1djWjJr8HsDbEUKPanqI/5/szeipzM8wO469uhmGl1 ubKg9Py0fh0g6xsY7+kfUfmnMCiPpRXZjvncljAAl2OLvKDLDzPhcf6OOWtQL1Xi6NfsBji4 V6m
- Ironport-sdr: N80l+oZK1hvH0f6fPJc6xDa6hn3iqe+Bo0qffCkqfM+1aU4Iz+8AIUznCVOa4LOIo2+JrSUqsb LuygA6GB7btRHBhMWSoE7rUje8h7yH6vpigpMxMkJ53LAU4WrTh2c9VZ1bE73/jLL1MMb3F3t/ pW/+eysgDtQZN+aWtaKaJNIupYiyS5luuBS5ebDl0woKqWTQT1dYUmGC2EwEdzAMS1+O0p1gGu V7WTwrchUDI7vjszv9uxMRkVO0srxX4+Ifzj0w7vX0RmHlluqBTEGq0WbxAuO+a+d8pUaTCGx6 OBNyZV0BqKvaZwylCcx6xz9Y
Hi Jason,
Ltac vs. Ltac2 is a bit like bash vs. OCaml (only slightly exaggerating). Ltac is optimized for one liners. It is an untyped language, but for one liners this doesn't matter. It is still quite OK for 10..20 lines, but 100 lines (for the complete proof automation task, not a single function) is already a stretch IMHO. Ltac2 is a typed language - essentially an ML dialect, and suitable for larger automation projects, while maintaining a lot of the syntax, which make it easy to write one liners (it is mostly compatible at the one liner level to Ltac by using notations).
Ltac2 documentation is rather terse, but you usually get quick help in the Ltac2 Zulip chat topic. Since the addition of printf I would consider Ltac2 ready for production use - not that there is nothing one could improve, but it is absolutely OK. The Ltac2 test files in the Coq git repo are quite instructive btw.
So for interactive proofs with a bit of ad hoc automation here and there, Ltac is just fine. For any serious proof automation project I would use Ltac2 (or reflection).
Best regards,
Michael
- [Coq-Club] Ltac versus Ltac2, Jason Hu, 05/30/2022
- Re: [Coq-Club] Ltac versus Ltac2, Michael Soegtrop, 05/30/2022
Archive powered by MHonArc 2.6.19+.