search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

coq: run silently and explicitly Show when necessary #742

Closed hendriktews closed 7 months ago

hendriktews commented 8 months ago

This is a step towards fixing #568. It fixes the cases after Proof, comments and auto, leaving now 3 instead of 6 failing tests in ci/simple-tests/test-goals-present.el.

The first commit here breaks prooftree. More work is needed.

hendriktews commented 7 months ago

Hi @erikmd , @Matafou , @cpitclaudel , AFAICT, the difficult cases of PG not showing or showing incorrect goals are solved now. IIRC, the conclusion in #467 was that PG should run Coq completely in silent mode. This PR precisely does this. If you have an opinion on whether we should prefer the approach of this PR over the alternatives in #467 or #429, please tell! If you have some time to try this out, it would be nice to hear if this PR breaks other stuff. What still needs to be done is clearing the goals after Qed and Admitted, I believe this is simple. What is harder is to get proof-tree to work again.

hendriktews commented 7 months ago

The approach used in this PR does not work for Search and Check commands. I'll start from scratch in a new PR.

cpitclaudel commented 7 months ago

Thanks a lot for working on this @hendriktews ; I don't have anything smart to say on the implementation at this stage but I'm very glad that you're on it :)