look for certificates relative to the theory
authorboehmes
Fri Nov 12 15:56:07 2010 +0100 (2010-11-12)
changeset 405131204d268464f
parent 40512 fd218201da5e
child 40514 db5f14910dce
look for certificates relative to the theory
src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
src/HOL/Boogie/Examples/Boogie_Max.thy
src/HOL/Boogie/Examples/VCC_Max.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/SMT_Examples/SMT_Word_Examples.thy
src/HOL/Tools/SMT/smt_config.ML
     1.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Fri Nov 12 15:56:06 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Fri Nov 12 15:56:07 2010 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5  boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
     1.6  
     1.7 -declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
     1.8 +declare [[smt_certificates="Boogie_Dijkstra.certs"]]
     1.9  declare [[smt_fixed=true]]
    1.10  declare [[smt_oracle=false]]
    1.11  
     2.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 12 15:56:06 2010 +0100
     2.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 12 15:56:07 2010 +0100
     2.3 @@ -38,7 +38,7 @@
     2.4  
     2.5  boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
     2.6  
     2.7 -declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Max.certs"]]
     2.8 +declare [[smt_certificates="Boogie_Max.certs"]]
     2.9  declare [[smt_fixed=true]]
    2.10  declare [[smt_oracle=false]]
    2.11  
     3.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy	Fri Nov 12 15:56:06 2010 +0100
     3.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Fri Nov 12 15:56:07 2010 +0100
     3.3 @@ -46,7 +46,7 @@
     3.4  
     3.5  boogie_open (quiet) "~~/src/HOL/Boogie/Examples/VCC_Max"
     3.6  
     3.7 -declare [[smt_certificates="~~/src/HOL/Boogie/Examples/VCC_Max.certs"]]
     3.8 +declare [[smt_certificates="VCC_Max.certs"]]
     3.9  declare [[smt_fixed=true]]
    3.10  declare [[smt_oracle=false]]
    3.11  
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 12 15:56:06 2010 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 12 15:56:07 2010 +0100
     4.3 @@ -7,7 +7,7 @@
     4.4    imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
     4.5  begin
     4.6  
     4.7 -declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]]
     4.8 +declare [[smt_certificates="Integration.certs"]]
     4.9  declare [[smt_fixed=true]]
    4.10  declare [[smt_oracle=false]]
    4.11  
     5.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Nov 12 15:56:06 2010 +0100
     5.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Nov 12 15:56:07 2010 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  begin
     5.5  
     5.6  declare [[smt_solver=z3, smt_oracle=false]]
     5.7 -declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Examples.certs"]]
     5.8 +declare [[smt_certificates="SMT_Examples.certs"]]
     5.9  declare [[smt_fixed=true]]
    5.10  
    5.11  
     6.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Nov 12 15:56:06 2010 +0100
     6.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Fri Nov 12 15:56:07 2010 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4  begin
     6.5  
     6.6  declare [[smt_solver=z3, smt_oracle=false]]
     6.7 -declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Tests.certs"]]
     6.8 +declare [[smt_certificates="SMT_Tests.certs"]]
     6.9  declare [[smt_fixed=true]]
    6.10  
    6.11  
     7.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Nov 12 15:56:06 2010 +0100
     7.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Nov 12 15:56:07 2010 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  begin
     7.5  
     7.6  declare [[smt_solver=z3, smt_oracle=true]]
     7.7 -declare [[smt_certificates="~~/src/HOL/SMT_Examples/SMT_Word_Examples.certs"]]
     7.8 +declare [[smt_certificates="SMT_Word_Examples.certs"]]
     7.9  declare [[smt_fixed=true]]
    7.10  
    7.11  
     8.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Fri Nov 12 15:56:06 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Nov 12 15:56:07 2010 +0100
     8.3 @@ -173,9 +173,12 @@
     8.4  val get_certificates_path =
     8.5    Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
     8.6  
     8.7 -fun select_certificates name = Certificates.put (
     8.8 +fun select_certificates name context = context |> Certificates.put (
     8.9    if name = "" then NONE
    8.10 -  else SOME (Cache_IO.make (Path.explode name)))
    8.11 +  else
    8.12 +    Path.explode name
    8.13 +    |> Path.append (Thy_Load.master_directory (Context.theory_of context))
    8.14 +    |> SOME o Cache_IO.make)
    8.15  
    8.16  val certificates_of = Certificates.get o Context.Proof
    8.17