From f5c995467f8342e84bd73ac6d6bbd3c3281b2b4e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 14:30:10 +0100 Subject: Fixing encoding in coqdoc output tests. The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept. --- test-suite/Makefile | 4 ++-- test-suite/coqdoc/bug5648.html.out | 18 +++++++++--------- test-suite/coqdoc/bug5648.tex.out | 12 +++++++++++- test-suite/coqdoc/bug5700.html.out | 2 +- test-suite/coqdoc/bug5700.tex.out | 12 +++++++++++- test-suite/coqdoc/links.html.out | 6 +++--- test-suite/coqdoc/links.tex.out | 12 +++++++++++- 7 files changed, 48 insertions(+), 18 deletions(-) diff --git a/test-suite/Makefile b/test-suite/Makefile index 61e75fa5d3..7a204bfd81 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -549,8 +549,8 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR $(coqc) -R coqdoc Coqdoc $* 2>&1; \ cd coqdoc; \ f=`basename $*`; \ - $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ - $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \ + $(coqdoc) -utf8 -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \ diff -u --strip-trailing-cr $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \ grep -v "^%%" Coqdoc.$$f.tex | diff -u --strip-trailing-cr $$f.tex.out - 2>&1; S=$$?; times; \ if [ $$R = 0 -a $$S = 0 ]; then \ diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 06789c1c10..5c5a2dc299 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - + Coqdoc.bug5648 @@ -31,14 +31,14 @@
Definition d x :=
  match x with
-  | A => 0
-  | Add => 1
-  | G => 2
-  | Goal => 3
-  | L => 4
-  | Lemma => 5
-  | P => 6
-  | Proof => 7
+  | A ⇒ 0
+  | Add ⇒ 1
+  | G ⇒ 2
+  | Goal ⇒ 3
+  | L ⇒ 4
+  | Lemma ⇒ 5
+  | P ⇒ 6
+  | Proof ⇒ 7
  end.
diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out index b0b732effa..82f7da2309 100644 --- a/test-suite/coqdoc/bug5648.tex.out +++ b/test-suite/coqdoc/bug5648.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 0e05660d6c..b96fc6281d 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - + Coqdoc.bug5700 diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 33990cb89f..1a1af5dfdd 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index e2928f78d4..70cbe50657 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -2,7 +2,7 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - + Coqdoc.links @@ -57,7 +57,7 @@ Various checks for coqdoc Definition a (b: nat) := b.

-Definition f := forall C:Prop, C.
+Definition f := ∀ C:Prop, C.

Notation "n ++ m" := (plus n m).
@@ -74,7 +74,7 @@ Various checks for coqdoc Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).

-Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A
+Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A

where "x = y :> A" := (@eq A x y) : type_scope.
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index de3182d1a0..7d93189ae2 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -1,5 +1,15 @@ \documentclass[12pt]{report} -\usepackage[]{inputenc} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{coqdoc} -- cgit v1.2.3