Skip to Content.
Sympa Menu

coq-club - [Coq-Club] emit .vo file during interactive editing

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] emit .vo file during interactive editing


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] emit .vo file during interactive editing
  • Date: Fri, 2 Apr 2021 10:28:05 -0700
  • Authentication-results: mail3-smtp-sop.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-ed1-f53.google.com
  • Ironport-hdrordr: A9a23:TIV/6KilVMb/HquZFL2aAYSUQHBQXmcji2hD6mlwRA09T+WzkceykPMHkSLlkTp5YgBGpfmsGomlBUnd+5l8/JULMd6ZNjXOlWO0IOhZnOjf6hL6HSmWzI5g/INBV4Q7N9HqF1h9iq/BgTWQN9o72tGI/OSJqI7lvhVQZDpnYa1h8At1YzzzeiZLbTNbDpk0Hof03LsjmxOcfx0sH6CGL0hAceyGg9HQjprpbVo9GhY75GC14Q+A2frVFR6X2xtbfhFu5fMZ8WbDmxHk/anLiZyG4y6Z+WnU4ZFb3OHk18IGPsqRkcIYQw+Cti+YIL9sUbGDozw5ydvA1GoX
  • Ironport-phdr: A9a23:qN5jthz5SdoH8hnXCzK/zVBlVkAck4WxBRYc798ds5kLTJ7L16rrMEGX3/hxlliBBdydt6sVzbOI7eu5ATNIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLd/IA+roQjQt8QajpZuJrozxxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuB2uqRxxzYDXfY+bKuZxc7jHct8GX2dMRNpdWzBDD466coABD/ABPeFdr4Tlu1YBthu+BQi3BOPv1DBIhWL90LE80+s7FwHJwRErEtUUv3vPrNX1NbwSUeCrw6nL1znMdfVW1i376IfVaBwhoPCMXa5/ccfKxkkvEhnKjlSUqYD/IzyV0eENvnGd4uF9Wu2hl3QppBttojiz2MgskI/Ji5oLx17E6yh03Yk4K9KlRUJlb9OoDphduj2UOoV2XM8vTGVltSQnxrAEpJO2fCgExZYkyhPdd/CLbZaE7xHgWeufJzpzmXxreLW6hxmo8EigzPXxWdWz0FZQqCpKjN3MtnQX2xPN98eHV/1w9Vqi1zaXzw3f9P1ILEQumafYK5Mt2KA8moYQvEjZHiL7lkP7h7KMeEo+4Oin8eHnb63mppCCM490jRnzMqE0lcy+BeQ0KxYBUHWG9eil2r3u/UP0TK9Fjv0xlanZv5TaKtoBqqGlBA9V154v6xe5Dzi4zNQVhWcLIE5BdR6djIXkO0vCLO7kAfq8mVihkDlmy+jDPrL7A5XNKnbDkK3mfbZ480NT0hE8zdBe55JPCrEOPvHzVlXru9zeFBA5NRG7z/zmCNV8yoMeVnmCAqCcMKzIsF+I4vgjLPWLZI8QoDr9MeQq5+byjX8lnl8QZbWm3ZwOaHyhAvtmJ1iZbmH3j9caEWYKuxI+Q/bwhF2DVz5TfXeyULgm6jE1EoL1RbvEE4uqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2ktX7igUI8s1lmHsgb8x/IzJ+DU+zYYuJGl3d584eGVlBAu+hR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6Ut25RwJZlo//pMFzwCG9vZxu1+Bcr1X2rpcdKASVLgSdKjU2hZZuJ0+McHZgNGI/vnlgrKtwKlBrYUk/qAA5lmqsr07z3KP894jk3++uwhgl0hKuNKPGyiw6Nzrk3dWtWPnEKemKKnM68b2XyVnFo=

Very often, I have a file X.v which I know has errors. 
So to fix them, I can only edit it interactively, e.g. in emacs/company-coq
When the fixing is done and the whole buffer has been processed by coq, can I ask the editor/coqtop to dump a .vo file for the current .v file?
Otherwise, I have to reprocess the whole file by coqc outside the editor which can take many minutes.





Archive powered by MHonArc 2.6.19+.

Top of Page