coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] emit .vo file during interactive editing
Date: Fri, 2 Apr 2021 20:10:21 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f46.google.com
Ironport-hdrordr: A9a23:7CJXjaj/6yI/F3EiMvRx0AjRpnBQX6d13DAbvn1ZSRFFG/GwvcaogfgdyFvIkz4XQn4tgpStP6OHTHPa+/dOkPEsFJ2lWxTrv3btEZF64eLZskTdMgDd1soY76dvdKBiFMb9ZGIRse/W6BS1euxQpeWv37uvgY7lvhVQZCFsL5pt9gJoTjuce3cGJzVuIbocON6i6tFcpzymEE53Uu2eCmMeV+bO4/3n/aiWBSIuPBIs5AmQgT7A0teTeCSw5RsQXyhCxr0v6wH+8zDR3LmpsP2w13bnpgjuxqlR8eGRrOdrNYijjowwJi/3ggilIL59U6CP1QpYnMifrHgtltfIr1MMHeRWr0nQcGa8vAf312DbvQoG2jvNz1mXhHemm8jlXXYBDdZbj44xSHTkwntlh9133KJV02/xjfRqMS8=
Ironport-phdr: A9a23:YMZelx+NkkcZvP9uWV27ngc9DhMPi/DPJgcQr6AfoPdwSMyLwZ3uMQTl6Ol3ixeRBMOHsqMC0rSI+Pm4BiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagZb5+Ngi6oATQu8UZnIduNqQ8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUTFKDIGhYIsVF+cOMuhYoIv9qVUArhWwGBeiC//gxDJTmn/2xLc33/g9HQ3a3gEtGc8FvnTOrNXyMacfSfq7zKjWwjXZdfNZxyr25ZbPchA8u/GMQbNwftTMyUIyEA7FllSQppL/PzOPyOsBqXSU7+19VeK1l24nqh9+oiW0y8cjj4nGnIMVylTe+Splx4Y1IMS1RUhmatGrDJVerTuVN5dqQsw8WWFovj43x70atZO5fyUHypYqyh/cZvGZfYWF5g7vWeePLDl4gH9oebyyihWy/EWvyuPwSsu53VRKoCZbktfBq3IA2h3T5MWBV/Bz8ECh2TOV2ADS7OFJOVw7la3BK54n3LEwkp4TvV7dESDrhUX7irKdeEY8+uWw9ejrfrHrqoWfOoJ0kA3yL6Ujl82lDek3MwUDWXWQ9/6m273550L5Ra1Hjv0onandt5DXPcEbqbS4Aw9Ry4oj6hG/Ayq/3NQWknQKLUhJeB2Aj4juNFHOJO73Ae2jjFSrlTdn3/HGPrv/DZXRNnXPjqvtcLJn50NfyAc/181T6pNVB70bL//+W1f9tNnCAR84Nwy0zfznCNJ41o4GQWKPA7GWMLnIsVCW/O4gP+6MZJIPuDbhKvgq+ePugGQ2mV8YZ6ap3J8XZGqkEfRhJkWVeWDsjcsZEWcWogo+S/Tnh0GFUT5Kfnq9Q6Y85iwgB4+9FofCRoWtgKSb0yuhH51WYHpGClGWHnvyeYWEQaREVCXHCch42hcASLLpH4QmzFSlsBLw47thNOvdvCMC48HNzt9wstXSmAso+HRfCNmHz2CAUikghmIFXSU7mqt4vFZhy1qe+ad9iv1cU9dU4qUaAU8BKZfAwrkiWJjJUQXbc4LMEQ7+Kv2WRAopR9d0+OcgJkN0GtGslBfGtwKlBrYUk/qAA5lmq8r07z3KP894jk3++uw5lVBOasRKPGyiwKV48lqLb6b51n6BnqPvTpwymS7A8GDr5W+HvUUdUQkpFKuZAzYQYUzZqdm/7UTHHefGNA==

Hi

I think this feature disappeared at some point. But you can reduce
drastically your waiting time by building ".vos" instead of ".vo".
Unsound but extremely fast.

My mojo:
1) add "Proof using ..." annotations everywhere in your sections,
otherwise the compilation time will not decrease. There is a mode in
proofgeneral where these annotations are added automatically when you
pass a Qed.
2) compile .vok from time to time to check proofs.
3) compile .vo file to really check universe constraints once a day
(or week maybe if you don't expect such problems).
Best
Pierre

Le ven. 2 avr. 2021 à 19:27, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> 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.
>
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

[Coq-Club] emit .vo file during interactive editing, Abhishek Anand, 04/02/2021
- Re: [Coq-Club] emit .vo file during interactive editing, Pierre Courtieu, 04/02/2021
  - Re: [Coq-Club] emit .vo file during interactive editing, Tej Chajed, 04/02/2021
    - Re: [Coq-Club] emit .vo file during interactive editing, Jason Gross, 04/02/2021