Stream: Isabelle/ML

Topic: Change theory data in proof

Hanno Becker (Apr 25 2023 at 19:51):

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'.

Hanno Becker (Apr 25 2023 at 19:53):

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

Hanno Becker (Apr 26 2023 at 13:44):

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.

Hanno Becker (May 01 2023 at 13:38):

Any ideas on this one?

Lukas Stevens (May 01 2023 at 13:58):

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.

Mathias Fleury (May 01 2023 at 15:49):

Isabelle has a timing panel

Mathias Fleury (May 01 2023 at 15:50):

that shows the timings from different tactics

Mathias Fleury (May 01 2023 at 15:50):

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

Hanno Becker (May 02 2023 at 05:21):

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: May 04 2024 at 12:26 UTC