added current goal info to dependent evars line #2
Conversation
This was broken by change 6608f64.
- added option to first print_dependent_evars arg to fix typing error - folded mapping info into the first part, removing other mapping info code - deleted code that made the output prettier - this is not for humans anyway - added info for evars in the current goal - this also contains instantiated evars, users interested in only the open ones need to filter themselves - change pr_subgoals to call print_dependent_evars without a goal argument, when pr_first is false - these are the cases when there is no current goal
| @@ -741,7 +739,8 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map | |||
| pr_rec 1 (g::l) | |||
| in | |||
| let pr_evar_info gl sigma seeds = | |||
| print_evar_constraints gl sigma ++ print_dependent_evars gl sigma seeds | |||
| let first_goal = if pr_first then gl else None in | |||
| print_evar_constraints gl sigma ++ print_dependent_evars first_goal sigma seeds | |||
There was a problem hiding this comment.
added option to first print_dependent_evars arg to fix typing error
Actually because you're passing None here, so of course you need to update the declaration
There was a problem hiding this comment.
Of course not. The None is inside an if, therefore gl must have (and always had) the type Goal.goal option. Otherwise the compiler would complain about incompatible types in this line.
There was a problem hiding this comment.
You can see the typing error, if you annotate the gl argument of print_dependent_evars in printer.ml with the type that you require in printer.mli in 912527f.
printing/printer.ml
Outdated
| if !should_print_dependent_evars then | ||
| let evars = Evarutil.gather_dependent_evars sigma seeds in | ||
| let evars_pp = Evar.Map.fold (fun e i s -> | ||
| let e' = pr_internal_existential_key e in | ||
| let sep = if s = (str "") then "" else ", " in | ||
| s ++ str sep ++ e' ++ |
There was a problem hiding this comment.
deleted code that made the output prettier - this is not for humans anyway
This seems to be just a minor difference in coding style/opinion, not essential to the goal of the PR. Better to avoid unnecessary changes unless there is a good reason. It distracts from the important changes. Everyone's style is a bit different.
There was a problem hiding this comment.
I wouldn't say it's coding style - it's about the style and readability of the produced output. But I agree, it is not essential.
printing/printer.ml
Outdated
| cut () ++ cut () ++ | ||
| str "(dependent evars: " ++ evars_pp ++ str ";" ++ cut () ++ | ||
| str "mapping: " ++ (pr_map sigma map_evars) ++ str ")" |
There was a problem hiding this comment.
folded mapping info into the first part, removing other mapping info code
Was this a necessary change or nice to have? Just to be clear.
There was a problem hiding this comment.
There are three changes in these two lines, for every one the answer is different:
- removal of
cut (): this is a code simplification, neither necessary nor related to the goal of the PR, similar to the simplification of the separators above. - removal of
pr_map: Not necessary, but very nice to have. I produce the mapping information in a, IMO, much simpler way, without the pr_map function and the calls toEvar.Map.bindingsthat were introduced in 912527f. As I said before, I would suggest to squash an updated version of this change with 912527f, such thatpr_mapwill never appear in the master branch. - addition of
evars_current_pp: necessary, this produces the output according to requirement 4 of Incomplete evars info when 'Printing Dependent Evars Line' enabled coq/coq#10420
|
Jim Fehrle <[email protected]> writes:
Actually because you're passing None here, so of course you need to update the declaration
No. The code in printer.ml does always pass goal option's to
print_dependent_evars. Try to annotate the gl argument with (gl :
Evar.t), what is specified in the mli in your patch, and you shall
see the typing error. Your PR does only compile, because the gl
argument is not used inside print_dependent_evars.
|
| let evars_current = Evarutil.gather_dependent_evars sigma [ gl ] in | ||
| Evar.Map.fold (fun e _ s -> | ||
| s ++ (pr_internal_existential_key e) ++ (str " ")) | ||
| evars_current (str "current goal: ") |
There was a problem hiding this comment.
1 The output after the eapply strange_imp_trans step is:
(dependent evars: ?X4 : ?P open, ?X5 : ?Q open, ; current goal: ?X5 )
However, the current goal is actually ?Goal. ?X5 = ?Q is not. Is the label current goal wrong or is the value wrong?
eapply strange_imp_trans.
4 focused subgoals
(shelved: 2) (ID 6)
P1, P2, P3, P4 : Prop
p12 : P1 -> P2
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
?Q -> P4
subgoal 2 (ID 7) is:
?P -> ?Q
subgoal 3 (ID 8) is:
?P -> ?Q
subgoal 4 (ID 9) is:
?P
p14 < Show Existentials.
<excerpted>
Existential 3 =
?Goal : [P1 : Prop
P2 : Prop
P3 : Prop
P4 : Prop
p12 : P1 -> P2
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4 |- ?Q -> P4]
2 It's odd to see fold here, which suggests there could be multiple elements in the mapping. There can only be one current goal. Would be clearer with something that makes this clear, such as Evar.Map.find_first. You might add a temporary check that Evar.Map.cardinal is 1.
There was a problem hiding this comment.
However, the current goal is actually
?Goal.?X5 = ?Qis not. Is the labelcurrent goalwrong or is the value wrong?
The evars after current goal are the evars used inside the current goal, see the feature description in coq#10420. This is not the current goal.
2 It's odd to see
foldhere, which suggests there could be multiple elements in the mapping. There can only be one current goal.
Please read my comment in PR coq#10489 from Jul 24, 2019, 10:42 pm GMT+2, there you see an example with multiple evars after current goal. The code uses Evarutil.gather_dependent_evars, which does not return the current goal, but rather all the evars used in the evar argument list, which is something completely different in most cases.
jfehrle
force-pushed
the
dependent_evars
branch
3 times, most recently
from
1af4f8b
to
1d5eba7
Compare
jfehrle
force-pushed
the
dependent_evars
branch
2 times, most recently
from
5d5393a
to
04105f0
Compare
The conclusion of WF-MOD2 was WF(E; Mod(X:S1[:=S2]))[]. But S2 should not be optional. In the case that S2 is not given here, WF-MOD2 is same as WF-MOD1 with meaningless premises for S2. coq@81f1219 changes the macro \Mod as: -\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}:={#3})} +\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}\,\zeroone{:={#3}})} So, "[" and "]" added in WF-MOD2 seems accidental.
For instance Reserved Notation "#0 #1" (at level 30). Reserved Notation "#0 #1 #2" (at level 40). (* Warning: Notations "#0 #1" defined at level 30 and "#0 #1 #2" defined at level 40 have incompatible prefixes. [prefix-incompatible-level,parsing,default] *) Reserved Notation "coq#20 coq#21 x #3 y" (x at level 30, at level 50). Reserved Notation "coq#20 coq#21 x coq#34" (x at level 40, at level 50). (* Warning: Notations "coq#20 coq#21 _ #3 _" defined at level 50 with arguments constr at level 30 and "coq#20 coq#21 _ coq#34" defined at level 50 with arguments constr at level 40 have incompatible prefixes. [prefix-incompatible-level,parsing,default] *)
instantiated evars, users interested in only the open ones need to filter
themselves
when pr_first is false - these are the cases when there is no current goal