Hi! I'd like to persist some information about a proof in the surrounding `theory`

, but struggle. My attempt so far: Capture the desired data in a `Theory_Data`

, model the data logging as a `theory -> theory`

transform, lift that to `Proof.context -> Proof.context`

, and perform the latter as part of a `Method.method`

(which supports `Proof.context`

transformation). However, while within the proof I do see the `Theory_Data`

appropriately adjusted, after the proof the information is lost. I guess this is due to how `Proof.context`

and surrounding `theory`

are merged after a proof, but I can't figure out how to get it right. I also considered keeping the data as `Proof_Data`

during the proof and transferring it to the `theory`

when the proof concludes, but I don't know how/where one would add the desired 'merge hook'.

Here's the code for my failed attempt:

```
theory scratchpad
imports Main
begin
ML‹
structure Data = Theory_Data (
type T = int
val empty = 0
fun merge (a,b) = let val _ = "merge" |> tracing in a+b end
)
val lift: (Proof.context -> Proof.context) -> Method.method =
fn f => fn _ => fn (ctxt, st) => (f ctxt, st) |> Seq.single |> Seq.make_results
val lift' : (theory -> theory) -> Method.method =
Proof_Context.background_theory #> lift
›
method_setup change_state = ‹Scan.succeed ((fn i => i+1) |> Data.map |> lift' |> K)› ""
method_setup dump_state = ‹Scan.succeed (fn ctxt =>
let val _ = ctxt |> Proof_Context.theory_of |> Data.get |> Int.toString |> tracing in
Method.succeed end)›
ML‹val l = Data.get @{theory}› (* 0 *)
lemma ‹x=x›
apply dump_state (* 0 *)
apply change_state
apply dump_state (* 1 *)
apply change_state
apply change_state
apply dump_state (* 3 *)
by simp
ML‹val l = Data.get @{theory}› (* 0 *)
end
```

NB The reason I'm interested in this is tactic profiling. I'm gathering some metrics about specific tactic invocations, and would like to persist them in the `theory`

to be able to have a single statistics in the end. Currently, I can only analyze the data from individual proofs.

Any ideas on this one?

The best person to answer this would be Makarius but he only reads the mailing list. In general, this seems to go strongly against the idea of a local context.

Isabelle has a timing panel

that shows the timings from different tactics

However, in my experience, the timings vary so widely, that it is completely useless

I have asked on the mailing list. In my case, I do get very valuable timing statistics from proof-local custom profiling, but it would be even more useful if the statistics could be merged across multiple proofs and theories.

Last updated: Feb 27 2024 at 08:17 UTC