ceps
ceps copied to clipboard
coq
Requirements for supporting Ltac2 debugging with a high-level outline of changes
Note that the CoqIDE on master is broken due to your change in #15772. You didn't like the fix I proposed, which at least worked.
You've known about the interaction model for almost a year now but are only objecting now. We should first consider a proper fix for possible inclusion in an 8.15.2 rather than a sweeping change. Unless you plan to revise the interaction model yourself, you'll need to state clearly what the problems are and what you would do about them. I think that would be mostly orthogonal to this CEP. Certainly we can discuss your concerns some Wednesday, but let's not hijack the discussion of this CEP.
I believe I raised the same concern in the ohr CEP about the debugger: ceps should be about the details, not about a high level view. In particular if a thing is useful, or not and if we should invest time in it does not belong here, IMO. Here is a place to discuss the details, how the feature interacts with others and why a specific design has to be preferred to others.
This text supports the importance of the feature, not really how it is done.
In particular if a thing is useful, or not and if we should invest time in it does not belong here, IMO.
Where does that discussion take place then? It's very hard to do a design without substantial agreement on the requirements. From comments made elsewhere some time ago, it was apparent to me that we weren't agreed on the requirements.
Here is a place to discuss the details, how the feature interacts with others and why a specific design has to be preferred to others.
Most frequently, the aim of the design process is to find a reasonable solution rather the "best" solution. If a clearly better idea emerges, then you iterate on the design. The idea of a waterfall model in which all design is completed before coding begins is archaic--30 to 40 years out of date. More modern approaches break the work down into numerous small steps: take a small but useful piece of the requirements, investigate/implement it, test it. The slow pace of reviews argues for bunching many small steps into a single PR. Note that working on Coq requires quite a lot of investigation/reverse engineering. Timely answers to technical questions are frequently not available; after a while one don't bother most of the time.
Of course there is some planning, but the plan may be revised after each small step based on what's learned along the way. This has happened frequently working with the Coq code--I discover something totally unexpected.
If the review process for a subsequent PR identifies significant bona fide design issues I'll make changes.
This would a good topic to discuss at greater length at another time or at least in another thread.
Here an example: the fact that debugger had to point back to the source code was foreseeable. How to do that would have been a topic for the CEP. IMO we did not even try.
Of course the design can change. Starting with no design is not a development model. Designing without requirements is slso impossible, I agree with you.
Well, I would not have known the information needed to intelligently discuss how the debugger points back to the source code without investigating (reverse engineering) and getting it to work to a significant degree. And indeed we only got consensus by building test cases and counterexamples. There is no detailed design at the outset; it's created incrementally as the project proceeds. IMHO. The process varies; we each have our preferred ways of working.
First question IMO to ask here is why DAP doesn't work for Coq, and how we need to differ from it.
We chose a strategy some time ago to support both the current XML protocol and eventually DAP. Anyone who wishes to can implement DAP support. However, DAP is not relevant to a discussion of Ltac2 support requirements. It would be inappropriate to try to hijack the discussion.
@jfehrle maybe you chose that strategy, but certainly me and other devs don't agree with it, if I understand correctly.
You can think DAP is not relevant to the current discussion, but for me, and in particular when discussing about what the interface between breakpoints and source code is (discussed just a few comments back) , it is clearly on topic. My position still stands regarding our debugging protocol: Coq should try to follow as closely as possible DAP (which is an industry standard), and if we need to deviate / extended, it should be properly justified.