HTML output for diffs #1
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
a) not explicitly setting the default value and b) not repeating attributes that are already set. Example (omitting escape character): Old: E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m New: E : [92mev[0m n (92 is bright green, the other codes set default attributes).
… CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Also provides an option to generate diffs in HTML in a file. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or "-diffs on|off|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and "end.diff.*", but only on the first and last strings of the span.
(cherry picked from commit 096afff)
2 tasks
jfehrle
force-pushed
the
diffs
branch
4 times, most recently
from
b0672f9
to
fca201d
Compare
jfehrle
force-pushed
the
diffs
branch
2 times, most recently
from
ca90aa1
to
6e2e2ed
Compare
jfehrle
force-pushed
the
diffs
branch
9 times, most recently
from
2439864
to
2cf033a
Compare
jfehrle
force-pushed
the
diffs
branch
2 times, most recently
from
b166ae5
to
7a844ad
Compare
jfehrle
force-pushed
the
diffs
branch
4 times, most recently
from
a45adb6
to
97069f6
Compare
jfehrle
pushed a commit
that referenced
this pull request
Jan 22, 2019
add some more material (preliminary provided in "tuto2" directory)
jfehrle
pushed a commit
that referenced
this pull request
Nov 15, 2021
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.
jfehrle
pushed a commit
that referenced
this pull request
Mar 5, 2022
\Indp and \Indpstr contains "(#1)" but all uses of \Indp and \Indpstr has empty first argument: \Indp{}... and \Indpstr{}... When the macros are introduced, \Ind also had "(#1)". coq@384d390 coq@81f1219 Later, \Ind removes "(#1)". coq@b94bdd3 "(#1)" was used to represent the local context of inductive definitions. So, we can remove "(#1)" from \Indp and \Indpstr.
jfehrle
pushed a commit
that referenced
this pull request
Jun 5, 2024
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] *)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Generate an HTML file with proof diffs. It is probably not general enough to be merged yet. Code is extracted from coq#6801 to allow for a good discussion of what this should be.
This is based on the jfehrle/coq/diffs branch, which hasn't been merged. Not sure if this this PR is useful as such or if I need to wait until diffs is merged (advice welcome).