Skip to content

Commit 23027dc

Browse files
VilletaneuseVilletaneuse
committed
Add the mktoc tool to make a table of content
The `mktoc` script is in `dev/tools`. It is mostly in `awk`. There are 2 test cases in `dev/tools/test/mktoc` with a `Makefile` in `tools/test`. I improvised this directory hierarchy; it is not set in stone.
1 parent d902193 commit 23027dc

File tree

6 files changed

+495
-0
lines changed

6 files changed

+495
-0
lines changed

‎dev/tools/mktoc

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
#!/bin/sh
2+
3+
usage()
4+
{
5+
cat <<EOF
6+
Usage: mktoc FILE...
7+
Number sections, subsections and subsubsections in coqdoc'ed documented
8+
Coq FILEs.
9+
Also write a Table of content after a line
10+
*** Table of content
11+
if it is present in the file.
12+
The section, subsection and subsubsections have the following format:
13+
(** ** A section *)
14+
(** *** A subsection *)
15+
(** **** A subsubsection *)
16+
17+
It is possible to reuse mktoc on the same file (e.g. to update the numbering and
18+
table of content after some changes).
19+
EOF
20+
}
21+
22+
case $0 in
23+
0)
24+
usage
25+
exit 1
26+
esac
27+
28+
case $1 in
29+
-h | --help)
30+
usage
31+
exit 0
32+
esac
33+
34+
tmptoc=tmptoc$$.tmp
35+
tmpfile=tmp_mktoc_$$.tmp
36+
TOCSTRING='\\*\\*\\* Table of content'
37+
38+
trap "rm -vf $tmptoc $tmpfile" EXIT SIGINT SIGTERM SIGABRT
39+
40+
for f; do
41+
# First pass to get the numbering right and write the TOC in a temporary file
42+
>"$tmptoc"
43+
awk -v "tmp=$tmptoc" '
44+
function spaces(num_spaces) {
45+
res = "";
46+
for (i = 0; i < num_spaces; i++)
47+
res = " " res;
48+
return res;
49+
}
50+
function remove_numbering() {
51+
if ($3 ~ /^[0-9.]+$/)
52+
$3 = "";
53+
gsub(/[[:blank:]]+/, " ");
54+
}
55+
BEGIN {
56+
nb_levels = 0;
57+
}
58+
/^\(\*\*[[:blank:]]+\*\*+/ {
59+
remove_numbering()
60+
61+
level = length($2) - 1;
62+
if (level > nb_levels)
63+
nb_levels = level
64+
65+
numbering[level - 1]++;
66+
for (i = level; i < nb_levels; i++)
67+
numbering[i] = 0
68+
69+
title = $3;
70+
for (i = 4; i < NF; i++)
71+
title = title " " $i
72+
73+
if (level == 1) {
74+
item = numbering[level - 1] ".";
75+
} else {
76+
item = numbering[0];
77+
for (i = 1; i < level; i++)
78+
item = item "." numbering[i]
79+
}
80+
81+
printf("(** %s %s %s *)\n", $2, item, title);
82+
printf("%s- %s %s\n", spaces(2 * (level - 1)), item, title) >>tmp
83+
next
84+
}
85+
1
86+
' <"$f" >"$tmpfile"
87+
88+
mv "$tmpfile" "$f"
89+
90+
# Second pass to write the TOC
91+
awk -v "tmp=$tmptoc" -v "tocstring=$TOCSTRING" '
92+
function spaces(num_spaces) {
93+
res = "";
94+
for (i = 0; i < num_spaces; i++)
95+
res = " " res;
96+
return res;
97+
}
98+
$0 ~ tocstring {
99+
# we need to save the indentation level
100+
match($0, /^ */);
101+
indent = RLENGTH;
102+
print $0;
103+
# next line(s) should be empty, we also skip any previous TOC
104+
do {
105+
getline
106+
} while ($0 ~ /^ *$/ || $0 ~ /^ *- [0-9][0-9.]+/);
107+
# now we need to dump the new TOC
108+
printf("\n");
109+
while (getline line <tmp) {
110+
printf("%s%s\n", spaces(indent), line)
111+
}
112+
printf("\n");
113+
}
114+
1
115+
' <"$f" >"$tmpfile"
116+
117+
mv "$tmpfile" "$f"
118+
done

‎dev/tools/test/Makefile

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
all: test-mkdoc
2+
3+
test-mkdoc:
4+
if [ -d mktoc/out ]; then rm -r mktoc/out; fi
5+
mkdir mktoc/out
6+
cp mktoc/example1.v mktoc/example2.v mktoc/out
7+
../mktoc mktoc/out/example1.v mktoc/out/example2.v
8+
@diff mktoc/out/example1.v mktoc/expected/example1.v || \
9+
printf "test-mkdoc example1.v FAILED\n" 1>&2 && \
10+
printf "test-mkdoc example1.v SUCCEEDED\n" 1>&2
11+
@diff mktoc/out/example2.v mktoc/expected/example2.v || \
12+
printf "test-mkdoc example2.v FAILED\n" 1>&2 && \
13+
printf "test-mkdoc example2.v SUCCEEDED\n" 1>&2
14+
rm -r mktoc/out

‎dev/tools/test/mktoc/example1.v

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
(** * Test file 1 for mktoc
2+
3+
*** Table of content
4+
5+
Here is some random text we hope will remain after mktoc.
6+
7+
*** Some other part of this tutorial's header
8+
*)
9+
10+
(** In this tutorial, we are going to search for lemmas, mostly about natural
11+
numbers.
12+
13+
We already have all lemmas and definitions from the prelude ([Coq.Init]),
14+
and we require the library file [Coq.Arith.PeanoNat] which adds hundreds
15+
of new constants.
16+
*)
17+
18+
From Coq Require Import PeanoNat.
19+
20+
(** ** 42. Basic [Search] queries *)
21+
22+
(** In its most basic form, one searches for lemmas or definitions containing
23+
- a given constant, eg [Nat.add], or [nat]
24+
- a given string to be part of the identifier
25+
- a given notation
26+
*)
27+
28+
(** Search all lemmas where the type [nat] and the operators (_ * _) and
29+
(_ + _) occur. *)
30+
Search nat (_ + _) (_ * _). (* still too much *)
31+
32+
(** ** 3.3.5 More sophisticated patterns *)
33+
34+
(** Some text *)
35+
36+
(** ** Filter results by logical kind and or syntax in queries *)
37+
38+
(** We can also [Search] for a constant defined with a specific keyword.
39+
For instance, the following lists all [Lemma]s whose names contain "add"
40+
and types contain [0]: *)
41+
Search "add" 0 is:Lemma.
42+
43+
(** ** 10.1 Disambiguating strings in Search queries *)
44+
45+
(** *** Some subsection *)
46+
47+
(** **** 2 Some subsubsection *)
48+
49+
(** We have seen two different usages of strings in search queries, namely,
50+
searching for constants whose name contains the string, such as: *)
51+
Search "comm".
52+
53+
(** **** 42 Another one *)
54+
55+
(** or, search for constants whose type contain a notation, such as: *)
56+
Search "||".
57+
Search "+".
58+
59+
(** *** A Great subsection *)
60+
61+
(** **** A subsubsection ! *)
62+
63+
(** We have seen two different usages of strings in search queries, namely,
64+
searching for constants whose name contains the string, such as: *)
65+
Search "comm".
66+
67+
(** **** Another subsubsection *)
68+
69+
(** With some text inside *)
70+
71+
(** **** Yet another subsubsection *)
72+
73+
(** So, what really happens here?
74+
Blah, blah, ... *)
75+
76+
(** ** Searching for constants with given hypotheses (parameters) or conclusions (return type) *)
77+
78+
(** Finally the [head] keyword is just a shorthand for [headconcl] or [headhyp]: *)
79+
Search head:"<->".
80+
81+
(** ** 0.0.0 Searching inside or outside a specific module *)
82+
83+
(** We hope mktoc works. *)

‎dev/tools/test/mktoc/example2.v

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
(** * Test file 1 for mktoc with a garbage TOC to remove
2+
3+
*** Table of content
4+
5+
- 1. This
6+
- 1.1 That
7+
- 1.2 One
8+
- 2. A
9+
- 2.1 B
10+
- 2.2 C
11+
12+
*** Some other part of this tutorial's header
13+
*)
14+
15+
(** In this tutorial, we are going to search for lemmas, mostly about natural
16+
numbers.
17+
18+
We already have all lemmas and definitions from the prelude ([Coq.Init]),
19+
and we require the library file [Coq.Arith.PeanoNat] which adds hundreds
20+
of new constants.
21+
*)
22+
23+
From Coq Require Import PeanoNat.
24+
25+
(** ** 42. Basic [Search] queries *)
26+
27+
(** In its most basic form, one searches for lemmas or definitions containing
28+
- a given constant, eg [Nat.add], or [nat]
29+
- a given string to be part of the identifier
30+
- a given notation
31+
*)
32+
33+
(** Search all lemmas where the type [nat] and the operators (_ * _) and
34+
(_ + _) occur. *)
35+
Search nat (_ + _) (_ * _). (* still too much *)
36+
37+
(** ** 3.3.5 More sophisticated patterns *)
38+
39+
(** Some text *)
40+
41+
(** ** Filter results by logical kind and or syntax in queries *)
42+
43+
(** We can also [Search] for a constant defined with a specific keyword.
44+
For instance, the following lists all [Lemma]s whose names contain "add"
45+
and types contain [0]: *)
46+
Search "add" 0 is:Lemma.
47+
48+
(** ** 10.1 Disambiguating strings in Search queries *)
49+
50+
(** *** Some subsection *)
51+
52+
(** **** 2 Some subsubsection *)
53+
54+
(** We have seen two different usages of strings in search queries, namely,
55+
searching for constants whose name contains the string, such as: *)
56+
Search "comm".
57+
58+
(** **** 42 Another one *)
59+
60+
(** or, search for constants whose type contain a notation, such as: *)
61+
Search "||".
62+
Search "+".
63+
64+
(** *** A Great subsection *)
65+
66+
(** **** A subsubsection ! *)
67+
68+
(** We have seen two different usages of strings in search queries, namely,
69+
searching for constants whose name contains the string, such as: *)
70+
Search "comm".
71+
72+
(** **** Another subsubsection *)
73+
74+
(** With some text inside *)
75+
76+
(** **** Yet another subsubsection *)
77+
78+
(** So, what really happens here?
79+
Blah, blah, ... *)
80+
81+
(** ** Searching for constants with given hypotheses (parameters) or conclusions (return type) *)
82+
83+
(** Finally the [head] keyword is just a shorthand for [headconcl] or [headhyp]: *)
84+
Search head:"<->".
85+
86+
(** ** 0.0.0 Searching inside or outside a specific module *)
87+
88+
(** We hope mktoc works. *)

0 commit comments

Comments
 (0)