README.md
1
2ProofCount
3==========
4
5ProofCount is a tool that collects metrics from finished
6Isabelle proofs. Specifically it finds the starting and ending
7lines for each lemma.
8The result of this count is saved in
9an xml file that can then be processed for metric analysis.
10Additionally the constant dependency graph is saved,
11as well as the theory dependency graph. This file
12can then be processed to compute metrics on the proof.
13
14
15Quickstart
16----------
17
18To use ProofCount you need to install it as an isabelle component.
19
20The script "install.sh" found in the main proofcount directory
21takes an isabelle executable and adds ProofCount as a component to it.
22
23Usage:
24
25 ./install.sh isabelle [-P]
26
27The -P option will patch the given isabelle install (after installing proofcount)
28to enable metric collection, by applying "isabelle\_patch.diff".
29
30
31Once proofcount is installed it can be executed as an isabelle tool:
32
33 isabelle proofcount -x l4v.xml -d ~/verification/l4v -L AInvs -T AInvs
34
35This will re-check the invariant proof and emit l4v.xml when finished. This
36file contains the line information for each lemma, the lemma dependency graph,
37the constants used in each lemma, the constant dependency graph and the theory
38dependency graph.
39
40Once this file exists, we can use proofcount to perform its default metric analysis.
41
42 isabelle proofcount -x l4v.xml -N AInvs -s Lib -s CapRights\_A -b Invariants\_AI -f AInvs.akernel\_invs
43
44This will emit a single metric calculation from the proofs in l4v.xml called "AInvs". The constant
45dependency graph will be restricted to those constants which depend on the "CapRights\_A" or "Lib" theories.
46The lemma dependency graph will be restricted to lemmas which depend on "Invariants\_AI", and
47are present in the dependencies for the top-level lemma "AInvs.akernel\_invs".
48
49Options
50-------
51Proofcount options are passed as usual command-line flags. There are roughly two categories of options,
52those which affect the actual proof counting and those which are used as part of the metric analysis.
53
54
55The options are:
56
57 * `-x FILE`: The name of the xml file, either as input or output depending on
58 if a proof is being counted or if metrics are being computed.
59
60 * Counting flags:
61
62 * `-d DIR`: The ROOT directory for building the proof to be counted.
63 Similar to the same flag given to `isabelle build`.
64
65 * `-L LOGIC`: The name of the logic image to build the proof against. It must
66 appear somewhere in the ROOTS files given in the ROOT directory.
67
68 * `-T THEORY`: The name of the top-level theory. All dependencies of this
69 theory will be counting.
70
71 * Metric flags:
72
73 * `-N NAME`: The name of the metric to be computed. Used to name the output files and
74 latex macros.
75
76 * `-D DIR`: The directory to output the resulting metrics.
77
78 * `-s THEORY`: A base `specification` theory. This flag may be given multiple times.
79 Any constant which does not depend on a base specification theory will not be considered
80 in metric collection. This is usually chosen liberally to include all constants defined as
81 part of a proof development.
82
83 * `-b THEORY`: A base `proof` theory. This flag may be given multiple times.
84 Any lemma which does not depend on a base proof theory will not be considered in
85 metric collection. This should be chosen carefully so that only lemmas
86 part of the desired proof are counted.
87
88 * `-t THEORY`: A top-level `proof` theory. This flag may be given multiple times.
89 Any lemma which depends on a top-level theory, but is not from that theory
90 (i.e. is `above` that theory) will not be considered in metric collection.
91 This is used in cases where multiple proofs are part of the given logic image
92 and we wish to separate them.
93
94
95 * `-f LEMMA`: The name of a top-level lemma statement. This flag may ba given multiple times.
96 Any lemma which is not in the recursive dependencies of a top-level lemma will
97 not be considered in metric collection. This is generally a single lemma that
98 is the `final` proof for the development.
99
100
101Output Files
102------------
103
104Metric computing produces multiple output files which can be used for analysis. For each
105named metric there are 4 files produced:
106
107 * NAME\_report.txt: This is an overview of the metric collection. It contains the total
108 number of lemmas counted, total number of lines counted as well as information
109 about the top-level statement. Additionally it gives information about what
110 specification and proof theories were used to compute the metric.
111
112 * NAME\_orphans.txt: This lists lemmas which were not in the dependency graph
113 of any given top-level fact. It says the same of the lemma, and its root
114 in the dependency graph, i.e. the topmost lemma that depends on it.
115
116 * NAME\_summary.tex: This is a latex file that defines
117 macros for some of the numbers in the report.
118
119 * metrics\_NAME\_num\_deps.txt: This is a machine-readable file which
120 has one entry per lemma, giving the specification size, idealized
121 specification size and proof size respectively.
122
123
124Specification Size
125------------------
126
127The specification size of a lemma is measured as the total number of unique constants
128required to write the lemma statement. This excludes constants which are outside
129of the theory range given by the `-s` option. The idealized specification size
130removes constants whose definitional lemmas do not appear in the dependency
131graph of the lemma.
132