search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Goals with large context #36

Open thery opened 3 years ago

thery commented 3 years ago

I have goals with very large context. When hovering over tactics. I mostly see the initial assumptions. Is there a way to activate some scrolling or at least have the visible part concentrated on the conclusion?

cpitclaudel commented 3 years ago

We could have a maximum height on the hypotheses area. I wonder if CSS has a way to say "truncate at top, not at bottom".

cpitclaudel commented 3 years ago

Related: #15

thery commented 3 years ago

maybe giving the possibility to display only the assumptions that have changed would be nice

Casteran commented 3 years ago

maybe giving the possibility to display only the assumptions that have changed would be nice

Giving options like (all-hyps -hyp1 -hyp2 ... ) or (no-hyps + hyp1 +hyp2 ... ) ?

thery commented 3 years ago

I was thinking more on something in the line of this where one displays onl waht has changed.

Casteran commented 3 years ago

Ok, I see! For my part, I’m working on using Alectryon for writing a pdf document. When commenting the main steps of a long proof, I often present some sub-goal, then the tactic for solving it. But displaying the full context results in a often hard to read block. So, I wish to display only the hypotheses which really matter.

Le 5 août 2021 à 12:12, Laurent Théry @.***> a écrit :

I was thinking more on something in the line of this https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#showing-differences-between-proof-steps where one displays onl waht has changed.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/alectryon/issues/36#issuecomment-893337826, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCR5FEQBZUY2I5MPV2TT3JPZHANCNFSM43DTAZ4Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email.

cpitclaudel commented 3 years ago

@thery I would love to do this, and it's been on my list for a while.

The problem is that Coq doesn't expose enough info right because the tree structure of goals is not exposed (there's no way to know which "parent" goal a new goal came from). This makes it hard to know what to compute diffs against: of course there's the problem of tactics like cycle or swap, but more importantly there's tactics that split cases: the first goal of the second case of an induction should be compared to the initial state, not to the last goal of the first case.

cpitclaudel commented 3 years ago

@Casteran I like this idea, even though it's a different use case indeed. I think it's just a matter of improving the annotation mini-language.

thery commented 3 years ago

I guess in my context as the context is very large, diff with sibling or ancestor both would do the trick. but I understand it could be difficult to do if Coq does not help. I am wondering how the diff is implemented when running coqtop -diffs on. Is there a way to get the info with serapi. Maybe @ejgallego knows.

cpitclaudel commented 3 years ago

-diffs on was implemented by @jfehrle; Jim, I'm hoping I didn't forget about a previous discussion, but apologies in advance if I did: how do you determine which old goal to compare a new goal against when computing diffs? IIRC in a proof by induction you don't show a diff for the first goal of a branch, right?

cpitclaudel commented 3 years ago

@Casteran I've implemented a prototype to allow you to select hypotheses and goals to display. It shares the language introduced for @jhaag in #2. Please see https://github.com/cpitclaudel/alectryon#controlling-output and the following sections.

Source:

image

Result:

image

thery commented 3 years ago

how do you determine which old goal to compare a new goal against when computing diffs?

Apparently diffs compares with the state before the tactical call which seems reasonable. I have tried

 forall P : nat -> Prop, (P 2 -> P 1 -> P 1 -> P 1) -> P 1

after intros P H, if I do apply H, it tells me that the first goal has changed while the others don't.

jfehrle commented 3 years ago

A short answer for now: The comments in proof_diffs.ml above match_goals explain a little. AFAIK the heuristic almost always recovers the parent/child relationships, but it can't handle a few tactics, such as clear, that modify parents rather than only resolving subgoals. I think serapi doesn't know about this info.

Well after creating that mapping, I learned that the kernel has a data structure with all evars (IIRC both resolved and unresolved), from which it would be even easier to recover these relationships and get the complete family tree of the contexts, then make it available through some API. The data structure match_goals operates on is derived from that kernel data structure.

Switching to the kernel data structure may not be entirely trivial but shouldn't be that hard.

IIRC in a proof by induction you don't show a diff for the first goal of a branch, right?

I think it would show a diff compared to the previous goal for both induction subgoals. Why don't you try it?

jfehrle commented 3 years ago

Also, db_goal_map will print the derived mapping.

jfehrle commented 3 years ago

And a few more comments above make_goal_map_i.

cpitclaudel commented 3 years ago

Thanks @jfehrle .

I think it would show a diff compared to the previous goal for both induction subgoals. Why don't you try it?

I did, and I didn't understand the result; hence the question:

image

It seems it shows diffs only in the first subproof?

@thery :

Apparently diffs compares with the state before the tactical call which seems reasonable.

The problem is: what is the "state before" for the second goal of an induction, when it gets focused?

Goal forall n: nat, n > 0 -> True.
  destruct n.
  - ….
  - (* Here *)
thery commented 3 years ago

not sure the diff works well with focus.

cpitclaudel commented 3 years ago

That, but also in the screenshot above, where there's no focus

jfehrle commented 3 years ago

@cpitclaudel ~I think you skipped over what I said above about that diff can't handle a few tactics, such as clear, that modify parents rather only resolving subgoals. Though I'm a little surprised you get a silent error rather than an exception. Perhaps you would submit an issue for this? See https://github.com/coq/coq/pull/14457 (in 8.14).~ You can see the diff here:

image

jfehrle commented 3 years ago

Though this gives the same diff result for your example:

image

The change is computed relative to the first previous non-trivial step rather than the parent goal. (cycle and swap are trivial). If we had the tree structure of the goals, it would be easy enough to compare against the parent, but it may confuse users because exact I didn't change the second goal. Off the top of my head, we could a) redefine diff as always in relation to the parent goal, b) make "a" a settable option, and/or c) provide some labelling like "diff relative to proof step 999" and include proof step numbers in the context display. But getting the parent without having the tree structure is rather unappealing--potentially you would need to examine many, many steps in some cases.

cpitclaudel commented 3 years ago

The change is computed relative to the first previous non-trivial step rather than the parent goal.

Got it, thanks.

But getting the parent without having the tree structure is rather unappealing

Yes, that's precisely the info I was talking about.