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: Stefan Monnier <monnier AT iro.umontreal.ca>
  • To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • 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 00:59:18 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
  • Ironport-data: A9a23:KivgnaN5kcmIYdDvrR0Ck8FynXyQoLVcMsEvi/4bfWQNrUojgjMCy GBLWjiPPqvbNDb8f4t1PNy0oUoOusDSzYMyQXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYAbNNwJcaDpOsPrd8kI35ZwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXEMF/S6NpWCHppHopF1v1LA1ERy fgXfWVlghCr34pawZq+Q+honc8qKs/mJsUeoHYm0DTeC+o8TJnHBa7DjTNa9G5r3IYURaqYP ZdfNGIHgBfoO3WjPn8SD5Q4neqyrnjldHtFrVWTubA66myVxwUZPL3FaYOII4PbGpQF9qqej mXd2l+kAhYnDd2kySKC+VSe3+TwzQquDer+E5Xir6Q73wHProAJMzUdUkL+qv2kgGalStdHI goV/DAvpO487iSWosLVWhS5pGWPtxgaVsAWEvc9rhyIzazI+QuQAi4PR1atdeDKquc0BhgU/ XCxm+i2JjsynKapS0LCyrOb+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOPXp5jESMWqrq w1mvBTSlJ1P0JNRjfnTEUTvxm33+MOWF2bZ8y2KNl9J+D+Vc6aOTuREA3D+6utGMM6jSUiIu BDocOC+t9hm4X1gWEWwrAglGbio4+2OOTvajEQpHoMmsSmo/Hi/Z41Z5Hd1LS+F0/romxe3P Cc/WisIufe/2UdGi4csOepd7OxwksDd+SzNDKy8Uza3SsEZmPW71C9vf1WM+GvmjVIhl6oyU b/CL5bzXClFUf42kGbrLwv47VPN7nxvrY80bc2jpylLLZLFOhZ5tJ9caQvQPrlnhE96iFyOq o832zS2J+V3CrSkM3aLreb/3HgQIGM2DI2+p4NWcOCEOA9vBGAmDeSZ2rggdop5nqpUj/rF5 TmxRwdB1Vf1iHaPaR+LcRhehEDHAP5CQYYAFXV0Zz6AgiF7Ca72tfd3SnfCVeR+nACV5aUvF KdtlgTpKqkndwkrDBxEPMSt9NU6KEjw7e9MVgL8CAUCk1dbb1Sh0rfZksHHrUHi1wLm7Jtsk K7qzQ7BX5sISiJrCcucOrrlzEq8sTJZ0Kh+VlfBaIsbMkj90plYGwqohN8OIuYINUriwBme3 F2oGhs2n7TGjLI019jrvpq6ibmVPdFwJWdgJFmD342KbXHb2kGB3b5/VP25eGGBdWHsp4SnS +Zn79D9F/wlhF1P45dwLO91x6QE9unQiaR+yyJkPXTUbmaEDqFrDWmG0PJu6IxM5O59kimnV n2f/uJ1Pe2yB/rkN1oKNi8JU/+m18xIqgLN7P8wHlr21BV38JWDT09WGRuG0w5ZE5dYL6Inx r0HlPMNygnilCcvDMmKvhpU+0uIMHYEdact7bMeIY3zjzsU2kNwWoPdBgD28aOwRY11aGdyG QCthY3Gm7h47WjBeSBqFXHygMxsta5XsxVOlFI/N1CFn+TevcAO3TpTz2UTbh9UxRB5we5MK jBVF0lqF56voRZspuZ+Bl6JJS8QKiGdyELLz3kxqFb4VGitD2zEE308M72C/Wcf6GNtQQJY9 7C5lkfgVSfgbZyo1BRjREJFifjScsNsx1fvmeSMPceML78laxXL346sYmsprUP8IMUT3Ufom 8hjzNxSW4baaxEChrIdMJaL84gQRDSvBn1wcds48IwnRWjjKSyPgx6QIEWPS+ZxDv3t837gL fdxJ8hKBi+M5AzXoh81XaczcqJJxtg3798/e5TuF24Mk52bihFL6Jvw1CzPtFUHcuVUs/QWC 93uLmqZM2mqm3FrtXfHr5BENkqGcNA0XlDA897vwtoZNaAokb9KQRkp36qWrkelFlJt3yips TPpY47UyO1fyrpQobb8L5UbByuIBIPycM+q7DGMt89/aIKTEMXW6CIQhFrVHyVXGrozR+VIk a+G6vj31kaYuL03DnjSnsmcG5YQ+8+0ZvtlDezsCHx8nQqDR87ezB8R8E+oKZFysY185+v2Y yCaecePZdoudNMF/0Jsag9aCAQ4J5XsS7XJ/AeRjq2rJEAG8ArlKNiHyyfYXVtDfHVVB6ykW x7Ghfm+w/t58qJOPUYgLNN7CcZaJFTDZ/MXR+fpv2PFMljy00KwgZq8px8O8jqRN2KlFvz96 pf7RhTTUhS+laXL7dNBubxJoRwlIydhsNY0Y34i1YZ6uxKiAE4CCNYtA5EMJ5VXsy71jZ/GP WCHKCNoDCjmRj1LfCnt+NmpDE/VGuUKPcy/PTAzuV+dbyCtHo6bHb997WFa7mxrfif4hvSSQ T3EFqYc4jDqqn2oeQoS2hB/qeJux/fBzXsO/03n1c3oBFADBLIMyGZsFQ4LXiWv/wQhUqnUD TBdeIyGaBjTpY3N/QJIemRSXgwcuzXz1TghaWGEyb4zfq2FmfZYxqSX1/7bi9U+gQdjGFLKb XLtQC2Q5meQxmYesK9vsNtBbWqYzx6UNpDSEZIPjjH+U019BqrL8i/CcecyoBkexTNi
  • Ironport-hdrordr: A9a23:9YmB9Ktkdm8QhkvwySXfhKPe7skDUtV00zEX/kB9WHVpmwKj9v xG/c5rrCMc7Qx9ZJhOo6HlBEDtexzhHNtOkOos1NSZLW/bUQmTXeNfBOLZqlWKcUHDH6xmpM JdmsNFaOEYY2IVsS+32njeL/8QhOO/2ITtpcDw6R5WPHlXQpAl1T5QLkK/PnJbYWB9dOEEKK Y=
  • Ironport-phdr: A9a23:jqR39BfoX6Y6YFtbnUxRCoRQlGM+ftTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWXG92AoKIUw6qO6ua8AzFGuc7A+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAI cJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+N hq7oRvQu8UMnYdvJKk9xxjKr3BVf+ha2X5kKUickhri5sq85oJv/zhVt/k868NOTKL2crg3Q rBfEDkoKX0+6tfxtRnEQwuP538cXXsTnxFVHQXL7wz0U4novCfiueVzxCeVPcvtTbApQjui9 LtkSAXpiCgcKTE09nzch9Fqg6JapBKhoAF/w5LRbYqIOvdyYr/RcNUHTmdHQ81fVTFOApmkY oUPEeQMI/tWoIv+qVsAoxWxCwajC//0xz9UmnP7x7E23/g7HA3a2gErAtIAsG7TrNXwLKocT Py1w7fGzTrZafNdxDDz6I/OchAnoPGDQ6hwetfWxEkqEAPFiFOQqY37MDOPzekNsnKb7+16W eKyjm4nrAdxoiS1xsgykIbJgpgZxUze+ihgxos+ONK3RlJhb9G+DJtQqz+VN5FwQs46XW1lv Do3xLMatZO/fCUEx5YqyhreZvGbbYWF4RDuWeaPLDl2hX9rd7KxihS9/0WjzuDxUte43UhJo ydKjtTCuXYA3AHQ5MifUvZx40ms1SiV2wzN9u1JLlo4mbTbJpI7wrM8ioIfvEXHEyPshUn7j a+bel859uWo6+nreKjqq56CO4JylwrwKL4hmtalDuQ9KgUOX3aU+eC71LD7+E32WrRKjvktk qbFqp/aI8IbqbCjAwNP04Yj8RG/Ay270NQdmnkHKk5FeAiZgIfzP1HCOuz3Au2nj1Stljdk2 ezGM6X8DpjDMHTPiqntcapy5kJG1gY+zcpT6pJIBr0ZJfL8QE7xtNjWDh8jNAy0xv7qCNB61 oMYX2KPA7GWMLnJvF+J/OIvJPOAZJIQuDb6Lfgl++TugmEjll8ZZ6WmwYEYZGi+Hvt9O0qZe 2bjgs8dEWcWuQozVPHmhEWYUTFPf3ayQ7485jYjBY26CofDX5mhj6CF3CemBZJbfXtGC1CJE XfwbYqIQfYMaCSIIs9giDMIT7ahS5VynS2p4Sbwy7t8LufXsgQevJTvnIx87e3SjhE/9np9C c2b3yeMTn17tmwNTj4ymqt4pBou5E2E1P1Dn/FWHNobwvRPVAY3L9aIyut8DdH/QCrAZNDPV VOhRMm8DDg1CNk4lYxdK31hEsmv20iQlxGhBKUYwuTj7P0c96vd2yK0PMNh0zPc06JniVA6Q 8xJPGngh6hl9gGVCZSa216BmfOMcqIRlDXI6H/F1XCH6URfVghxXL/tXGoYIFbTqtLl/E7LS /mlAOdvKRNPnPaLMbACcdj1lRNDTfbnNs7ZZje0nGG2BBuS7rKWa8z3fmIbwD/QAUxCmAlAt W2eO10YASGs63nbECQoFV/rZBb09vJirXqgUkIu5wSDbkl63LOz/BMPw/2GTLUO27UCpD0so jEyF1/VM8v+Ld2GqkIheaxdZYl4+1JbzSfDsAc7OJW8Lqdkj1pYcgJtvkqo2Q8lQoNH2dMnq n8n1m8QYeqRzU9BejWE3JvxJqyfK2/8+wqqYrLX3VeW2cif+6MG4vA141v5uwThGk0n+nRhm 95bthnUrpDNCgwTXIjZU1wwsQV/oLfGeCQ048Xf3DwkMKW5tCPDx8N8HPEsmXPCN59UNKKJE hO3EtVPXpP0brZyxx7zM1RZZLM3luZ8Jc6tevqY1bT+Oe9hmGjjlmFb+MVn1UnK8SNgS+nO1 pJDwveC3wLBWS2v6TXp+s3xh41AYikfW2Slzi2xTotWYKtzcJwjCH2pZdCywdNinZPkXzhT/ RTwYjFOkN/sYheUY1HniEdV0kIRoHG9sSqiyHppljYvsrCS1SiIyO2oJ39lciZbAWJli1nrO 429idsXCVOpYwYenxyg/U/mxqJfqcyTNkHrSFxTN2jzJmBmCO6rs6aaJtRI49UuuDlWV+K1Z RabTKT8ql0UyXGrE2xbzTE9Pzak3/ex1xl9jmScIWxbrWDeP9x1whHD/tHVQbha13IKSTJ5h j/eGlWnd4Dyp5POz8uF6L34CjrpX4Y2E2Gj1Y6asSqn+WBmSQaymfy+gJyvEAQ31zP6y8g/U CzJqBjmZYy4n6++MO9hYgxpHAqlsJA8QNki1NFtwsxIih14zt2P8HEKkHn+K4Be0KP6Nj8WQ CIThsTS607j0VFiKXSAw8T4UG+cy41vfYrfACte1yQj4sRNEKrR4qZDmH4/p12+qwPce9B8h DBb1P4p7mIAjugN/gEkhHb4YPhaDQxDMCrgmg7dpdW5qqNWaXyHcKK3kld7mta9FryLpkdXU TyqH/VqVT815cJ5PlXW1XT14YyxY9jcY+UYsRiMmgvBhexYe9oh0+AHji19NSfhrGUonqQl2 Ad208jw7+3lYy19ubi0CRlCOnjpatMPr3vz2L1GkJ/e1tKqE49qBy8GGprySrS1FTUUqe7qP gLIGzRZyD/TEOjaFA6bsB4grmjIVY2uMHeLPnQQyZNpTVGUdklWgQRSXS892IM8EQa23sHod AFy71Vzrhbx+B5Fy+ZzPBD5VGrF4gaybXEpTZ+ZMABb5wUE7E6dMMqV6v9/EnNF+5qnsBaAI 2jdbA0AG2gNXgbs60nLGL6o6JGA9uGZArD7NP7SefCUrucYUf6UxJWp248g/jCWN8zJMGMwR /s8klFOW3x0AaG7030GVjAXmiTRbsWauAb0+yt5qdq6+ejqXwSn7JWGCr9bO9Fisx6shqLLO +mVjSd/YTFWs/FEjWfP06Qa1UUOhjtGcjCsFa8LvCjLQbiWm7VQSQMebCVvLsZB6+Q310gFO MLWjM/0yq8tjvMxDAQgNxSpkcWoaMoWZmClYQqcXgDRbOjAf2CNnpmkBMH0Aaddh+hVqRCq7 DOSEku5ey+GiyGsTRekd+dFkCCcOhVa/oC7aBdkT2b5H7eEIlW2NsF6iTouzPg6nHTPYCQZN j56ck5XhryK6mVFh/J5B3ZM534jJuDOyEP7p6HIb40bt/dmGHE+j+VB/HEz0KdY9glBTf1xg yDbqNhjuReniO7J1z9gVgZUpz9PwomC9xYHW+2R5txLXnDK+wgI5GObBkERptdrPdbovrhZ1 tnFkK+bwNhq8sjTu9YZAM7IMs+ONDwqOEiwcNYxJAofSni2MGbZm1ZQmfXU/XTH9vDSS7Dpk ZsKUbRSUlo4DLUbEEMjAdkFJottUzog17WS3pZg2A==
  • Ironport-sdr: 649d0faa_aYIDLUn/lVn4QlTGpuUIPhiiUkv0mlDGZqLZzCB3mZlcSLe uyQPxmw6UtDAIbH1ZgD3F/A6uyzAHtJzZJ1RQfA==

> 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