coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Hu <fdhzs2010 AT hotmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] HTML output that remembers proof states step by step
- Date: Tue, 30 Jul 2024 13:16:50 +0000
- Accept-language: en-US, en-CA
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=dOcj+v4fR8c66em4f+cVx55/JFV/cz4HLNfiFa/lUPI=; b=bgSrGsCdOp41n/QiOyy+nWW+6GiE8SeOBmHqKn2BeL5etVWZJ4rGpB4/aGG+bdkl4mGOeFytQnR6t9h9W7QcKnU2WDFQt38hkOy8HFuh6Z+9OrTC3JzN12AaUY5pMJXBcpyJcMDHRacJW+jbKb6AlSDsI999yF1abJxvclST036W99GtenpAT0Sm/OLDEAoM7ErRXmETrMnRXEr9YTanhMUjKO1DRJ1IT8CFHFwV4rQq9MRqHPnYoVqbNvL+hh6i4QkbP+CZ2i8J1fRMVqdeqS2Wa1fIBrzH1UHeWuttGyZBnNoeuDBTzF267wsWO3Tev6HnyiXoPHCop21RbNlhPg==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=WAHvu1NZZP6dGywba334ZomRofCU7LTNb4cCQ8g8S4iWkpE6dwuDbLvvzS/Bb/q3z2+y0bWgTyt6ZI0XHTv3VnQJB7o/j/wFkcGDDcCHLcOT+WvaILdm95SeNgaz/uiyZcqRfBpqkl2xxJ7n8Y16SSZDgeqVwaL8/v5pwVkYbTJq28OyDLI7B0kmG+Nvy5JiCIQSCD9oLm/IuEnVtlgJYZeHOnew99IIN5vcHMCU4kAkx2rrGWbso/Ss9bZgJSfS0h46c3b2qjyU6oJR6lO8bAXAVqe//wZG5NYwhZ/DYok5oxiBniLejkdsG0Vpi7mp4RgWfnIwGBzH/TL0UaunZA==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM11-CO1-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:eingF6J2N0qIOfD+FE+Ryp4lxSXFcZb7ZxGr2PjKsXjdYENShDVVy mUdXWCDPv6INGXxc9AlbI6z/RtXsJDVxtQyTgEd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf0s9JIGjhMsf7b90g35K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LuLUnBkqpTMkAKMLY8ubZpPmcX1 sQ1N2VYBvyDr7reLLOTbMBJ351mB+6yeYQVtzdn0C3TCusgTdbbWaLW6NRE3TA2wMdTAfLZY MlfYj1qBPjCS0EXfAZNTstu2rjz7pX8W2UwRFa9q6Y38XOJlFUp+LjqLN/ce9jMTsJQ9qqdj jOdpTmoX0tAXDCZ4R3b3SKIpd2UphmhAqstFqX71PVbpFLGkwT/DzVNDgHn/pFVkHWWUNVGb kcQ5yAGtrk37EXtT9/nXhT+rmTsg/IHc99ZEul/4wbUzKPRul+eAmsCFGYeM5ohqdM8QiEs2 hmRhdT1CDdzsbqTD3WA6rOTqjD0Mi8QRYMfWcMaZVU3zoi8nb8ysh/0apUzDpGz1/7NNC6ll lhmsxMCr7kUiMcK0YCy8lbGny+gq/D1ougdtlW/soWNvlMRWWK1W7FE/2Q3+hqpEWp0ZlyIv XxBkM/H6ukLVMiKkC+LGr1SR/eu+uqPNyDajRh3BZ49+j+x+nmlO4dN/DV5I0QvOcEBEdMIX KMxkVwNjHOwFCLwBUOSX25XI5hzpUQHPYi+Ps04lvIUPvBMmPavpUmCn3K40WH3i1QLmqoiI 5qdesvEJS9FU/49nGbmHLxEgeVDKsUCKYX7FcGTI/OPgev2WZJpYelfagvmgh0RsP3b/F6Fq 4Y32zWilE0DALWmCsUozWLjBQtRdyRkbXwHg8lWffSEOQ1oBCkqDOXJqY7NiKQ095m5Ytzgp ynnMmcBkASXrSSedW2iNCo/AJuxBswXhSxgYkQR0aOAgCVLjXCHt/tEKPPavNAPqIRe8BKDZ 6BcI53dWKkSE2WvFvZ0RcCVkbGOvS+D3WqmVxdJqhBmF3K5b1WRpoW2TRil7yQUECu8uO03p rDqhEuRQoMOS04mRIzaYe6mhQH593UMuvNAb22RKPlqeWLo7NdLLQ71haQJOM0iE0jI6Qab8 Ae0Oi0mg9fxjbU7y/T3oJyVjpyIFrJ+F3VKHmOA4reRMzLbz1WZwoRBcbipfm33aF/Z6IGfQ 91w9KjiAfg6gVwRjdJNFucyx6cH+tDPhaFW4TpmEFrPcV6qV61sEkOd15MerIlI4KFTgiqte 0e14tIBE664CMDkN18wJQQeceWI088PqATS9fgYJEbb5jd92aiuCGF+HkCrozNMCql2K6Ynz vURg9EX4AmBlRYaCNaKoSRK/WCqLHZbcaEYmrwFIY3smCw540pjZMHCNyrI/52/UdVAHU00K DuyhqCZpbB9xFLHQkUjB0r2wutRqpQfii9klGZYCQyypePEofsr0Dl60zc9FF1Vxyoa9dNDA DFgMkktKJie+zttutN4YFmtPAN8HzycxF36zgoYtW/eTnTwbFf3Ek8GBb+v8nwaokVmRRoK2 JGDyW3gbyTmQ9Gp4As2RnxeiqLCSf5fy1T8vf6JTuW/Mbs0Wz7HupOVRHEprkLnCPwhhUecq uhN+v1xWJLBNiURgvMaDomE2ZtJSBm7O3FzG6B93aIWHFPzfCO59iiOJnuQJOJMBa3u2m2pB /N+IvlgU0yF6x+PiTQAFIgwLKRRjtdwwPYjIZbvfXUntZmbpRpX6KPgzDD03jIXco8/gPQDJ ZP0XBPcN36bml9/uXLH9etAMUqGOeg0XhX2hr2Jwb9YBqA4kb9edG8p2eGJpFSTCgxs+iyUs C7lZ6P7y+9Dy5xmr7DzE5dsVhmFFtfuaNumqAyDkcxCTdfqA/f8swk4rlrGPQMPGZAzX99xt 6qGsf+p/UfjkYs1bVvkmMi6J/EU3fmxYetZCdKoDX94mSDZZtTgzSFe8E+FKLtIsuhn2O+Ze yWCZvGNKOElA+Vm+CUNagx1MQosNKDsX6Kx+QK/t6utDzYe4yzmLfSm13jjNltHRxAMILn7L BH+gNe1x9VitI8XLgQ1N/JnJJ5ZIVHYRqotcePqhwSYFmWFhlCjuKPosBgdtRXnL2aiK9nrx 4DnSjzVVgWAiIuRwP5364VN7wAqVlBjiuwOT2ch0t9RiRXhKUUZLO4YYK40OrsNngPcjJjHN SzwNk08AiDAXBNBQxX2wPLneiy9XuUuGNPIFgYFznOuSRWdJd2/WeN61yJa/X1JVCPpz7inJ fEg63TABEWN7a8zd9kDxM6QoLlB/ezb9EIq6Eqmss3VAjQiO5so+kFlPjJwUX3gL5mQumTNf GQ7fDURCgXzA0v8Ct1pdHNpCQkU9mGnhSkhaSCUhs3TocOHxelH0+fyIPz3zqZFVskROboSX jnicgNhOYxNNqA75cPFeu7FgJOYzdqtN+3jderIYlRXmKu9rGM6I8kFgCwDCtk4/xJSGE/ck T/q5GUiAEOCKwZa37j+JcAh5cdqSnxVZ93WpFeXmNMEuUVRIxvll9yCzAXnLJjxr+7ouEAwr PI6chOKu1PP3Nf7jWAWixnYz2BrxekREmXBWyEsCJj1l39AjYOb+K9JiykH6j6azJGIKki4u kpcPxXRNb9Lhh+y4j0=
- Ironport-hdrordr: A9a23:lSjHyKwLmA+paDySDStFKrPx7uskLtp133Aq2lEZdPULSKGlfp GV9sjziyWetN9IYgBZpTnyAtj6fZq8z+893WB1B9uftWbdyQ+Vxe1ZjLcKhgeQYhEWldQtnZ uIEZIOb+EYZGIS5amV3OD7KadH/DDtytHKuQ6q9QYJcegcUdAD0+4WMGamO3wzYDMDKYsyFZ Ka6MYCjSGnY24rYsOyAWRAd/TfpvXQ/aiWKyIuNloC0k2jnDmo4Ln1H1yzxREFSQ5Cxr8k7C zsjxH53KO+qPu2oyWsmlM7rq4m1+cIh7N4dYCxY/ouW3TRYzWTFcRcsoi5zX4ISLnG0idorD CDmWZjAy050QKqQoj8m2qR5+Cn6kdk15fvpGXo/UcLjPaJMQ7SMfAx8b5xY1/c8Q4trdt82K VE0yaQsIdWFwrJmGD468LTXx9nm0KoqT56+NRj+UB3QM8bcvtcvIYf9ERaHNMJGz/78pkuFK 1rANvH7PhbfFuGZzTSv3VpwtarQnMvdy32NXTrkaSuokdrdPQT9Tpr+CUypAZyyHtmceg02w 3tCNUZqFlvJvVmE55AOA==
- Ironport-phdr: A9a23:vEabCR3iI9vuMZlnsmDOJQwyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeHo6oxxwGTFcWDsrQY0buQ6/ihEUU7or+/81k6M6ZwHycfjssXmwFySOWkMmbcaMDQUiohA c5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/I RuqoQnLtMQbjoRuJ6cvxhDUpndEZ/layXlnKF6Nmxvw/Nu88IJm/y9Np/8v6slMXLn1cKg/U bFWFjMqPXwr6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4 LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8FeWTFcAoOnd 4sAEfYOPfpWoYn6olsBtxq+BQ+xD+/rxTJFgnr60Ksn2OojDA7GxhQtEdIQvnrJsNX7OqQcU e63w6bUwjrOdOlZ1Svh5IXSbhwtvfOBULRtesTR00kvEAbFg02Up4P/JDOV0eINuHWZ4ep9S OmijGAnpBxxojmu3ccglJXFip8Jxl3f9SV5x5o1JdiiR056Zd6oCodftyafN4ZvRM4pXm5nt jogxLIcpZ67YDYFyI4hxxPHafGKcIiF7xL+WeuePDt2i3BodK6/iRuw8EWt1uPxWtW73VpXo SRIjsfAu3IM2hDN6cWKRfhw80mj1DqS1A3f9OdJKl06m6rcLp4u2L8wlpwLvETMHy/2hEX2j LKNeUk+++io7PzrYrrnpp+AN490lxrxPr4ylcy4BOQ0KhMOX3CB+eS90r3j8lP2QK9QgvIql anZtZbXLtkYqK6hGwJY3Zov5wy7Aju4ytgUgHoKIEhHdR+Jl4TlJVDDLOz2APq6nligjCxky vHDM7DhH5nBMn3OnKrucLlh7kNRzQg+wNZC7J9KDrEBPenzWlPvu9zCExE5Mg21zPj/Bdlh0 I4VRHiBDbWDMKzItF+F/uIvLPeIZI8SoDvzM+Qo6fnzgXMkgFMQY7Cn0YYOZHC/BftpPV+VY X3xgtcdCmgKuRc+TOr3h1GYST5TfXGyX74i6T4nFIKmDIDDRoa3jLyGwSe7AplWZmdBClCPC 3vna4KEW/IUZCKTJM9ujCAEWKCuRoM9zx2jsBH2x6B6IufX4CEVt5zu2MBw5+LJlBEy8TJ0D 96a02GIV2x0kH4HRz833aBkv0Bx1kqP3bRjjvxYEtxT+/ZJXR07NZ7Y1eB1F9fyWgfZctePU 1mpWs+mDi0pTtIt398OZF5wF8i6ghDZwyWqG6MVl6CMBJEs7q3c2GHxK99hxHbCyakulEIrQ tBPNG2jnq5w7RLfB4/Pk0WDlqalb74Q3CDX9DTL8W3b9kpfSUt7VbjPdXEZfErf69rjrAuWR Li3TL8jLwFpyMiYK6IMZMe/3ntcQ/K2Gt3FZGT5u3r4URiExqGXNtKzI00d2znYAUkA1QsU+ CDVZkAFGi69rjeGX3RVHlX1bhawoIGWyVu+R04wlESRalF5kqGy4lgTjOCdTPUa2vQFvj0go nN6BgX1xMrYXvyHoQcpZ6BAeZUl+l4S227ZpRcnZsX4B6BlmlsXcgAxtETrhF1sEosVqcExt zsxyRZqb6eR0VdPbTSdiJ78Oq/McDGrpDivbLLT01Dalt2R//RH8+w2/m3qpxrhDU8+6zNn3 t1ShmOb/YnPBREOXIjZdG8SrkE/jJaDJy436sXTyGFmNrSyvnnawdU1CeA5yxGmOdBCLKeDE wy0GMofbyS3AMotnVXhLhcNPeQJsbUxI9vjbPyenqiiIOdnmjuiy2VB+oF0lEyWpWJ6TabT0 pAJzuv9vEPPXirgjFqnrsH8mJxVLTAUEG2lzCH4BYlXLqRsdIcPAG2qLoW53NJ7z5LqXndZ8 hakCTZkkIendRqAdAalhFV41UMLpHWmnW2zyDk12zAlo6yD3TDflvz4fUlPMWpKSW9+yFb0d NTsyYFAGhH4KVdyx37HrQ7gyqNWpbpyNTzWSEZMJG3tKn16F7C3rvyEatJO75UhtWNWVv69a BaUUO2YwVNS3iX9Em9Z3D1+eSutv8CzkRB6mnnHdC8rhHreZcR5xBOZ79vZD600vHJOVGxjh D/bC0Lpddel/cePzc+a6si+UH6kX5xXNyLsyMnT0UnzrX0vChq5kfepn9ThGgVvyi732e5hU iDQpQr9aI3mv0ijGdpuZVIgRFr16s4hX5p7jpN1n5YIn34TmpSS+3MD12b1K9RSn6zkPjIBQ jsCwtid5waAugUrIH6J1ZmjDizF6stme9yzY2dQ0SU4p8xHE6ab6rVYkDA9/gL+/FiXOKg7w WxVwOBm8HMAhuAVpAchq0fVSqsfG0VVJ22klhiF6cy/sLQCYW+udbaq008t1dulDbyEvkRdQ COlItFzR2kpvoMgawGpsjW78IzvddjOYMhGsxSVl0yFlO1JMNcqkeJMgyN7OGX7tHljyughj BUo04vp2erPY2hr4q+9BQZVczPvYMZGsD/hjbRFxJ7Ph6ivGYlkEzQPGpDvSLj7dVBa/eSiL AuIHDAm/z2VFbrNBlXHsR9Or3XTFpmqMzecI3xTnrAADFGNYUdYhg4TRjAzmJU0QxuryMLWe 0B8/jkN51T8p0gE2qdyOhL4SGuauBawZ2J+Vs2ENBQPpFInhQ+dIYmE4+l0BS0d4pCxsFnHN DmAfwoRRWARBh7ZXRa6ZuLovZ+YtLHHTuumc6mXOenI9bMYD7HQgsvwt+kutzeUapfTZj8zV btjnBIEBC4xGtyFyWxXF2pLyGSXN4jD403nsixv8pLmqKitBF2pvNPfTeMVa44KmVj+gL/fZ bfI2GAldnAHi9VUgiWUgLkHgAxL030oK2brTO9G6HaKFv6Ym7cJXUQSM3ohbZIRvaxghlEfa 4mH2raXnvZ5lqBnUV4dDA64w5j7a5BSeDPvcw+WTEeTaubcLGWSkZiuOPGyFeUL3rUM70Xi6 3HGSyqBdnyCj2e7DRn3aLMV1XjJMkAG49O2Kk41WzqkEYuuawXlYoV+1WRkmORt1H2WbTVOP 2AkKxEf6eDKpWZRhvE1c4BYxkJsNvLM2yOQ7u2Db40TreMuGSNs0eRT/HU9zbJRqiBCXv183 iXI/JZipFSvk+/HzTQCMlIGsjFQmIeCpllvI43/37wZADPv20tI6m+dTRMXu9FiF9vj/bhKz cTCn77yLzEE9M/I+cwbBI7fL8fiUjJpPRfyGTHSBRcIVnb3bSeO3QoEwLfNrTWctdAip4Lpm YYSR7MTT1EzGv4ASwxkENEEPJZrT2YknLqc36tqrTK1qBjcQtkfv4iSCqrUUK+pcWbf0uIXA nlAian1JokSKIDhjklra10h2Z/PB1KVRtdV5Ctocg4zpkxJtnl4VGw6nUz/OWbPqDceE+C5m hkuh05we+MooX3i71clPQCS/XMYkE4tnNzkhXaadzu7f8LSFclGTjH5sUQ8KMaxWwFucQi7h lBpLh/ibpcI1v5LUjkujwXR/5xSBfRbUKtIJgcKwu2abOkp1lIarTi7wUhA5q3ODp4ox25IO da86nlH3Qxkdts8I6fdcbFIwlZnjaWLpia01+o1zVxWNwMX/WiVYiJNpF0QO+xsOX+z5uI1o 1/n+XMLaC0WWvEtuP4v6k4tJ7HK0Xf7y7AaYkGpa77Dd+XI4S6Y05bPGw5411tUxRUdu+Euj oF7NRLTDh5KrvPZFgxVZ5eYb1gNN4wKsiCUJHrGsP2Rk8stY8PhSaawC7fJ7flcg1r6TlwgR 91et51YTJfwiBmKf4C7fNtngV0s/Fq5flzdVaYQIUvZnmtf+JPti8MmlYhFeGNHCD0kY3zuv +TZ+ldx0qrbBI9kMDBHB+5mfjo3QJPowScB5iYZVWDl3L5Bk1qJt2ek9HaXUWC0bsI9Nq2dP Uo+UYjvqztjq/PkhwaPqseMYDygfZFrvtuFgQv7j7CuLqoNCJJa6gLbkYQeQGG2WWnSF9LzP 4L3d4Qncd3zDDC9T0C7jDU2Ccz2OYT0RkBnqQHvWYNdsY3d1zcmZ5bV/tQ2GxBsougC4OR3Y ghRO/IG
- Ironport-sdr: 66a8e7c6_WQcB55EwN18Ptwkeb5GEcURrIjkoTIrLMNXWyK2d9RRpgjO azIbIN77tmCpL3RiAABem3KiCsFRA1RGchk1N1w==
- Msip_labels:
Thank you for all your pointers! Exactly what I was looking for!
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of James McKinna <james AT fixedpoint.org>
Sent: Tuesday, July 30, 2024 2:15 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] HTML output that remembers proof states step by step
Sent: Tuesday, July 30, 2024 2:15 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] HTML output that remembers proof states step by step
Proviola? https://github.com/coq-community/proviola
(Apologies for self-citation!)
Sent from my iPhone
On 30 Jul 2024, at 04:13, Jason Hu <fdhzs2010 AT hotmail.com> wrote:
Hi all,
I vaguely remember someone's Coq HTML artifact that remembers all proof states so that I was able to inspect proof step by step in the browser. I don't seem to find anything on Google. Do I remember it incorrectly? Any more verbose output than what coqdoc already provides is appreciated.
- [Coq-Club] HTML output that remembers proof states step by step, Jason Hu, 07/30/2024
- Re: [Coq-Club] HTML output that remembers proof states step by step, Julin S, 07/30/2024
- Re: [Coq-Club] HTML output that remembers proof states step by step, James McKinna, 07/30/2024
- Re: [Coq-Club] HTML output that remembers proof states step by step, Jason Hu, 07/30/2024
Archive powered by MHonArc 2.6.19+.