Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2 tutorial?


Chronological Thread 
  • From: Talia Ringer <tringer AT cs.washington.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Ltac2 tutorial?
  • Date: Thu, 3 Mar 2022 12:56:14 -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 mx5.cs.washington.edu
  • Ironport-data: A9a23:axH9Aa0JOM+8j2ApH/bD5QR3kn2cJEfYwER7XKvMYLTBsI5bpzJVy 2MYDW+COvaJNGr8e98iO4my/UwPuZCEzNIxSgNr3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOH9IQMcacUsxLbVYMpBwJ1FQyw4bVvqYy2YLjW1jV4 ouoyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt+gqw /xiibmZckBqN6/it8Q7bURgKRgraMWq+JefSZS+mcmDkgvNaD3zyu5uDUc5IYoevOt7HAmi9 9RBcmBLNEjTwbjwnO7TpupE3qzPKOH3JoIZtXx65TrCS+kvWpDCRarW4tke0Tst7ixLNamDO pdDN2YHgBLobg8fB3k2DcgFsr2OpiL1fHphkFeXjP9ii4TU5FEojuiza7I5YOeiTsJM202cu 2ju5HX8GhhcNdqFyDPD/GjEuwPUtSbrBcQZD/un/+VqgVuc2msVThAaSDNXvMVVlGaGANl2B HAx0xFp7qEw2mOLaOegZyeB9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVsctKnQIB93CPRbWBwv mJlj+8FFhQz7+PFFCP1GqO86GroY3JEfDNqiTosEGM4D8/fTJbfZ/4lZu1uGbKpitCd9drYk mDT9XVWa1n+fac2O0iT+ECaxTm34IfAVQ404ArLWWTj4w9kDGJEW2BKwQSChRqjBN/HJrVkg JTjs5LGhN3i9bnXyESwrBwlRdlEJ5+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB43bpheJWK5O BGP4Fg5CHpv0J2CMPQfj2WZVp9C8EQcPYiNug38NYITPMYtHON51HwzOyZ8IFwBYGBxyP9vZ 8zznTeEEHAbF6l91zuqVq8a3/c0zzs+xGXcWZf9pylLIpLDDEN5vYwtaQPUBshkvPLsnekj2 4gDbpfiJtQ2eLOWXxQ7BqZIdQFadSVgXMuuwyGVH8baSjdb9KgaI6e56dscl0ZNxsy5T8/Eo SOwXFF20l36iSGVIAmGcCk8Orj0G4l2tnI6OyMwOlDu1nQ+ON794KAafpoxXL8m6O0+l6AtE KddI52NUqZVVzDK2zUBdp2s/oVteSOiiR+KIyf4MiM0eIRtRlCR99K9Jlnv+SACAzCZr8w7p 7H8hArXTYBaGFZpF4DJYemvzlW+oX8b3u9+QhKQcNVUfUzt9qlsKjDw06Vpep5ScU2by2LDh QiMABoeqe3cmKMP8YHE1fKesoOkM+piBU4LTWDU4IG/OTTe4mf+k5RLV/yFfGyFWW75pPeia OFSw62uOfELhgwT4Y9sTvBg1uQh7sDvprlV0gNiWnjHcg3zWL9nJ3CH2+hJt7FMm+UH4FToA hrX94kII6iNNePkDEUVelgvYNOD4u4Zx2vJ5vMvLUSkuCIupOibUV9fNgWngTBGKOcnK5ssx Oos5JwM5wqkhkZ4O9qKlHoNpWGcczoLSOM4v4oaAYnklg0tjFxOfMWEWCPx5ZiObfRKM1Urf 2XK3fWc3+wEyxqQaWc3GFjMwfFZ28YEtidK+0APegaSkd3fi/5pgBAIqWYrTh5Yxwls2v5oP jQ5LFV8IKiD8l+EXiSYs7xAz+2AOPGYxqA1414ZySvSVA+3X3fNLWsyJeGLuk0V7gqwu9SdE K6wkA7YvfTCJakdHRfenWZusLr8RMdx9wvNhMehWcmJAvHWpBL717S2azNgRwTPWKsMaY6um QWu1O1rL7LyLi4RpaInDI/c2LgNIPxByKquXtk5lJ408arglP1eFNRAx41dui+AGhASzXKFN g==
  • Ironport-hdrordr: A9a23:c+QmPKAf3UCsay7lHel055DYdb4zR+YMi2TDtnoBMiC9F/bzqy nApoV+6faZskd1ZJhko6HjBEDiexPhHPxOkO8s1N6ZNWGM1QeVxcNZnOjfKlbbalTDH4BmpN 9dmmtFZ+HYPBxVic775U2fCNYvwN6O9eSNif3Fx3lgCSFGApsQiDuRxjz0LqS+fmh7OaY=
  • Ironport-phdr: A9a23:eUgiwRGD/4PNdQcwId2p6J1Gf95FhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31hmQBduQsqsZw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PNbwlSmTaxfbJ/I BqroQnMtsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3U bJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5 LptRRT1iikIKiQ5/XnYhcx+jq1VoByvqR9izYDKfI6YL+Bxcr/HcN4AWWZNQsRcWipcCY28d YsPCO8BMP5GoYbno1sOrAGxDhSwCuPuzD9IiWH53bcn2OkmDQHGxg0gH9QBsHvKttX4L7sdU fuvwKjG1zrDdPNW2Tb76IjHbhAhpveMUahufsXM1EkiDgXIhUifpoL5JT2azPgNs3SF4Op6U +Kik3Mrpx1xrDah28shjofEip8Ux13F+yh0z4g7K92mRUB0YNOpFIdduj2aOoZqTc4sTX1lt SUmxrAEt5C2fywHxZUhyhXCZfKHdI2I7QjiVOaXOTp4i3NleK6/hxav6kes0PHzVs6x0FtMs yFLkcHMu2gQ2xDN6cWLUOVx8lui1DqVyQzf8O5JLE8smabFN5IsxqQ8m5kTvEjZAyP7mUT7g LWLekgn5OSl7fnsbK/8qZ+GLYB0jxnzMqQwlcy7BuQ1Kg0OXmeb9OimyLLj5lf1QbtQgf0tk qnZsZbaJcsHpq6+BQ9ZyJgs5AuiDzu+0dQYm2cILE5ddR6akYTkOEvCLO7kAfq8mVigji1ny v/JM7H5B5XCNHnDkLPvfbZn7E5czRI+zcxF55JVDLEBL+z8WlXqudPEFR81KQK1zPz8CNV91 4MeX22PArOeMKPUq1OH+P8gI/SUaI8ToznyM+Il6OL2jX8lhV8derGk0YYPZHCiAvtmO1mZY WbrgtoZDWgKuRM+QPX2h12GTD5cfG2/X7k85zE+EIKpF53PRoGrgLyb3Se0BIdaZm5cCgPEL XC9fIKdHvwIdSi6I8l7kzVCW6LyZZUm0ESSvQv7wvJdL+zb9zdQ4Y751d566vf7ngp06jVvD 8Wb3H2KSSd5kn5eFGx+57x2vUEokgTL6qN/mfENTbS7httMWwY+btvHyvBiTsv1QkTHd8uIT 1CvRpOnByswR5Q/2YxGeF5zTvOliB2LxC+2G/kNjbXeGIY19K3RxVD6PIBiwm3G1a8uk14gB MZDKD7unbZxojDaHJWBiECFj+CvfKUY0jTK8TKf12uIs0xCeAVrF7rMRnAeYETKqtK/60/fH Pe1EbpyFAxHxIaZL7dSLN3kiVITXPD4JNHXeH68gU+1FUvOzajKc4Pxe2Qb0znaDg4Jnx17E W+uEw84C2/hpmvfCGcrDlfzewb39vE4rnqnT0gyxgXMbkt71rPz9ARHzfqbA+ge2L4JokJD4 319AUq90tTKCtGBuxspfaNSZsk46UtG0mSRvhJ0P5ipJaRvzlAEdAE/s0Tr3hRxQoJO9Kpi5 G8wzQx9JLiw20gHaDqD3ZH2NaHQLC//8A3uI6/a11fC0cqHr78V4addyR2rtwWoG0w+tnR/h oAPgz3GvsWMVkxODcGUMA5/7RVxqrDEbzNo4orV0SYpKqyoqnrZ3MpvAuI5yxGmdtMZMaWeF Qa0HddJYqrmYOEshVWtaQoJee5I86thdd+8dv2J1bSDN/0mgzu9jWVB75x61ASB+zc2GYuql 94VhuqV2AeKTWK2kE2gtM/6g6hPfncNF3G/yC7rGIlXIKB+YMxYbAXma93yzdJ4iZn3Xnde/ 1P2HFIK1viifh+KZkD81wldvagOiUSugjDwjzl9kjVy67GawDSL2OP6MhwOJm9MQmBmy1bqO 4m9yd4ADgCkaA0glR3t4kifpeATuL5+KWbeW29DZG7pJnpiU62/qr2EJcND9dskvD5WX+K1f V2BAuen811Ai3OlRS0CmHgybFTI8t3hkgZ/iX6BIXo7t3ffdcxqhF/e6NHaWf9Nz28DTSh8h yPQAwv0NN2o8NOI0pbb57nkByT7Ds0VK2+3kdDl1mPz/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+NtBQcPPbt2OK3ogNxX1HziSAQcYDHaqOWzZm01BgaSS+3mS/f1Y4tDnn JsDTKMeVURgT6lKTB49TJpYZssrDVZG2faBgcUF5GSztkzUTcRe5dXcU+6KRO7oMHCfhKVFY B0BxfX5K54SP8v1wR8HCBEykYLUFk7XRd0IrDdma1p+vF9M9ndzVEU4wAT6Yxit4XkcCfmy2 BM6l0EtBIZlvCep+FoxKlfQ8WEol1ItnNz+nT2LWDvhceG7RsdJAjH0tk4+LpT9BQt5cEfh+ C4sfCeBTLVXgbx6cGltgwKJoppDF8lXSqhcaQMRz/WaDx3H+V9H7Dqu3k9G4+TZDp0kmQc3I 8fER5do0Bklc9cuJa3WK7ZOyB5dir/c5kdAN8g00FJYLF1L72qJeC8Ot1APMP8rKzf6poRR
  • Ironport-sdr: EZlF8X/kRCImc8fWZuiq0k3ZpFXihzQlNUvlnucxDM23GnIZmDs5bbgVgi4hEOHqPEjmFJgXDQ 1e+U/xuPK4oRnhooqhj93GwHi+glGnbgqwvhZmfWtVWUyJgCSnWTDMEsb1e+auUfnY8oi7KDgN Qq4gqW+CZTuYCQUK7mNTpWdr407tqkhkwcvmjMRpXSzrsBTqz57i0PpYMDszYRsTNoSd1Ii5c6 /sACJ+HBJ3devtfBIBq0G4guwC/N/Lj8QUWw7ifxyPdvLyZ6gE9eiT4JlvrIcLXrFmhF6/qvpz 6nE8wlQhh8sMlUOY7BhI37/w

In case it's relevant to the Coq developers, some tradeoffs that came up for Ltac versus plugins:

Ltac:
- breaks less often over time
- doesn't require learning internal Coq APIs
- has good navigation of goals and hypotheses, and easy ways to refer to other tactics
- can do all in one file
 
Plugins:
- extremely powerful
- OCaml is a popular language, so it's easy to find help/support for writing OCaml
- good type system
- semantics
- easier to organize large projects
- more control over what automation does

This is why I'm especially interested in what students would think of Ltac2, which has some of the upsides of both of these. But the help/support point is really big. I don't even know how to learn Ltac2.

Talia 

On Thu, Mar 3, 2022 at 12:40 PM Talia Ringer <tringer AT cs.washington.edu> wrote:
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