Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] automatically running proof-process-buffer at emacs startup

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] automatically running proof-process-buffer at emacs startup


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: Stefan Monnier <monnier AT iro.umontreal.ca>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] automatically running proof-process-buffer at emacs startup
  • Date: Thu, 29 Jun 2023 07:51:15 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f54.google.com
  • Ironport-data: A9a23:X+NjwKCFutVbKxVW//7nw5YqxClBgxIJ4kV8jS/XYbTApDt00jYOx jcdWT2Daf+ONjf8KdolYN+08hwP6sXUz9NgOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHYTdJ5xYuajhPs/zZ+Us11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc50CafX/V6NV/NlkZHaI69+pFBjhsp fNNfVjhbjjb7w636LeyS+0pmd56ace2YMUQvXZvyTyfBvEjKXzBa/+StJkIgXFq3JkIQKq2i 8kxMVKDaDzJaR1OIVcaC9Q3mu6uij/+ciFXgF2QrKszpWPUyWSd1ZC0aYePJIHWHZ89ckCwh 1zs8lnIDQEmH/O6lgW0+ViMrb+MpHauMG4VPOTgqqQCbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72SuR9j5GgKi+TuK40JaVN1XHOk3rgqKz8I4/jp1GEAJEjBFUfcGpfUuahwF9 FKFrdSwJ2xg5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiNFj5v4oZoYzeJNZnuEZChmrn G/X9HlWa6E7yJ9Uh//irDgrlhr1/sCRJjPZ8Dk7SY5M0++UTIusZojt9kKCqPgdcMCWSV6Ou HVCkM+bhAzvMX1vvHzUKAnuNOvxjxpgDNE6qQA0d3XG32r2k0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvW5t7kve4T4S8CK+8gj9yjn5ZJF/vEMZGNR744owRuBVEfVwXY 8fFKp3zXR7294w5kWLrLwvi7VPb7nlmmTm7qWHTwBOg3r6TDEN5up9UWGZimtsRtfveyC2Mq 4g3H5LTl313DreiCgGJqtV7BQ5RfRAG6WXe8ZM/mhireVo4RgnMypb5ndscRmCSt/UJx7qSo izhAie1CjPX3BX6FOlDUVg7AJuHYHq1hShT0fUEbA3wiUswK52i9rkefJYRdLwqvr4rh/1tQ vVPP43KDv1TQ36Vs34QfLvsnrxELR6LvAOpOzb6QT4de5U7eRfF1OW5dSTS9Q4PLBGNi+0An 5Oa2Dj2f78/ViV5LcOPaPuQ31K75nccv+RpXnr3GNpYeWSy0Y0zKyXOkeM7eOAcDSrynx2xi gCcW0Yer8bwvr5vocXohL+FnaitAeBRDkpXJEiFzLeUZA3x3Huv/p9Ea8mMJQvibWLT/L6wQ Mlk1NT+DaE3p0lLuI9CDLpb96IyyN/xrbt8zA4/PnH0Q3m0K7FneF+q4NJus/BT+7pnpgeGY EKD1d1EM7GvOsm+MlowJhIgX9uTx8MvhTjewvQkEnrUvBYt0uK8bnxTGB2QhAh2Drh/atoly Nh8nv8m0VW0jx5yP+uWiixRyX+3EUUBdKcZ57U6G47gjzQ5xm5SOaL8DjDE27DRStFuHHRzH BqqqvvjvZp+yHDGUUIPLlnW/O8EhZ0xqBFAl1ADAFKSm+v6vPw83TwP0DE7UjVqyg5j1sRtM FNKLGxwH72FpB1ztfhAXketOgBPPwKY8UrP0Gk0lHXVYk2rd27VJkg/BLqp0GUG1VlDJx530 aq9ymn3dRrLJuTKwToUS0ppj9fBXO5B3FTOt+7/FvvUAqRgRyTuh5GfQFYhqjzlJJgUr1LGr +w7x9RAQ/T3GgBIqpJqFrTA86obTS2FA2lwQftB2qctNkOEcRGQ3Qm+EWyASvlvFdfrr3DhU 9dPI/hRXSuQzCyN9zAXJZAdKo9OwcIG2oAwRaPJF0Un7Z2v9iFkobDBxBjY3WULeehjoew5C 4HWdg+BLFCuuGtpqzfzi/dAa0WFYogiRQzj3eqK3v0DOLAdvcpNL0wj8LuGkE+EEQlg/iDO5 QPKWLDL/rYz1aVtgIrePaFRDCqkKd7Idbqp8SLil/9sfN/wIcP1mAdNkWbePiNSJqo3Z9tss Kak6frb4Rvgh6kndEz8gLyDJrltyeTpe9QPKePxDn1RvRXaaf/W+xFZplyJc81You1S9uyMZ lWdesCvUfU3Rt0E5nleSxYGIiYnE66tM5vR/3Ksnc+tVCoY/xfMdu681HnTampeSC8EFrv+B iLwuNes/tpol5tNNjBVG8BZB4JEH3G7VZsEb9HRsRyqPlusiH6GuZrgkkMu12iaQD3MWsP3+ onMSRXCZQy/8vOAhs1Qt4tp+AYbFjBhiO03ZVgQ4MNylyv8NmMdMOABKt8TP/m4SMApOE3QP 1khrVfOCBkRmRxBeBT4pcv5B0KRW7BINdD+KTgkuUiTbk9awW9G7KRJrk9dD7VeI1MPD91L7 fkR/3TxOl66xZQBqSM7+Kmgmek+rh/F7itgxK0++vAexz4RBLwL0DpqGw8luekr1S3SvB2jG FXZjlyojK12pYAd3Cqgl7No9MklgQ7S
  • Ironport-hdrordr: A9a23:pJ1oAqMbVbdti8BcTvqjsMiBIKoaSvp037By7TESdfUnSL38qy nOpoVj6faaslYssR0b9OxoW5PwOU80l6QFgrX5VI3KNGKNhILCFu5fBP7ZogEIbBeRygcy78 tdmuNFebnN5BBB/KHHCSeDYrAd/OU=
  • Ironport-phdr: A9a23:23GVSxWXKqN4eauB/mWb/ij2jQLV8KzQXDF92vMcY1JmTK2v8tzYM VDF4r011RmVB9uds64P17ae8/i5HzBavNDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+I v5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vI BmsogjdqMgbjZF+Jqs+xRfErXRFcPlSyW90OF6fhRnx6tmw8ZJ57yhcp/ct/NNcXKvneKg1U bNXADM6Pm4v+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54 KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU91PXCJdHIyzc 4oPD/IAPelGqYn9u0AOpga6CQW1Ge/j1iNEinrw0KYn0eouDBvG0RQvENIAsnvarNv7OqQPX +6r0qTH0S7OYOlK1Trn8oXEbgwtrPOKULltccTR004vFwbdg1iMsoPlPzKV1v8Ns2eF7OprS P6ii2g9pAF3vzek28AhhZPSiYIVy1DE7iV5z5g2JdGiUkF7Z8SrEJ1NuC2ANot2Q98iQ25zt SY1z70Jo5+7fCwQxJs7wB7fbuWKfo6V6R3sSOifOy13hG55eL2hnRay91CtxvDhW8S00FhHr ipInsXQun0Q1RHd6siKR/h580ql2DuC2A7d5+JZLE02m6TWKYItz7o0m5cXsEnOADL7lUr0g aKQa04q9O+o6+H9bbXnoJ+RL5N7igbkMqQohMO/BeA4PhIQUGeG5OSx0qDo807hQLhSkPE6j q3UvIrZKMkbvKK1HRFZ3ps55xu/ADqr1skTk2MdI1JfYh2HipDkO1HQL/D8Cveym1Gsny1qx /DCJ7HgDI/NImXanLfvfbtw5FRQyAU0zdBY6JJUDq8OLOjvVU/2sdzUFh45MwqqzOb7ENhxy J8SVGaVDqKaMK7eq0GE6vwyL+WWZIIYty7xK/0/6P7viX85l0Udfa6s3ZYPcn+3BfRmI0SCY XrsnNgBEn0GsRA4TOPwjl2NTCRfZ3ezX6Ig6TE2E42mDYLZSYCshLyNxju0HppTZmxeDFCDC m/nd5+YVPcUdCKSPshhnyQZWbS5UY8uyQmutBPmy7pgNufb5ioYtYv62Ndp4+3TiAo9+CdvD 8Wd1mGNV3t7knkJRz8wxqB/oFZyxk2N0ahi0LRkEolo+/5HWwFyEJnaye13EZimXwXHeNaEU n6nWNLgHDQ2SM4rztYKJU10TYaMlBfGigOgA74Ol7GITLUy+6TQlyz4LcZ80HbL1+8oiVAgT o1ONHGprqF6/gnXQYXOlhPKxO6Raa0A0XuVpy+4xm2UsRQdCVYoOU2kdXUWZ0+M6M/8+luHV bilT7IuLgpGz8eGbKpMcNzgy1tcF7/4INqLRWW3li+rAAqQgKuWZd/jcWUcxyXQCw4NlQkV8 TCHNBQxLiikqmPaSjdpEAGneFvipNF3s2jzVUoo10ePZkxl2aCy/0scj/ydUPMe3fQNvi4np 3N1HUqy993TAtuE4QFmefYUessztXFA02+RrAlhJtqgIqRl00YZaBhytljy2g9fD4xBlY01t ipvwlcub62f11xFenWT2pWY1qT/DG708VjvbqfX3guby9OK4uIV7/9+rVz/vQavH05k8nN90 tAT3WHOrpPNRBEfV578SCNVv1Bzuq3aby8h5ojVyWwkMK+6tSXH0s4oA+1twwipftNWOqeJX AHoFMhSC8+rIe0s01+nC3BMdOlY9K8vP86lMfKA0aineudhgD2OgmFO4YQ72UWJtmJ9RuPOw 5cZ0qSAxALUMlW0xFyls83xhcVFfWRIRjv5mXWiXtQIIPAuLuNpQS+0Lsa6x8tzncvoUn9cr hu4Ak8endWuclyUZkD82gtZ0QIWp2amkG221W8R8Xlho6yB0SjJ2+mnegAAPzsBTWNijEzsL IvyhtYTWkTubgk1mzOq4E/7w+5Qo6E1fAyxCQ9YOjP7KW1vSP76v7CCYtVP5ZBuuCNeVuj6Y FGGRZbyphIb12XoGG4Ul1VZP3m6/57+mRJ9kmeUKn1++WHYdc9HzhDa/NXARPRV01LqXQFAg CLMThi5Ntitp5CPkovb9/q5XCSnX4FSdi/iycWBsjG67CtkG0/3k/e2k9zhWQ80tE2zn9BgV STTrBv/JIDt3qK2d+NmYkZAC1r16s48EYZ72oc9n5Af33EGi47dpyJW1zeud48BgOSjMDIEX ltpi5bN7RLg2VF/I37B3I//WniHg4Nga9S8fmIKy3c45sFOBr2T6e8Mli90r1yk6APJNKIlz 3FNlL10sidc3r1a3Whlhj+QCb0TA0RCaCnllhDSqsu7sL0SfmGkN765yEt5m9mlSrCEuABVH njjKfJAVWd96NtyNFXU3Tj98IbhLZPZZ9ISrR2ZkFHJieFTJNQwl+YFrSViMGP5+3YizqRo6 H4mlYH/p4WBJ2h3qeiwCB5ZLT34ZIUa/DjrgeBfn9qZ94+qF5RlXD4MWdG7KJDgWCJXvvPhO QGUFTQ6oXrOArvTEziU70J+pm7OGZSmZDmHYWMUxtJ4SFyBNVRS1UoKCS4ikMdzRWXIjITxN V107TcL6hvkpwtQn6h2YgLnXD6XpR/0OGxpDsHOdFwMsl4EvwCPbYSf9r4hQX0epMb66lXTc irDIF0ZaANBEk2cWwK9YP/3vYOGq67AQbDmZ/rWPefQ96oEC6bOlcrpisw8p36NLpndYSMkV qF9gxsZGyg+QpS8+X1HSjRLxX2RKZfB+VHkvHUw95738ey3Clu3tc3WVOQUYZM3vErvyaaba 7zJ230/cGcEkMtKnTiRlt19lBYTk308LWH8V+Rd83eXHOSI3fYIRx8DN3EpbZUOsvJ6h1gXf 5ac04K916Yk3KRsVREfDg2nwZvvPYtTcgTffBvRDUKPftxqPBXtxMf6KeO5QLxU1qBPsgGo/ CycGAnlNyiCkD/gU1auN/tNhWeVJk4Wvob1aRtrBWX5KbCuIhSmLN96iyE3yrwolzvLM2AbK z11b0JKqPWZ8ypZhvx1H2EJ4GBiKKGInCOQ7u+QLZhz07MjGiNvi+dT+2g30ZNQ5SBAAeNvw W7c84IorFahne2CjDFgVVsGqzpGgp6KoVQ3Oajd8colOz6M9xYM4GOMThUS8oE9W5u/5uYKk IGJyf6gTVUKu8jZ9sYdGcXOfceOMX57dAHsBCaRFgwOCziiKWDYgUVZ1vCU7Hyc6JYg+f2O0 NIDTKFWUFstG7YUEENgSZYLKpd2RTMpkviSiscO6Ty/rQXebMpft5HDEPmVBL+8TVTRxakBf BYOzb7ieM4LMZbn3kV5dlRgtIHDGk6VQsoU5yM8Mkk7p0JC9HU4RWo2kRGACEvl8DoYEvi6m QQzgw11bLE29Tvi1FwwI0LDuCo6lERZcTrNjjWYcTq3J6C1D9g+48/cuE04M5e9SAFwP1Xad a1MMT7FQ/dOleIlez03zgDbvpRLFLhXSqgWOHct
  • Ironport-sdr: 649d7056_huVjQodEdaSV2J+06kiR0Mwh2BvGzZkexdpa2NuXN9v+CrL xV73AkCB4H/mU5WVaAOUw6+twQs3ZwJegBC6E9w==

The following worked, thanks:

emacs myfile.v --eval "(proof-process-buffer)"

On Thu, Jun 29, 2023 at 12:59 AM Stefan Monnier <monnier AT iro.umontreal.ca> wrote:
> emacs  --eval "(proof-process-buffer)" myfile.v

Emacs processes its args sequentially, so the `proof-process-buffer`
will be called inside the *scratch* buffer and only after that's done
will `myfile.v` be loaded.

You might want to try

    emacs myfile.v --eval "(proof-process-buffer)"

instead, or

    emacs myfile.v -f proof-process-buffer


-- Stefan




Archive powered by MHonArc 2.6.19+.

Top of Page