coq/test-suite/unit-tests, branch master

Change OUnit package name to ounit2.

2020-08-18T10:39:02+00:00

OUnit package name is changed from "oUnit" to "ounit2":
https://github.com/gildor478/ounit#user-content-transition-to-ounit2

This change follows it and fixes
a failure, `ocamlfind: Package oUnit not found`,
at `make test-suite` and `dune build`.

Revert "[test] unit tests for ide/coq_lex.ml" + makefile support

2020-05-17T11:22:09+00:00

This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and
0976a670cf853c9bc61b3eee6dceae4a429e066f.

Fix proof_diffs_test.ml

2020-05-17T11:22:09+00:00

[test] unit tests for ide/coq_lex.ml

2019-06-19T11:27:37+00:00

Make prvect tail recursive (fix #9355)

2019-01-22T13:09:34+00:00

Using a unit test as it's way faster than messing with universes.

You can test with universes by
~~~coq
Set Universe Polymorphism.
Definition x1@{i} := True.
Definition x2 := x1 -> x1.
Definition x3 := x2 -> x2.
Definition x4 := x3 -> x3.
Definition x5 := x4 -> x4.
Definition x6 := x5 -> x5.
Definition x7 := x6 -> x6.
Definition x8 := x7 -> x7.
Definition x9 := x8 -> x8.
Definition x10 := x9 -> x9.
Definition x11 := x10 -> x10.
Definition x12 := x11 -> x11.
Definition x13 := x12 -> x12.
Definition x14 := x13 -> x13.
Definition x15 := x14 -> x14.
Definition x16 := x15 -> x15.
Definition x17 := x16 -> x16.
Definition x18 := x17 -> x17.
Definition x19 := x18 -> x18.

About x19. (* 262144 universes *)
~~~
Note on my machine `About x18.` did not overflow even before this
commit.

Make diffs work for more input strings

2018-12-20T21:01:46+00:00

Diff code uses the lexer to recognize tokens in the inputs, which can be
Pp.t's or strings.  To add the highlights in the Pp.t, the diff code
matches characters in the input to characters in the tokens.  Current
code fails for inputs containing quote marks or "(*" because the quote
marks and comments don't appear in the tokens.  This commit adds a "diff
mode" to the lexer to return those characters, making the diff routine
more robust.

Get hyps and goal the same way Printer does; don't omit info

2018-11-14T20:19:14+00:00

Allow for new goals that don't map to old goals
Include background_goals in all_goals return value
Fix incorrect change to raw diffs in shorten_diff_span
Fixes #8922

Make tokenize_string an optional parameter for diff methods in pp_diffs.

2018-07-24T03:13:29+00:00

Remove forward reference to lexer.

Displays the differences between successive proof steps in coqtop and CoqIDE.

2018-07-24T03:13:19+00:00

Proof General requires minor changes to make the diffs visible, but this code
shouldn't break the existing version of PG.

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.

Make the out_channel for the log file accessible so tests can write to it (e.g. for debugging)

2018-07-23T15:25:11+00:00