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