ProofGeneral
Fail output not shown when running completely silent
Fail Check 0 : 0.
should say "The command has indeed failed with message: ..." in *response*
but says nothing (the message is still visible in *coqù* though)
IMO this is a duplicate of #842, which will be fixed when rocq-prover/rocq#21038 is released. In the meantime please disable coq-run-completely-silent and restart PG.
Also does that mean it's intended to stay broken on previous rocq versions?
I think the situation is the following (@hendriktews correct me if necessary):
- For now and for coq <9.2 there are no perfect solution
- with
(setq coq-run-completely-silent nil)you will experience goals that are not updated correctly (go back an forth or using C-c C-a C-s 1 to see the goal). - with
(setq coq-run-completely-silent t)you lose some commands output.
- For 9.2 everything should be fine with
(setq coq-run-completely-silent nil)which will be the default.
@hendriktews what do we need to do for 2. to be already working when coq 9.2 gets out, and maybe even now for pepole currently using the rocq master branch?
That doesn't make sense, I'm running rocq master. Please reopen.
It is a duplicate and I am not going to further work on it before the necessary support in Rocq is released. Coq/Rocq master is not officially supported by PG and unfortunately I don't see capacity to change this. Not sure what does not make sense here. I don't care to have duplicates open here, so if you want to have several issues open on the same problem, here you go...
Also does that mean it's intended to stay broken on previous rocq versions?
Yes, I don't see any other choice we have as long as the Rocq team does not backport the necessary fixes to previous versions. I still believe that what you call broken is a big improvement over the situation before #762 was merged.
IMO "For 9.2 everything should be fine" doesn't make sense with master (= 9.2+alpha) not working. I didn't look at the duplicate because I trusted you when you said https://github.com/rocq-prover/rocq/pull/21038 fixes it, and I know this issue isn't fixed so I thought it couldn't be a duplicate.
2. For 9.2 everything should be fine with `(setq coq-run-completely-silent nil)` which will be the default.
No. IMO for 9.2 we need to make Set Silent in coq-shell-init-cmd version dependent and disable it for Rocq >= 9.2. As an alternative to changing coq-run-completely-silent people can also delete the Set Silent there.
@hendriktews what do we need to do for 2. to be already working when coq 9.2 gets out, and maybe even now for pepole currently using the rocq master branch?
More capacity to also support Rocq master. Frankly speeking, it was the Coq team who introduced the changes (in Coq of course) that caused #568 and then PG volunteers had to spend a huge amount of time to remedy the situation.
IMO "For 9.2 everything should be fine" doesn't make sense with master (= 9.2+alpha) not working. I didn't look at the duplicate because I trusted you when you said rocq-prover/rocq#21038 fixes it, and I know this issue isn't fixed so I thought it couldn't be a duplicate.
I never said that 21038 fixes the problem, I rather said "#842 [and all its duplicates] will be fixed when 21038 is released."
No. IMO for 9.2 we need to make
Set Silentincoq-shell-init-cmdversion dependent and disable it for Rocq >= 9.2.
That is what I call "what we have to do". I can handle this part.
@hendriktews what do we need to do for 2. to be already working when coq 9.2 gets out, and maybe even now for pepole currently using the rocq master branch?
More capacity to also support Rocq master.
I work every day with 9.1 with no real problem except #841 . Is there something in particular that will not work on master?
Frankly speeking, it was the Coq team who introduced the changes (in Coq of course) that caused #568 and then PG volunteers had to spend a huge amount of time to remedy the situation.
That is the curse with PG and, frankly, we were lucky this happened so rarely (the late pcoq and ctcoq teams would agree I guess). Such problems have been very rare in the last 25 years. Even coqide itself was harder to maintain than PG.
But indeed recently with the new coq interaction protocols,I think less care has been taken concerning the continuity of behavior of coqtop specifically. But honestly I could have suggest this new option for goal printing much sooner if I had more time thinking about it. A waste of time indeed.
Nice proposal, I would certainly support this. To give you an idea, PG currently supports 11 Coq/Rocq versions and 10 Emacs versions. Instead of the full matrix of 110 combinations we currently test 37 combinations, see https://github.com/ProofGeneral/PG/blob/master/ci/doc/README.md . It probably does not make sense to run PG tests to this extend in Rocq's CI. If there is interest on the Rocq side to pursue your suggestion further, I would be interested to further discuss this in a telco.
I am on the Rocq side ;) I guess we would only test 1 combination (current rocq * whatever emacs ubuntu gives us).
I think to make it happen we just need
- some command or make target to run tests so we can essentially
git clone $pg_url && cd PG && make test-target(can be more than 1 command or target if needed) - for PG to be ready to run tests on Rocq dev in PG's CI, so that PG changes don't break Rocq CI
I read "current rocq" as the HEAD of your master branch - can you confirm this? Otherwise, please give me some time before I answer in detail.