Jim Fehrle (May 14 2023 at 15:59): Jim Fehrle (May 14 2023 at 15:59):Does tag in ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr give enough information to allow printing its value as a Pp.t or string? And if so, what call do I need for that? I think debugger users will want to see (at least) the value of items tagged with "constr".
Rodolphe Lepigre (May 14 2023 at 16:28):You can compare tags (and learn that their types are equal) by matching on the result of Tac2dyn.Val.eq, so it is probably possible to setup a sort of map from tags to printing functions, and to lookup functions in that map for printing ValExt values. I think you want this mechanism to be extensible so that new tags defined in Ltac2 extensions (via plugins) can also be given printers.
Gaëtan Gilbert (May 14 2023 at 17:12):I would not expect a ltac2 debugger to be merged considering how the ltac1 debugger went.
Even getting reviews may be difficult.
Jim Fehrle (May 14 2023 at 17:44):I would not expect a ltac2 debugger to be merged considering how the ltac1 debugger went.
What do you mean by "how the Ltac1 debugger went"?
Gaëtan Gilbert (May 15 2023 at 12:30):it took a long time to get merged because the maintainers did not approve much of the design
ltac2 being stricter than ltac1 means a similar situation results in no merge
Jason Gross (May 15 2023 at 15:21):I was under the impression that most of the issues were about the storing of location information in the tactic AST, and most of the remaining issues were about adding features to CoqIDE at all?
I, at least, would be interested in getting Set Ltac2 Debug. Set Ltac2 Batch Debug. in coqtop, so I don't have to rely on printf debugging quite so much. AIUI, this part of the infrastructure should be independent both of coqide and of the vo format / location information, and so I expect this part of the infrastructure to not run into the same issues. Does this match the expectations of other devs? And @Jim Fehrle is implementing this part separately/first feasible/useful on your roadmap to full Ltac2 debugger support?
Michael Soegtrop (May 15 2023 at 20:13):I would appreciate if the core team would support Jim in his endeavours. Sure the Ltac1 debugger had sever issues initially, which have been fixed. If the design is not agreeable, an agreeable design should be discussed upfront and/or in a cloder loop than happened with the Ltac1 debugger. Definitely the Ltac1 debugger as is is very nice and useful and I would very much appreciate similar functionality for Ltac2.
My own code has sufficient amounts of debug prints (by default disabled) to debug it in case the need arises, but I am not sure what I would do if I ran into the situation of having to analyse tactics of the complexity of the VST automation written in Ltac2. Sure Ltac2 is a much nicer type safe language with much less need for debugging, but on the other hand I am doing substantially more complicated stuff with it than with Ltac1.
Jim Fehrle (May 16 2023 at 03:07):@Jason Gross We came up with a good way to store the location information in the AST. I have no concerns about that.
My intention at the moment (subject to input from you and others) is not to support Batch Debug for Ltac2. I thought the ability to step backwards in an Ltac/Ltac2 script that you suggested would make that unnecessary.
And @Jim Fehrle is implementing this part separately/first feasible/useful on your roadmap to full Ltac2 debugger support?
That's not my current plan. My current code already steps through Ltac2 source code nicely. No CoqIDE changes required (though I expect to make a few small improvements in CoqIDE, such as additional menu items/function keys). I still need to figure out how to extract constrs from ValExt so you'll see values for such variables. I spent a couple hours on @Rodolphe Lepigre's suggestion to no avail, but I have a couple other ideas to try tomorrow. There's also the issue I raised here, which is solvable despite the snark. I think users could live with that behavior in the initial Ltac2 support.
Jim Fehrle (May 16 2023 at 03:26):Gaëtan Gilbert it took a long time to get merged because the maintainers did not approve much of the design
ltac2 being stricter than ltac1 means a similar situation results in no merge
They didn't suggest any alternative design, either, which I would have happily discussed. The debugger design has a lot of constraints. We should be looking for reasonable solutions (not the "optimal" solution) that provide significant value to users with a good ratio of effort to value.
I did add code that Emilio requested so the debugger can work with vsCoq2. Many of the review comments were on the level of "you can't have this variable".
Jason Gross (May 16 2023 at 04:27):@Michael Soegtrop The type safety is not enough when the code needs to be performant. I had a lot of trouble debugging Ltac2 PHOAS reification code where I was using Constr.Unsafe everywhere and couldn't even check the constrs in most places for debugging because the necessary context variables were not in scope (because evar context management is too expensive).
Rodolphe Lepigre (May 16 2023 at 05:54):I spent a couple hours on @Rodolphe Lepigre's suggestion to no avail, but I have a couple other ideas to try tomorrow.
If you need more help looking into this, I'm happy to have a look. (Did my answer to your DM help?)
Paolo Giarrusso (May 16 2023 at 11:49):There's also the issue I raised here, which is solvable despite the snark
What they fail to say seems that the "somewhere else" you must find type info must be in the typechecked program, like you'd have to do in C (or even C++ without runtime type identification). That types are aggressively erased from programs is a performance feature, not a bug, but it sure requires more work for debugging.
Paolo Giarrusso (May 16 2023 at 11:53):regardless, if a debugger is a useful feature (I'd say yes), the core team could prioritize it appropriately and provide such core functionality. Especially because (without knowing this codebase, but knowing this design) mapping runtime locations to types seems the kind of feature that'd be pretty coupled with any code transformation/optimization.
Enrico Tassi (May 16 2023 at 12:11):Definitely the Ltac1 debugger as is is very nice and useful and I would very much appreciate similar functionality for Ltac2.
Just to be clear, the problems which were mentioned in the integration of the Ltac1 debugger are about how it was done, not about the functionality it provides (which is great, no questioning that). I concur with Gaetan that we should do better next time, and discuss the design before coding, or start with a prototype but then be ready to properly rewrite it.
Jim Fehrle (May 16 2023 at 20:05):I concur with Gaetan that we should do better next time, and discuss the design before coding, or start with a prototype but then be ready to properly rewrite it.
It will be a prototype. I'm open to rewriting, but I'd need to work with someone who's willing to respond in a reasonable amount of time, have real discussion and make an effort to understand my comments rather than ignoring them. (Understanding doesn't necessarily mean agreement.)
Jim Fehrle (May 18 2023 at 01:43):The value for patsin Pattern.v multi_match! as seen in the debugger has more nesting than I expected (i.e. the parts circled in red). If the nesting isn't needed, perhaps this can be simplified? (The patterns are True, False and _.)
Gaëtan Gilbert (May 18 2023 at 08:45):that's just a linked list
Jim Fehrle (May 18 2023 at 23:47):In other cases it could be a conventional array? If it's always a linked list it could be printed more simply as a list.
Gaëtan Gilbert (May 19 2023 at 08:02):that is why we said you need type aware printing
Last updated: Oct 12 2024 at 12:01 UTC