coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jim Fehrle <jim.fehrle AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] add Search functionality to ltac2
- Date: Fri, 3 May 2024 10:50:15 -0700
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f46.google.com
- Ironport-data: A9a23:o7q9rKoXi39eO/8pl5ER+qk0VdpeBmKGYRIvgKrLsJaIsI4StFCzt garIBnXO6mLMWX1fdB3YNjk8hxS7ZCExt5kT1drrHpjRClH9uPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKiefHoZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGjxSs/3rRC9H5qyo5GtF5gdmP5ingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYj9yuuuTnuUiG9Y+DCDW4pZkc/DKbitq+kTe5p0G2M80Mi+7vdkmc+dZk 72hvbToIesg0zaldO41C3G0GAkmVUFKFSOuzdFSfqV/wmWfG0YAzcmCA2kkNqgVoOJPEV1Cr 8BIMGsyRSqtmsmPlefTpulE3qzPLeHuNYIb/3VulHTXUahgTpfETKHHo9Rf2V/chOgURaeYN 5dfMGQwKkieC/FMEg9/5JYWnuatwHfycydcpXqaoKM25y7YywkZPL3FYISOIY3RFJw9ckCwl HCZ+TvFPUojF+ObziOhyGOFltL0tHauMG4VPOblr6Y10QP7KnYoIBYRTB6wpeSzolWvXspWb U0S4Csn66YonHFHVfH4Vhy85XqK51sSB4QWHOo95wWAjKHT5m51G1ToUBZTY/kr7ssOVQAmj GPZh4jWLgZBrZasHCf1GqivkRu+Pi0cLGknbCACTBcY79SLnG3VpkKfJjqEOP7q5uAZCQ3NL ya2QD/Sboj/YOYO3qS/uFTJ2nei+saPQQky6QHaGGmi62uVhbJJhaT5sTA3Dt4Zc+51q2VtW lBax6ByC8hQVvmweNSlGrllIV1Qz6/t3MfgqVBuBYI90D+m5mSue4tdiBknex41bJlYJ2G2O BaP0e+02HO1FCv6BUOQS9LhY/nGMYC5SLwJq9iNMoQTP8ctKGdrAgk1Ox7MgwgBb3TAYYlkZ M7DLpfyZZrrIatgyzWySq8c17Rtrh3SNkuCLa0XOy+PiOLEDFbMEeltGALXMogRsvnYyC2Lq I03H5XRm31ivBjWOHa/HXg7dgBUcxDWxPne96RqSwJ0ClA2RDh4VqeMmelJlk4Mt/09q9okN 0qVAidwoGcTT1WeQelTQik7Mu29boU1tn8hIy0nMHCh3nVpM87l774Se9FzNfMr/fBqh6w8B fQUWdSyMtIWQBT++hMZccbcqq5mf0+Vng6gBXeuTwU+WJ9CfDb33OHYUDHhzwQ0NRrvh/AC+ +Wh8ij5Xas8Qx9TCZeKSfC3kHK0k3svuMNzeErqJNNsVl3m29VoIXapj9scAcIFGTPczBS0i ieUBhY5o7HWgokXqdPmu4GNn72LIcBfQHVIPjD8xqmkEAXn5Uyf+J9kfMfUWCHCRUX21b6HZ +4I/8rjMfYCoklGg7B8H5lv06g6wdnl/J1e8ShJA1TJaEaNGJp7A3zbw/RKiLJB9oVZtSSyR EiL3NtQYpeNGcH9FW8uNBgXVfuC2d4Uiwvtw6wMemui3xBO/Z2DTUl2FDuPgnYELLJKbaUU8 d14s8sSswGCmh4mN+idtR9t9kOOE2chVps2vZRLEa7pjQsWkmt5W6L+MROvwp+zaIRrCHIIc xu0n6vJgopOynXSK0QTEWf/5ssDpJAsli0T8no8CQWnpt73iMUz/iVtyhUsbwEMzhx4w+N5Y WdqEEtuJJSxxTRjhekdfmWgBzB+AAa9/2rvwWAoj0zcdVGjDUbWHV0+OMGM3UEXyH1ddT5l5 4OlyH7pfDLpXcPp1A4wZBJBh9n8a+duryvutduCHcuXO7UbOx/enb6Id24EjzDFEPEBrhTLi scy9dkhdJChEzAbppMKLrWz1JMSbUuhD3NDS/Qwx5E5NzjQVx/q0AffNn3rXN1GIsHL1kqKC 8ZOAMZrfDbm3QasqgErP4I9E4VWrtUIuuVbIqjKIFQYuYSxtjBq6ZLc1hbvjV8RHulBr5wPF ZPzRRmjTEqrmnpmq03cppJlO025Q+U+Si/S4eSXyNgNRrU/6LxCUEdqybalnWSnAC0+9TKug Q7zTav3zetj9IdSo7XRAphzXwWaFf6jVcCj0hyCjNBVXNaebebMr1w0r3fkDSR3PJwQechGq rCWlOHn2Wb+5bMQf1HEqcPQCZsT9cGWWcxJOPnWN1hfpzOJA+X30isA+ke5CJ1Hq8xc7c+ZX DmFaNO8WNoWetVFzlhHQnJ6PzdELIqvdYbmhye2j8rUOygnyQadce+Wry74X19UZgojGsPYC Datn92M+9oBjoBHJCFcNsFcG5UifWPSA/o3RebQ6wudIHKj2G6Zm73YkhEl1zHHJ1+EHOv+4 rPHXhLOTwuzio6Z0OBmt5FOgTNPAEZfmeUQemcvy+xygR2+D08EKr05GrcCAZd2jCfz9c/ZY BfgUWgcMhj+DA90KUjE3NfeXwmhX71Efp+zIzEy5EqbZhunHI7KUvMr6i5k5GwwYTf5iv2uL dYF4HDrIxyt2ddTSP0O4uCgy/JSrh8AKqnkJWim+yAzP/ofPVnO/HloHQ4IUSKeVs+RygPEI m86QW0CS0a+IaI0/QCMZFYNcCz1fhu2p9nrUctL6NnasoSfiuZHzZUT/snth6YbYp1iyKEmH BvKqqjk34xS8nMWsKot/dkuhMeYzB5N8teSdMfeeOHZo018BqnL8S/PcerjgfzOIDJiLm4=
- Ironport-hdrordr: A9a23:NbG/SKOV38sxucBcTvijsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZEmPHPP+VQssTQb6LO90cq7IE80l6QFhbX5VI3KNGLbUSmTTL2KhrGSpAEIdReOkNK1Fp 0NT0G9MrDN5JRB4voSKTPXL+od
- Ironport-phdr: A9a23:+UnS+RROvdKr6BwKm8+90DqkHdpsokqVAWYlg6HPa5pwe6iut67vI FbYra00ygOTDMOBsaoP0rOK+4nbGkU+or+580o+OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF 95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba12I RmsswndqNUajYR/JqosxRbCv2dFdflRyW50Kl2fmArx6N238JB/7Spbpugv99RHUaX0fqQ4S aJXATE7OG0r58PlqAfOQxKX6nQTTmsZnBxIAxPY7B7hRZf+rjH6tutm1yaEO8D9UK05Vi6j7 6dvTx/olTsHOjsk+2zZlsB8kKRWqw+nqhdiwYDbfZuVOeJxcaPTf9wURWRPUMVMWSJfHoyxd JEAA/YbMOtCs4Xxu1kDoB2jDgesHuPvzTpIi2fy06071uQqDAHI0xIgH9IUtHTbssj+OaAQU eC0yanE1zvDYO1W2Tfn7IjHbAssof6JXb1qcMrRzVMjGB/CjlWVsIHoOS6e2esRvWaB9eVgS f6vhHA9qwF3ujWixscih5XHi44Lyl7I6Dt1zoYoKNC7VUJ3fdypHZtOuiyeN4Z7Qd8uTmVmt Ssm17ELu4O2cSwWxZg7xxPSb+CKfo6V6RztU+aRJC13hHNjeL+nmxmy9lKgyuviWcmw1FZGt DRKncTRtnwV1hzT7NKHSvpn8Uu71zaPzQbe4fxHL0AsjafXNYItz7oqmpcQsUnPBDL6lUT0g aOMeUgp++6l4Pn5b7Xiu5+cLJN0hR/kMqozm8y+APo3PxASU2Wd5O+yzqfs/VfjT7VPlvA2k rfWsJTdJckDo662GQ5V0oI65xa7ATeqzc0UnXcIIV9EYh6HgI/pO1bBIPD8E/izmUijkDBux /zeP73hBIvCLmTbnbv/Ybpw71RQxQkzwNxF+p5ZC7MMLOj8V0LwrNDYCwU2Mw2ww+bpEtV90 YYeVHqNAq+YNaPeq1GI6fwvI+mWYI8api3wK/cg5/H0jH85nUURcrWu3ZsScHy4GO9pLF2DY XXwmtcBDXsKvg0mQeD3kFGCSyJcZ26uX6Ig4TE2EJ6pDYDaRoy0nLOB2Dq7EYZNa2BdClGMF G/oeJ+eV/cNbiKSOM5hnSYeWbivUY9ynS2p4QT90v9sKvfe0iwer5PqktZvtMPJkhRn1z1xR +qQ03uJQikgnGINATE73Lp7rGRyz16C1e5zhPkORo8b3O9ATgpvbc2U9Od9Ed2nAmopH/+MQ VeiGZC9BC0pC8k225kIalp8HNOrilbC2TCrCvkbje/DH4Q6p4Tb2XW5PMNh0zDezqB0jVgjB MVCNXeii4Zw8gHSA8jClEDK372ye/Ek1TXWvHyG0XLIuUhZVABqVqCQX3EaIEXbrc7962vNS ravDfIsNQ4SgdWaJP5sbdvkxU5DWO+lONnaZDepnHysAB+T2r6WRI/jemFY2CuETUZYzUYc+ nGJMQV4DSCky47HJBppE1+nI0bl8O0l7Wi+Uldx1AaSKUtoy7uy/BcRw/2aUfIamLwe6m8nr H1vEVCx0sizaZLIrhd9fKhafdI24UtWnWPfuQtnO5W8LqdkzlcAegVztknq2l15EIJF2cQtq XorykJ1J8f6mBtDdjbe053wILnaAmb39RGrLaXR3xCW0dqb/LsO9OVts0/q70miEksv9Wki0 sEAiSPNoMWXSlNMDtStDBVSlVAyvbzRbygj6pmB0HRtNfLxqTrew5cyA/NjzB+8ftBZOafCF QnoEsRcCdL9TY5i01WvcB8AO/hfsaAuOMbzPfmH3eilMeZ6mD+OgmFO4YQ72UWJvXkZKKaAz 9MezveU0xHSHTX9iRGvv8DtnY1sajQbH275wi/hTt00BOU6bcMADmGgJNeyz9N1isv2WnJWw 1WkAksPxM6jfRf6g0XV5QRLzgxXpHWmnXD91Dloi3QyqbLZ2iXSwuPkfR5BO2hRRWAkg02+a YSzitkbWgCvYW1L3FOn5EO8yaVbvqByB2bWSEZMOSPxKiluX7CxubyLf8NUoMlw4GMHDaLlP w/cFuC1qgBSyy75GmpC2D03ElPi8o70mRB3kiPVLXp+qmbYZdAlwB7e4NLGQvsCljECRSR+l XzWHg3mZ4jvrYjSzsmc9LzgBAfDHtVJfCLmzJ2Nrn6+7GxuWlikmuyr38bgCU482DP60N9jU WPJqgz9a8/lzfffU6ovc092CVv788c/FJt5l956hpAVn3YXho+R8FIIlG7yNZNQ3qe0Px9vD XYbhsXY5gTowhgpLHOMgYz0Vm+Zz+NuYtC7ZiUd3Sd3vKUoQO+EqbdDmyVyuF+xqwncNON8k jkqwvwr8HcGgusNtVll3mCHD7sVB0UdIT30mkHC8YWltKsOLjXKE/D4xA9kkNumFr3HvgxMR COzZMI5BSEppsRnbACXjTuqu9miIoWPK4pU7EHckg+c3bYJbshqzbxT23IhYSWk7BhHg6Y6l UA8g8/85dDdbT0rpOXjWlZZLmGnOZ1VoG28y/YG2J7RhdjnH409SGpRGsK0C6v5SnRK8q23U mTGWDwk9iXERfyGR1LZsAE+6CuRW5GzayPOfClflIo9AknbfAsF2UgVRGlox8FiUFn7mIq5N h8+v250hBawqwMQmLgwZl+vDyGG/lfuMnBtF9CeNEYEtFgcoRqFd5XPtKQrWHgJtpy58F7Xc zLdPV8ZSzpTHBTDXgGGXPHm89DE96Lw6vOWCfzIbP3OrOVfU6zN3pezys59+C7KMMyTP35kB vl920xZXHk/Fd6L0zMIAzcakS7Adav57F+15zF3o8aj8f/qRBOn5I2BDKFXOMlu/Bb+iLmKN uqZjiJ0YThC0ZZEyXjNwbkZlFkc7kMmPyGqCqgFvDXRQbj4n6ZWC1sfZXo2OpcWqa072QZJN IjQjda0nr90g/gpCktUAFzsnsb6AK5Ca2q5NV7BGAOKLOHcfWyNk5yxOP3jD+EO34A2/1Wqt D2WElHuJGGGnjjtDFW0NP1UyTqcJFpYsZ28dRBkDS7iSsjnY1u1KowS73V+zLsqi3fNLWNZP yJ7dhYHrLyVqy1Vgu97FkRO63NkKa+PnCPTvIy6Yt4G9OBmBCh5jbcQ+HMh175c9z1JXtRwk SrW69pg+hSozrfJxT1gXx5D7D1MgcjY2CcqcbWc/Z5GV3He+RsL5mjFEBUGqexuDdj3srxRw NzC/EoSADJL8taR+cVFQsaIdoSIN30uNRevEznRXlNtpdGDOmTWhkgbm/aXpCT9Rn0SpZ3lm Z5IQbheBgRdKw==
- Ironport-sdr: 663523e4_mpBJN8xV68I1ydZqKkA++0Pf5K+VjMCsxMgNzNdcgD4LRwI 0dck1OphfsbHZ4xvA4VA+qH+naXwNzbk46xR8ZQ==
Can you be more specific about what you mean by "Search functionality", which is vague? I don't see how your examples (smart IDEs, serializing for LLMs) fit into search.
Jim
On Fri, May 3, 2024 at 4:55 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
Another use could be to automatically find relevant lemmas to prove a goal, without needing to add to hint dbs, and potentially emit a primitive proof that can be checked faster later.On Thu, May 2, 2024 at 2:47 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:How hard would it be to add Search functionality to ltac2?
Has somebody already done that?While developing smart IDEs, this would let us push more functionality to ltac2 rather than having to implement it in elisp (emacs)/typescript (vscode) and have different versions for each IDE.My concrete usecase is to take an iris separation-logic Coq goal and serialize it for consumption by LLMs.I would like to implement all of it Ltac2. `Search` API could be useful to feed the LLM relevant lemmas about the constants mentioned in the goal.In some past projects (e.g. https://sympa.inria.fr/sympa/arc/coq-club/2023-10/msg00026.html),
I found it much easier and less error-prone to write most of the logic in ltac2/ltac rather than in elisp.-- Abhishekhttp://www.cs.cornell.edu/~aa755/
- [Coq-Club] add Search functionality to ltac2, Abhishek Anand, 05/02/2024
- Re: [Coq-Club] add Search functionality to ltac2, Abhishek Anand, 05/03/2024
- Re: [Coq-Club] add Search functionality to ltac2, Jim Fehrle, 05/03/2024
- Re: [Coq-Club] add Search functionality to ltac2, Abhishek Anand, 05/04/2024
- Re: [Coq-Club] add Search functionality to ltac2, Jim Fehrle, 05/04/2024
- Re: [Coq-Club] add Search functionality to ltac2, Jim Fehrle, 05/04/2024
- Re: [Coq-Club] add Search functionality to ltac2, Jim Fehrle, 05/04/2024
- Re: [Coq-Club] add Search functionality to ltac2, Abhishek Anand, 05/04/2024
- Re: [Coq-Club] add Search functionality to ltac2, Jim Fehrle, 05/03/2024
- Re: [Coq-Club] add Search functionality to ltac2, Abhishek Anand, 05/03/2024
Archive powered by MHonArc 2.6.19+.