coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] proof-general/company-coq: always keeping goal window in sync

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] proof-general/company-coq: always keeping goal window in sync
Date: Thu, 22 Aug 2019 12:11:08 -0700
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-io1-f52.google.com
Ironport-phdr: 9a23:ohUasRBQHmUh4L8C21uiUyQJP3N1i/DPJgcQr6AfoPdwSPT7pMbcNUDSrc9gkEXOFd2Cra4d0ayP7/6rCTxIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+roQjet8QajohvJ6UswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9UrxKvqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAooThvFQOrRq+BRKsBOzxyT9Dm2P73asg3OQnDA7NwQstEMgVv3TUrdX1L6cSXv62zKXS1zrDaelZ2THg54TScxAhoO2MXb1rfMrezEkgDQLFjlGKpYP5ODOV0/0Avm6G5ORuUuKvjnQoqwB3ojW32sgsjZPJhoQLxVDA8SV12pg6KsClSEN9fNWqE4NQujmEO4dqRs4uWWJltSYgxrEbuJO2fTIGxZQ5yxPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq9Eiv0Oz8Vs2t3FZLqSpJj8DAtn4N2hDN8MSHRfx9/kCu2TaLyQ/f8P1LIUcxlabDKp4hxKA/loYLvEjdAiP7nF/6gayWe0k+5+Sl6uXqbq/mq5OCL4N0jxvxMqUqmsyxG+Q4NQ0OUnCB9uun1L3j/Fb5QLVUgf01iKXWqpbaKt4dpqGkGQNV04cj6wqwDzq939QYmGMILFNBeB6dk4fpPFTOLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g4gZQCeEBrKTePfZtkbN7eYyKcGNYpUUsXDzMa52yeTpiCoQk18cZqmk3tM+bnm+ErwyKk+ZYGHsj9RHGGEDuAZ4Te32h3WNVDdSYzC5WKdqtWJzM56vEYqWHtPlu7eGxiruRsQKNFADMUiFFDLTT6vBQ+0FMXvALcpokzhCXr+kGdd4hEOe8TTiwr8iFdL6vygRtJbtzt9wvrSBmhQ79DgyBMOYgTjUEjNE21gQTjpz55hR5ExwzlDZjPp9iv1cUN1UvrZHD118OpnbwOh3Tdv1X1CZcw==

While using proof-general with company-coq, I often get confused because the goal window is showing a stale proof state, even several minutes after the processing has finished. I think there are instances in the proof-general/company-coq code where the proof goal would not be updated ever.

Is there a way to configure the editor system so that the proof goal window is always kept in sync, except of course when Coq is processing the commands, and except a few seconds after the processing is finished.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] proof-general/company-coq: always keeping goal window in sync, Abhishek Anand, 08/22/2019
- Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync, Yannick Zakowski, 08/22/2019
  - Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync, Christian Doczkal, 08/23/2019
    - Re: [Coq-Club] proof-general/company-coq: always keeping goal window in sync, Pierre Courtieu, 08/23/2019