poor PG man's workaround for coq/coq#11479 #750
Conversation
hendriktews
force-pushed
the
proof-stat
branch
2 times, most recently
from
ad39c0c
to
69d65e2
Compare
|
This is only an intermediate state, it needs some cleanup. I intent to add a batch mode feature, where the result are written into a file, maybe in the test anything protocol (TAP). And I also want to do tests and documentation. |
|
I think it would the right place (if if the code is sufficiently prover-independent of course). |
hendriktews
force-pushed
the
proof-stat
branch
6 times, most recently
from
2b68486
to
3c99467
Compare
|
Thanks a lot Hendrik! I did not have the time this week, but I plan to test it on next Tuesday! Cheers |
hendriktews
force-pushed
the
proof-stat
branch
2 times, most recently
from
ca9fb11
to
232f13b
Compare
|
The last force-push switched to TAP version 13 (instead of 14). I was told 14 has issues and therefore not as wide tool support. |
There was a problem hiding this comment.
Dear @hendriktews, sorry for replying late! I've just tested the feature.
It is very nice and useful, thanks! in particular as a regular user of PG's omit-proofs feature :)
I wrote some feedback in the review comments below.
Cheers
| command generates a list of all opaque proofs in the current | ||
| buffer together with the information whether the proof script is | ||
| currently valid or invalid. The command can also be run in batch | ||
| mode, for instance in a continuous integration environment. |
There was a problem hiding this comment.
CI is a good use case as well indeed. Did you already tried this? I mean, not from an internal PG elisp test, but from an example GHA script stored in this repo or another one, that would call emacs like this?
emacs --batch --load "init.el" --eval "(proof-check-proofs \"...\")"
And maybe I'm mistaken, but to facilitate this, maybe the function proof-check-proofs should query from some way the filename of the file to test? (which could be the current buffer in interactive mode, for example)
There was a problem hiding this comment.
No GHA and no other repo but I manually tested it a lot from the shell. Please see the PG manual for the command line. Adding a test invoking proof-check-proofs from a makefile is probably a good idea.
There was a problem hiding this comment.
Apparently we get this error in GHA:
emacs -batch -l ../../generic/proof-site.el proof_stat.v \
--eval '(proof-check-proofs nil "proof_stat.gen-out")'
Coq project file not detected.
Coq project file not detected.
Coq project file not detected.
Starting: coqtop -topfile /github/workspace/ci/simple-tests/proof_stat.v -emacs
Hit M-x proof-layout-windows to reset layout
Window #<window 6 on *goals*> too small for splitting
Adding a test invoking
proof-check-proofsfrom a makefile is probably a good idea.
Yes!—and maybe calling this Makefile test from a specific GHA job would make it more visible in the GHA page?
There was a problem hiding this comment.
I investigated the error yesterday: 3-pane mode (on by default) is broken if the frame height is too small and certain Emacses set the frame height to 9 inside a docker container.
In the commit I added yesterday, the test you asked for runs as part of the simple tests. Do you have the opinion that this is not enough?
There was a problem hiding this comment.
certain Emacses set the frame height to 9 inside a docker container.
OK!
In the commit I added yesterday, the test you asked for runs as part of the simple tests. Do you have the opinion that this is not enough?
No worries! it is enough as is.
Thanks a lot @hendriktews !
| (setq src-file (buffer-name))) | ||
|
|
||
| ;; generate header | ||
| (with-current-buffer (get-buffer-create proof-check-report-buffer) |
There was a problem hiding this comment.
Some feedback:
- (important) I believe the
*proof-check-report*buffer should be read-only, adding(read-only-mode)somewhere here. - (minor, maybe to do later, not in this PR!) It could be nice to just type
RETon one of the lemma name, to directly switch to it (handy if the .v file is very large), you know, a bit like the*ert*buffer ofM-x ert.
There was a problem hiding this comment.
- read-only: good point
- key binding: good idea, but I am not motivated to do this now. Instead I envision an extension of
proof-check-proofsthat annotates failing theorems in the Coq sources with(* FAIL *). For my repos I then want to set up a CI action that only checks the consistency of theseFAILcomments usingproof-check-proofs. This way, fixed proofs and new failing ones pop up prominently during review and one can search form them. Moreover,M-.(xref-find-definitions) works in the report buffer.
There was a problem hiding this comment.
annotates failing theorems in the Coq sources with
(* FAIL *)
OK, looks like a nice idea!
M-.works in the report buffer.
Great!
OK looks good, but I'm not TAP-savvy, so I can't comment more on this one. |
Neither me, but our local QA expert is. |
|
Rebasing this PR on #761 to fix the errors in the previous test run. |
hendriktews
force-pushed
the
proof-stat
branch
3 times, most recently
from
2a7c6c1
to
7876226
Compare
The first phase only classifies proofs to be omitted and stuff not to be omitted. The second phase does the actual replacement and adjusts the overlays/spans. Feature wise this commit does not change anything but it enables reusing the first phase for new features. Additionally, slightly extend the omit proofs test.
M-x proof-check-proofs checks all proofs in one buffer and displays a list with which tests currently pass or fail. This is a Proof General implementation of coq/coq#1147. It enables a PVS-like workflow where files are processed with -vos and proof-omit-proofs-option enabled such that one can focus on the most interesting/difficult proof instead of the first failing one.
- read-only and no undo in report buffer - add a batch mode test for proof-check-proofs; require seq library to make this work in Emacs 26
Work towards a feature that permits to extract lists of failing proofs from PG. Similar to what coq/coq#11479 would provide.