Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Ltac2 tutorial?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac2 tutorial?


Chronological Thread 
  • From: Talia Ringer <tringer AT cs.washington.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Ltac2 tutorial?
  • Date: Thu, 3 Mar 2022 12:40:26 -0600
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mx6.cs.washington.edu
  • Ironport-data: A9a23:SgUHGKPKZdXMPCrvrR2RkcFynXyQoLVcMsEvi/4bfWQNrUoh3jwOz GZOW2jXPP2LYWTxeY1+bN+0pxxS6JXVzIRlTXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/jgqoPUUIYoAAgoLeNfYHpn2EoLd9IR2NYy24DiW1jV4 7senuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB3Kx+8yl ItOqaWfYixuLoz9n8BNeglhRnQW0a1uoNcrIFC6oZLVxFaAbHL3w/RoA10xO8sV9vsf7WNmr KZIbmpVPlbf2KTrmdpXScE07ignBNXxPYUQt2tIxiqfEv89QZHFTLnN45lV0CpYasVmQquDO 5dBMVKDajybJABwOGgwLa4xv+WGm1jifTFDkwia8P9fD2/7kVUvgOa2WDbPQfSBQtwQlUKFr Erd7mHhC1cbMsaewHyL6BqRavTnmDOlHokJUqKx7f5rhlKPwWpVBRELPbemnRWnog3mZJEDd U8IwwUFhu8i1X2saonUTyTt9RZooSUgc9ZXFuQ77iSExazV/xuVCwA4c9JRVDA1nJNpG2Nxj Tdli/usXGY16+HPFBpx45/JxQ5eLxT5OoPricUsdgYM/8XnrenfZTqeHo87S8ZZYjAFcAwcL hiPvHZ4jK5VkscQ16S98kzAhXShqoWhou8JCuf/BTzNAuBRPdDNi2mUBb/ztKooEWphZgPd1 EXoYuDHhA3OZLnU/MB3fM0DHauy+9GOOyDGjFhkEvEJrmrxpST/INAIvm0nfy+F1/ronxe0O yc/XisMv/du0IeCMcebnqrqU5l0k/SI+SrNC62KBjaxXnSBXFLeonEwPiZ8LkjwlkkynLskO IuKOcGiRWkTEqRmyjWqQOF17FPY7n1W+I4SLLilpymaPU22PybEGe9YawLVNojULsqs+W3oz jqWDOPSoz03bQE0SnC/HVc7IQ9YIH4lK4rxrsALJOePLhA/RzMqELnOyKgheopqg6NT0OrE4 yjlCENfzVP+g1zBKBmLNyo9MeyxBc4noCJpJzEoMHapx2MnMNSm46oofpcqeaUqqb54xvluQ vhZI8iNW6wdSjnO9zkHQ4P6qYhuKEaiiQ6UZnX3ayN5YJd7Rw3P9cPjeE3i+DRXVni7ss43o ruB0ALHQMdZGV09Up6OMP/2lgG/p3kQnu52TnDkGNgLdRW+6pVuJgzwkuQzcpMFJhj0zzeH0 xqbXEUDru7Xro5pqNTEiPzWr4qtFOciTENWE3OBtOSzJXec9XHl3oZbUOeOcizaUiX59Lj7P bdZyPT1MfsmmldWstcmTe80k/pmv9a/9aVHyglEHWnQawr5AL1XIk6Z0JQdraZK3LJY51e7A xrd5tlANLyVE8r5C1pNdhE9Z+GO2K1GgDXU9vhpckz26DUtpeiCQRsUNALKlyVGLLpzP58ix 6EstNNPs16zjR8jM9CniCFI9jnWcCVfDf1/7pxKUpX2jgcLy01ZZcKOACHB4KaQZogeKUItO DKV2vbP3uwO2krYfnMvPnHRxu4B148WsRVHwVJqy45lQTYZaivbHSG98AjbiixQ3ksB2Pk1J WFwN0xzKrmJ+XFliNUrs6VA3e1eLEXxx6Az4wJheK7lo42AXXeLM2QmOeeL81we9SRRciUzE HSw1jP+STizFC3u9nJaZKOmwsAPifR67UvdkdunHsKKA548Jzfpn8dCoIbORwTPWasMuaEMm QWmECucp0E22e78bpDX07Wn6Ik=
  • Ironport-hdrordr: A9a23:x67jdKONkXFrUsBcTu2jsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZYmPHPP+VUssRIb+exoWpPwJU80nKQdieJ9UYtKNzOW31dAQrsSi7cKAAeOJwTOssBY3a dkN45kCNPxClB+yeL3+hOxHdpl4PTvytHMuQ4T9RlQpMhRCp1d0w==
  • Ironport-phdr: A9a23:p2paqhDEqlTAXLfmCMCgUyQUrkoY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua83ygaRA86CsqkMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YPfbx9ViDahYL5+I wi6oRjfu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ 7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8 qFmQwLqhigaLT406G7YhMx+gqxYvRyvuQBwzpXOb42JLvdzZL/Rcc8YSGdHQ81fVzZBAoS5b 4YXEeQOJ+JYr4jnqFATsRW+BA+sBOzxxT9Sm3T72rE60/4gEQHA0wwvAcgOvW/Io9XuLqsTX /q6zLLIzTXCafNW1iv96I/Ochw7v/6DQK9wfNPXxEIyGAzLkk+eppb5PzOJyOsNqW6b4vJgW ++si2MqqgV8riShy8oyiYTEhYIbxk3Y+Ch5wIg7KtO2RU17bNOrEJZety6UOoh2TM8/R2xkp Tg3x74YtZO5eiUB1Zopxxnaa/OdcoiI5AruVOmQITdkhHJlZamwiwyu/kinz+3xUNS/3lVSr iddj9XAqHMA2wbN5sSbSfZx5Eis1DSV2w3T9+1IOV44mbbfJpI7wbM9loAfvVnCEyL3gkn7j LKae0M58eay8evneK/pppqEOo90lA7+NqMul9S6AeU3MwUCRXSU+f+m2Lzt50L5W7VKjvwwk qnWrJDaIsIbqrSnDABIz4Yv8xe/DzG439QEhXQLMUxJdRGdg4T3J13DI+r0APi9jli2kDpn2 ujKPrj7DZXMKnjDnq3hfbF460NE1Aoz19Ff55RbCr4fOvL+QVP+tMfCAh43KQO02ObnCNR71 oMRRWKPBamZPLnMvlCV++IjO++Ma5QNtzbnN/cl/+LujWM+mVIFYKWlxYEXZ2ygHvR6P0WZZ mLhjcsGEWcTpwYxUOjqiECZXjNIfHazX6c85ikhB468DIfDQJqtgL2b0yuhEJ1WfDMONlfZG nDxMo6ARv0kaSSII8YnnCZXe6KmTtod3BWvvUfAyrxoI/CcrjECtJTs2cJd7PaVihgp9T1yA Nia1SeAQ3wizTBAfCM/wK0q+R818VyEy6Ut25SwdPRW7vJNCUIhMILEivd9E5b0Ux7AedGAT BCnRM+nCHc/VIF52McANmB6HdjqlRXfx2yyGbZAi6aKApM56IrXxD7uLt19ynDJyK4nyVQqX 5gHLnWo05Z27BObHIvViwOcnqeue74b2XvR7maFwmeUlEpDFhF5SqXEW38DYU2QoNjktQvZV 7H7L7MhP0NazNKabKtHbtq8lVJdWPLqI8jTeUq0izn2Dg3O2bqXbIvsdHka2mPQBFVsfxk72 3GAOEB+Ay6gpzmbFzlyDRf0ZFuq9+BiqXS9R0tyzgeQbkQn2aDnshgSzeeRTf8exNdm8G8ot il0EVCh3tnXF8vIpgxve79ZaM8851EP3HzQtgh0NJitZ654gVtWfwNytkLonxJ5b+cI2dQwr XUlwRBaIrnez1padzKe0oz3PPvaJnSztBGjZqjK203Phc6M8/RqirxwoFHisQe1U0s6piw9g 58PiyvausqMUVNBNPC5Glw6/BV7ubzANyw05oePkGZpLbHxqTjandQgGOoizB+kOdZZKqKNU gHoQKh4T4CjLvInn1+xY1cKJudXoeQoJcKgePac8KWwevlphzKni2tb54Y7306RvXkZKKaAz 9MezveU0xHSHSvmjVGuv9rfkpsCejgJHmu5xjTjAshcarA4LuNpQS++ZsawwNt5nZvkXXVVo UWiC10x08isYROOblb50GW8zGwvqGe80Wu9xj1wyHQyq7aHmTfJ26LkfQYGPWhCQC9ji03tK M66lYJSUE+tZgkv3ByrgCSyj7RBpaJwInP7SlwOYCHtL2BkXbe3sPyPb9MH5J4zsCpRWfixe hjDEO67+UNKlX+8WTYHjDkgElPi8o30hRl7lH6QID5ooXzVdNsxjRbT6drAROJAiz8PRS12k z7SVRC3O9ik+8nRlo+W67ruETj5BtsPLm+2lNDl1mPz/2BhDByhkurmn9TmFVN/yirnz5xxU j2Oqh/gY47t3qD8MOR9f0AuCkWvjqgyUox4jIY0g4kdnHYAgZDAt2YdkGH8PM9z0rm4c3MWR T8NzMLS5k7o1FApfRfrj8rpE26QxMdsfYzwfnkX3C0w9ehBE+GL5adEnC16vl2+6w/dfLIu+ 1VVgetr43kcjeYTvQMrxSjIGbEeE35TOin0ngiJ5dSz/+1HIXyier+q2A9ijMisWfuc9xpEV i+zKfJAVWdgq99yO1XW3Djv55H4LZPOOMkLuETcmkXbivRNL48t0PERwzd4f2/xoBhHg6Y6l UA8h8nn+tLdcyM0o/3/W0IGcWavL8ILpmO31fsYxJzOmdnxQ9M4RmtMB8GNL7rgESpO5629Z 0DfTXtm9i3dQ+CFWlTFoEZ+8yCWScDtbSnHYiFfkJI5HlGcPBAN2VpEGm9izthgRlnsnIu7L iIbrngQ/gKq80cUjLs0bV+kCCGG/lfvMGp8SYDDfkMKtkcbux2Ta5fCqLspT2YCo/jD5ESMM jDJPlsTSztUAgreXQ+lZv70uZHB67TKX7XlaaGTOfPX97wYDq/Ygsn1t+kutzeUapfRbz8zV rthhxAFBys+QJ6Rmi1TGXVNx2SXN57d/k7gvHMq6ZvllZajEAP3udnWUesUa40/vU7ux/7Yb anL3m54MWoKj8lcgyWQmP5BhBhP12Y1LVzPWfwBsyXJUa7dyJhMFxBdZCR0O89Fqak720FMP 8Xfl9/4hKVggLgtEVBZWFf9m8avI8sXP2W6M1CBD0GOUdbObTzNyMXqba7uR7FLlOtJrFu+o zuAE0LmNzWH0TjuHxGpOuVRgCzJOwFCsoagdBpoAGnnCtnhbAO6N5lxgCFTo/V8kHrOMSR03 SFUVURLo/XQ6CpZhq46AGld9j9+KvHCnS+F7u7eI5JQsP1xAy0ymfgIqHI9g6BY6i1JXpkX0 GPbs8Jurle6k+KO1isvURxArSxOjZ6KukMqMLvQ951JU3LJtBwX6mDYBxMPrtpjQtrh3sIYg sDIj772ISxe/sj8+NtCQcPPbt2OK3ogNxX1HziSAQcYDHaqOWzZm01BgaSS+3mS/f1Y4tDnn JsDTKMeVURgT6lKTB49TJpef9EqB2BB8/bTlsMD6HugoQOEQcxbusuCTfeOGbD0Ly7fi7BYZ hwOyLe+LIIJN4S91VYxDzsy1InMBUfUWshA5yN7aQph6llX8X5xQ3cb0FmjdQq24H4VGuKzm Fg7hhY0MoFPvH/8pkw6IFbHvn56iE4qhdDsmiycahb0PPn2VpoQFCPvt0k3PY/8RUB4YRD4z ikGfH/UArlWibVnb2VijgTR7IBOFfBrRqpBeBYMxPuTap3AMHxZunvhzlQB+uLeCZpkmxctd 9iho28Sg2qLg/Y+PurPLbFJz15fmqWI+CKky7JoqOf7D00WtnybYy4JvkMUMb9gKia1rLQE1 A==
  • Ironport-sdr: cA7d+3eVz4CESaQY0zhMzz+/1GSvp0dYzjDgeUBXfvuG2+U6p+n2BAKX0K6YZBZs7hvuc5qSTL aY2RUQkKhd+VhBCYJcSzCF6e7EXSkG41DBiQdLAGxSJlZcV36p+JY8Ex88xiJX+EzY+Szn4SBU aHOEATMPTRgsLYBtgmiuynWbUvCoqJgLabiu7m6VcmCx3DHqtqFl6/xxjDq0G5gqH2SVCFTNQd 8EGBxKYy/TY7edGR8/1s/qsK+imy4hxFUnqgPvcJo50gTu034+MonkLHk0cClXRAFLeJmPFA6m Jq5JLwBEbmypSVFqalZ3ho+o

Hi all, I just wrapped up a class today where students in my proof automation class walked through a plugin tutorial (https://github.com/tlringer/plugin-tutorial). The tutorial I made was based on the ones in the official Coq repo, but modified to make it into an exercise and do some interesting things.

After the class, I found that almost everyone in my class preferred plugin development to Ltac. But I also know that Ltac2 is an apparently nice middle ground. When I tried to learn Ltac2, though, I couldn't find any resources that helped me understand what was going on, so I gave up.

I'm curious if anyone has written or would be willing to write an Ltac2 tutorial similar to the plugin tutorials in the Coq repo, or the one I just shared. If so, I'd like to use it next time I teach this class.

Talia 





Archive powered by MHonArc 2.6.19+.

Top of Page