Making isabelle run on modern z3. · General

Stream: General

Topic: Making isabelle run on modern z3.

irvin (Oct 10 2024 at 00:49):

Making a new thread to distinguish from the previous thread on making isabelle run on musl-c

irvin (Oct 10 2024 at 00:49):

https://www21.in.tum.de/~boehmes/proofrec.pdf
think this is the paper?

irvin (Oct 10 2024 at 03:41):

Ok looking at it so far Z3 now uses SMTLIB2.
isabelle already has some code ~~/src/HOL/Tools/SMT/smtlib for smtlib2 which is used for verit i think.

irvin (Oct 10 2024 at 03:48):

https://www.verit-solver.org/papers/pxtp2019.pdf
found another relevant paper

Mathias Fleury (Oct 10 2024 at 04:56):

The PhD thesis is probably a better start https://www21.in.tum.de/~boehmes/phd_thesis.pdf

Mathias Fleury (Oct 10 2024 at 05:04):

I have to do some digging if I still have the patch I used back then, but anyway the realistic path to do this is to add a z3_new and keep the old one:

add a Z3_NEW_SOLVER to the binary to the .isabelle/etc/settings file (compare it to $ isabelle env | grep Z3
add a z3_new system to ~/src/HOL/Tools/smt/smt_systems.ML (duplicate the z3 fields + duplicate the reconstruction function by creating a new file)
copy ~~/src/HOL/SMT_Examples/SMT_Examples.thy into ~~/src/HOL/SMT_Examples/SMT_Examples_Z3_New.thy, replace z3 by z3_new, remove the certificates stuff (comment out the two lines on top) and look at the examples that fail here

Mathias Fleury (Oct 10 2024 at 05:05):

Then you need to know the [[smt_trace]] flag to see what the reconstruction is doing

Mathias Fleury (Oct 10 2024 at 05:06):

and the obvious thing: if the lemma you have is only about quantifiers, bool, and int, you can copy it over to SMT.thy and change the reconstruction directly

Mathias Fleury (Oct 10 2024 at 05:06):

Do not forget to start Isabelle with Pure as base session (-l Pure)

Mathias Fleury (Oct 10 2024 at 05:10):

(PS: there are two people around who can answer questions on the reconstruction, @Hanna Lachnitt and me, so it might be a good idea to explicitly mention me when you have a question)

Fabian Huch (Oct 10 2024 at 08:07):

I have a request: the SMT method sometimes fails if there is high system load, e. g. here. While you're delving into SMT, could you check if this can be made more robust? I suspect that there's a timeout somewhere in the internals.

Mathias Fleury (Oct 10 2024 at 08:12):

That is another issue that has nothing to do with this (if there is a timeout you get a proper error)

Mathias Fleury (Oct 10 2024 at 08:12):

There is no timeout anymore (see the smt_timeout parameter)

Mathias Fleury (Oct 10 2024 at 08:14):

I think the issue is that Isabelle is spawning so many tasks that all the external threads (smt is running in a bash shell) is starved until another general timeout happens

Fabian Huch (Oct 10 2024 at 08:21):

Hmm I see

Mathias Fleury (Oct 10 2024 at 08:22):

I believe that this issue is somehow linked to the windows issue of stuff not being killed

Mathias Fleury (Oct 10 2024 at 08:24):

Internally smt and sledgehammer are relying on this in cache_io to run code:

fun raw_run make_cmd str in_path out_path =
  let
    val _ = File.write in_path str
    val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
    val out1 = try_read_lines out_path
  in {output = split_lines out2, redirected_output = out1, return_code = rc} end

and this:

fun with_time_limit ctxt timeout_config f x =
  Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
    handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out

to limit the amount of time

Fabian Huch (Oct 10 2024 at 08:25):

So the culprit would be Isabelle_System.bash_output

Mathias Fleury (Oct 10 2024 at 08:25):

That is my guess, but I have no clue how to check that

Fabian Huch (Oct 10 2024 at 08:25):

We also get some spurious nitpick errors:

Unexpected outcome: "unknown"
***                              At command "nitpick"

which might be for the same reason

Mathias Fleury (Oct 10 2024 at 08:26):

basically yes, but here there is a timeout

Mathias Fleury (Oct 10 2024 at 08:26):

hence the unknown answer

Fabian Huch (Oct 10 2024 at 08:29):

Oh you're right, that seems like a weird implementation of nitpick

Mathias Fleury (Oct 10 2024 at 08:32):

It is more complicated than that I think: during development it totally makes sense to have such a timeout. Also these problems only appear on big servers or slow machines (I tried to run Isabelle on raspberry pi)

Fabian Huch (Oct 10 2024 at 08:32):

Well also under heavy load on normal machines

Mathias Fleury (Oct 10 2024 at 08:36):

I remember the time before I could run -j 8 on my office machine (not enough RAM) and back then that was not an issue

Mathias Fleury (Oct 10 2024 at 08:37):

but you are right that this should be fixed somehow

Fabian Huch (Oct 10 2024 at 08:38):

It was not an issue before because the build strategy was too inefficient

Mathias Fleury (Oct 10 2024 at 08:43):

Fabian Huch said:

So the culprit would be Isabelle_System.bash_output

But somehow trying to understand the behavior sounds like a bachelor project (at least understanding the behavior)

Mathias Fleury (Oct 10 2024 at 08:44):

do you have bachelor students around?

Fabian Huch (Oct 10 2024 at 08:46):

I don't think code archeology is a good thesis project...

Mathias Fleury (Oct 10 2024 at 08:48):

Not for a thesis. But as a more practical project (so trying to understand the behavior and the order in which the jobs are done)

Fabian Huch (Oct 10 2024 at 08:49):

Sadly I don't really have students for that

irvin (Oct 11 2024 at 13:04):

Mathias Fleury said:

I have to do some digging if I still have the patch I used back then, but anyway the realistic path to do this is to add a z3_new and keep the old one:

add a Z3_NEW_SOLVER to the binary to the .isabelle/etc/settings file (compare it to $ isabelle env | grep Z3

add a z3_new system to ~/src/HOL/Tools/smt/smt_systems.ML (duplicate the z3 fields + duplicate the reconstruction function by creating a new file)

copy ~~/src/HOL/SMT_Examples/SMT_Examples.thy into ~~/src/HOL/SMT_Examples/SMT_Examples_Z3_New.thy, replace z3 by z3_new, remove the certificates stuff (comment out the two lines on top) and look at the examples that fail here

Manage to finally get started. And found the issue specifically its from calling

lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by (smt (z3_new )) which leads to this issue https://github.com/Z3Prover/z3/issues/5073

irvin (Oct 11 2024 at 13:15):

Im planning to ignore that issue first try to get proof-bind to work. Can even revert back to an older commit where its fixed

Mathias Fleury (Oct 11 2024 at 13:18):

I checked it as far as to find a release where that was working

Mathias Fleury (Oct 11 2024 at 13:18):

(it is written somewhere on Makarius' bug tracker)

Mathias Fleury (Oct 11 2024 at 13:20):

Or not https://isabelle-dev.sketis.net/T29, I must be misremembering

Mathias Fleury (Oct 11 2024 at 13:20):

but there was one release where this was working

irvin (Oct 11 2024 at 13:27):

Mathias Fleury said:

I checked it as far as to find a release where that was working

You wrote it in the issue itself https://github.com/Z3Prover/z3/issues/5073#issuecomment-1273517432

irvin (Oct 11 2024 at 13:36):

I noticed you mention https://publikationen.bibliothek.kit.edu/1000131835 as papers using z3 with proof reconstruction as one of the latest do you have a list of papers which have z3 reconstruction

irvin (Oct 11 2024 at 13:38):

search engine does not seem to really show any except the isabelle one

Mathias Fleury (Oct 11 2024 at 13:46):

There is the Isabelle one by Sascha, the HOL4 one by Tjark (https://www21.in.tum.de/~boehmes/fast_proof_rec/fast_proof_rec.pdf) -- they both wrote it up together --, and the Key one you found

Mathias Fleury (Oct 11 2024 at 13:48):

I had a patch to support proof-bind (it was not hard, I think ignoring it was possible)

Mathias Fleury (Oct 11 2024 at 13:48):

but I cannot find it anymore

Mathias Fleury (Oct 11 2024 at 13:48):

The main issue is finding out what it does, because I never found any documentation on that

Mathias Fleury (Oct 11 2024 at 13:52):

irvin said:

Im planning to ignore that issue first try to get proof-bind to work. Can even revert back to an older commit where its fixed

that is a good plan. Better finding out how much is broken before trying to fix the bug on the reconstruction side

Mathias Fleury (Oct 11 2024 at 13:58):

(I mostly stopped at that point because I run out of free work cycles while waiting for Z3 answers)

irvin (Oct 11 2024 at 14:26):

Mathias Fleury said:

The main issue is finding out what it does, because I never found any documentation on that

Seems to be the commit where proof-bind was added https://github.com/Z3Prover/z3/commit/520ce9a5ee6079651580b6d83bc2db0f342b8a20

Mathias Fleury (Oct 11 2024 at 14:40):

So it is the equivalent of the Isar block

{
fix x
  ...proof..
} (*exported last fact here*)

Mathias Fleury (Oct 11 2024 at 14:45):

This is not hard to represent in Isabelle (you declare the new variables in the context and export the fact at the end):

(*creating a sub_ctxt where the new variable skolem_name is declared*)
val ([name], sub_ctxt) = Variable.variant_fixes [skolem_name] ctxt
       ||> Variable.declare_term (Free (skolem_name, fastype_of declaration))
    val old_names = (Free (skolem_name, fastype_of declaration))
    val new_names = (Free (name, fastype_of declaration))
(*now export it*)
val export_thm = Proof_Context.export sub_ctxt ctxt theorem to export

Mathias Fleury (Oct 11 2024 at 14:46):

IIRC purely ignoring the rule does work because the format of z3 is not very precise anyway.

Mathias Fleury (Oct 11 2024 at 14:47):

But it would be better to change that to properly support that, but this is a lot of work and context manipulation is tough (because of the very weird bugs it generates)

Mathias Fleury (Oct 11 2024 at 14:48):

(if you look at the veriT proof, you will see that the used datastructure is recursive exactly to handle these context manipulation properly)

irvin (Oct 12 2024 at 10:19):

Mathias Fleury said:

This is not hard to represent in Isabelle (you declare the new variables in the context and export the fact at the end):

(*creating a sub_ctxt where the new variable skolem_name is declared*)
val ([name], sub_ctxt) = Variable.variant_fixes [skolem_name] ctxt
       ||> Variable.declare_term (Free (skolem_name, fastype_of declaration))
    val old_names = (Free (skolem_name, fastype_of declaration))
    val new_names = (Free (name, fastype_of declaration))
(*now export it*)
val export_thm = Proof_Context.export sub_ctxt ctxt theorem to export

thanks for the help.

irvin (Oct 12 2024 at 10:22):

Mathias Fleury said:

IIRC purely ignoring the rule does work because the format of z3 is not very precise anyway.

Seems to be this bit

text ‹
Several prof rules of Z3 are not very well documented. There are two
lemma groups which can turn failing Z3 proof reconstruction attempts
into succeeding ones: the facts in ‹z3_rule› are tried prior to
any implemented reconstruction procedure for all uncertain Z3 proof
rules;  the facts in ‹z3_simp› are only fed to invocations of
the simplifier when reconstructing theory-specific proof steps.
›

irvin (Oct 12 2024 at 10:26):

Right now im directly modifying the z3 proof reconstruction code instead of copying. Hope that it would work for both versions.

irvin (Oct 12 2024 at 15:51):

Do any of the other smt provers use smtlib_proof.ML because according to https://smt-lib.org/papers/smt-lib-reference-v2.6-r2024-09-20.pdf#Hendnote.50 there is no standard smt-lib proof format

irvin (Oct 12 2024 at 16:03):

irvin said:

Do any of the other smt provers use smtlib_proof.ML because according to https://smt-lib.org/papers/smt-lib-reference-v2.6-r2024-09-20.pdf#Hendnote.50 there is no standard smt-lib proof format

grep -r "SMTLIB_Proof"
src/HOL/Tools/SMT/lethe_proof.ML: val parse_raw_proof_steps: string option -> SMTLIB.tree list -> SMTLIB_Proof.name_bindings -> int ->
src/HOL/Tools/SMT/lethe_proof.ML: raw_lethe_node list * SMTLIB.tree list * SMTLIB_Proof.name_bindings
src/HOL/Tools/SMT/lethe_proof.ML:open SMTLIB_Proof
src/HOL/Tools/SMT/lethe_proof.ML: let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx
src/HOL/Tools/SMT/lethe_proof.ML: |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id))
src/HOL/Tools/SMT/lethe_proof.ML: let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l) cx
src/HOL/Tools/SMT/lethe_proof.ML: let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) def cx
src/HOL/Tools/SMT/lethe_proof.ML: let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx
src/HOL/Tools/SMT/lethe_proof.ML: let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx
src/HOL/Tools/SMT/lethe_proof.ML: val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx
src/HOL/Tools/SMT/lethe_proof.ML: val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings term cx
src/HOL/Tools/SMT/lethe_proof.ML: fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso
src/HOL/Tools/SMT/lethe_proof.ML: parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding 0
src/HOL/Tools/SMT/z3_proof.ML:open SMTLIB_Proof
src/HOL/Tools/SMT/smtlib_proof.ML:structure SMTLIB_Proof: SMTLIB_PROOF =
src/HOL/Tools/SMT/smt_real.ML: SMTLIB_Proof.add_type_parser real_type_parser #>
src/HOL/Tools/SMT/smt_real.ML: SMTLIB_Proof.add_term_parser real_term_parser #>
src/HOL/Tools/SMT/verit_strategies.ML:open SMTLIB_Proof
src/HOL/Tools/SMT/z3_proof.ML~:open SMTLIB_Proof
Oh looks like it being used

Mathias Fleury (Oct 12 2024 at 16:06):

Even if there is no smt-lib proof format, all proof formats use the SMT-Lib syntax for terms

Mathias Fleury (Oct 12 2024 at 16:07):

hence it is used by veriT (Lethe) and Z3

irvin (Oct 12 2024 at 18:48):

Z3 seems to support lambdas expressions. Specifically that seems to be what this commit seems to add.

irvin said:

Mathias Fleury said:

The main issue is finding out what it does, because I never found any documentation on that

Seems to be the commit where proof-bind was added https://github.com/Z3Prover/z3/commit/520ce9a5ee6079651580b6d83bc2db0f342b8a20

Z3 also seems to support algebraic datatypes (part of SMT lib i think) part of the match stuff.

Right now smt has infrastructure so that lambdas are converted. When doing translations from HOL to MSFOL. Should I try to remove that.

Lambdas are not part of MSFOL so I probably will do code duplication and write a second function for z3
Cant really figure out this bit but not really a issue just a bad error msg
Second right now will have to be reworked for z3. lambda is not part SMT-LIB. However this function gave a weird error message when its executed with SMTLIB.S [SMTLIB.Sym "lambda",...] which it then tries to parse term and succeeds but then another later call fail lookup_binding cx lambda failed and then it called parse_term t which then it incorrect and you get the error bad SMT term which does not make sense. Do you know anyway to future proof against this sort of errors

fun term_of t cx =
  (case t of
    SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx
  | SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx
  | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx
  | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] =>
      with_bindings (map dest_binding bindings) (term_of body) cx
  | SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx
  | SMTLIB.S (f :: args) =>
      cx
      |> fold_map term_of args
      |-> parse_term f
  | SMTLIB.Sym name =>
      (case lookup_binding cx name of
        Tree u =>
          cx
          |> term_of u
          |-> (fn u' => pair u' o update_binding (name, Term u'))
      | Term u => (u, cx)
      | None => parse_term t [] cx
      | _ => raise SMTLIB_PARSE ("bad SMT term format", t))
  | _ => parse_term t [] cx)

irvin (Oct 12 2024 at 19:00):

~~I think i figured out the second one~~ or maybe not

irvin (Oct 12 2024 at 19:07):

image.png

Mathias Fleury (Oct 12 2024 at 19:31):

irvin said:

Z3 seems to support lambdas expressions. Specifically that seems to be what this commit seems to add.

That does not mean that it must be a lambda in Isabelle. fix variable are usually not written as lambdas in Isabelle

irvin (Oct 14 2024 at 07:36):

irvin said:

~~I think i figured out the second one~~ or maybe not

While trying to figure the parser errors. I realized that the current parser does not do let binding scope correctly.
The parser goes through parse generating a binding => unparsed binding context
The term is not parsed as more information is needed to known whether it is a binding to term or proofterm (this is for z3 not sure whether other proof formats it is clear)
On the first instance when the binding is encountered. (Now clear whether it is a term or proofterm).
Its parsed and updated. With the binding of the first encounter of the new context.

irvin (Oct 14 2024 at 07:45):

Also repeated lets wont work
ie.
let a = foo in
let b = something with a
let a = bar in
...

irvin (Oct 14 2024 at 07:49):

So im going to rewrite the parser

Mathias Fleury (Oct 14 2024 at 07:50):

Doesn't z3 generate a new name for each binding?

irvin (Oct 14 2024 at 07:52):

Yup it does so this is really just being more defensive. Against inputs. Current version can run forever on some inputs

irvin (Oct 14 2024 at 07:53):

Also is there any method of execption combinators

Mathias Fleury (Oct 14 2024 at 07:54):

irvin said:

Yup it does so this is really just being more defensive. Against inputs

You can safely assume that you will get inputs from z3 only, so being defensive is not really necessary

Mathias Fleury (Oct 14 2024 at 07:55):

(and there will never be another solver that uses that proof format)

Mathias Fleury (Oct 14 2024 at 07:56):

irvin said:

Also is there any method of execption combinators

No, the first error can just itnerrupt the execution

irvin (Oct 14 2024 at 07:59):

Mathias Fleury said:

(and there will never be another solver that uses that proof format)

This affects the generic smtlib terms also

Mathias Fleury (Oct 14 2024 at 08:03):

irvin said:

So im going to rewrite the parser

Anyone rewriting that scares me a lot

irvin (Oct 14 2024 at 08:03):

Mathias Fleury said:

irvin said:

So im going to rewrite the parser

Anyone rewriting that scares me a lot

Mathias Fleury (Oct 14 2024 at 08:03):

I know that it is tempting to make it better

Mathias Fleury (Oct 14 2024 at 08:04):

but working stuff that is not buggy is always better

Mathias Fleury (Oct 14 2024 at 08:04):

So unless you find a bug, I would not rewrite the smtlib parser (the z3 parser is fine)

irvin (Oct 14 2024 at 08:23):

For documentation purposes. This is the affected function. A simple fix would probably be to make let call update.

fun term_of t cx =
  (case t of
    SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx
  | SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx
  | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx
  | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] =>
      with_bindings (map dest_binding bindings) (term_of body) cx
  | SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx
  | SMTLIB.S (f :: args) =>
      cx
      |> fold_map term_of args
      |-> parse_term f
  | SMTLIB.Sym name =>
      (case lookup_binding cx name of
        Tree u =>
          cx
          |> term_of u
          |-> (fn u' => pair u' o update_binding (name, Term u'))
      | Term u => (u, cx)
      | None => parse_term t [] cx
      | _ => raise SMTLIB_PARSE ("bad SMT term format", t))
  | _ => parse_term t [] cx)

and quant q vars body cx =
  let val vs = map (dest_var cx) vars
  in
    cx
    |> with_bindings (map (apsnd (Term o Free)) vs) (term_of (dest_body body))
    |>> fold_rev (fn (_, (n, T)) => fn t => q (n, T, t)) vs
  end

irvin (Oct 14 2024 at 08:24):

Is comments to zulip links considered bad?

Fabian Huch (Oct 14 2024 at 08:48):

You mean in the source code? Certainly.

Mathias Fleury (Oct 14 2024 at 09:19):

Adding a pattern to term_of is fine

Mathias Fleury (Oct 14 2024 at 09:21):

but isn't with ẁith_bindings`already doing an update?

irvin (Oct 14 2024 at 09:27):

Mathias Fleury said:

but isn't with ẁith_bindings`already doing an update?

Oh my bad seems to ok then.

Mathias Fleury (Oct 14 2024 at 09:34):

At least the code looks like it:

fun with_bindings bs f cx =
  let val bs' = map (lookup_binding cx o fst) bs
  in
    cx
    |> fold update_binding bs
    |> f
    ||> fold2 (fn (name, _) => update_binding o pair name) bs bs'
  end

(and this is one of the cases were always updating is the easiest solution)

irvin (Oct 14 2024 at 10:03):

Mathias Fleury said:

At least the code looks like it:

fun with_bindings bs f cx =
  let val bs' = map (lookup_binding cx o fst) bs
  in
    cx
    |> fold update_binding bs
    |> f
    ||> fold2 (fn (name, _) => update_binding o pair name) bs bs'
  end

(and this is one of the cases were always updating is the easiest solution)

It doesnt it simply registers unparsed tree in the symtab

irvin (Oct 14 2024 at 10:04):

with_bindings (map dest_binding bindings) (term_of body) cx term_of is not passed into with_bindings at all so it cant have a chance to parse it

irvin (Oct 14 2024 at 11:08):

Explanation of the code.
bindings are destructored using map dest_binding bindings
with_binding call
current binding is saved in the
val bs' = map (lookup cx o fst) bs
update the binding the unparsed values of (map dest_binding bindings)
call the (term_of body with the context updated.
reset back the bindings. to the thing so let scoping works. for the case of
let a = ... in (let a in ...) (Which i was wrong)
However weird recursion let work
something like
let a = b in (let b = a)
Modifing with_binding

fun with_bindings bs f cx =
  let val bs' = map (lookup_binding cx o fst) bs
         val cx2 = fold update_binding bs cx
         val _ = writeln (@{make_string} (map (lookup_binding cx2 o fst) bs))

  in
    cx
    |> fold update_binding bs
    |> f
    ||> fold2 (fn (name, _) => update_binding o pair name) bs bs'
  end

Everything printed is of Tree (not yet parsed)
datatype 'b shared = Tree of SMTLIB.tree | Term of term | Proof of 'b | None

irvin (Oct 14 2024 at 11:10):

Side note I dont seem to see verit make use of let at all is this true

irvin (Oct 14 2024 at 12:51):

Also do you know anyway of creating a type ('a, 'b) context for testing

Mathias Fleury (Oct 14 2024 at 13:08):

empty_context

Mathias Fleury (Oct 14 2024 at 13:09):

irvin said:

Explanation of the code.
bindings are destructored using map dest_binding bindings
with_binding call
current binding is saved in the
val bs' = map (lookup cx o fst) bs
update the binding the unparsed values of (map dest_binding bindings)
call the (term_of body with the context updated.
reset back the bindings. to the thing so let scoping works. for the case of
let a = ... in (let a in ...) (Which i was wrong)
However weird recursion let work
something like
let a = b in (let b = a)
Modifing with_binding
fun with_bindings bs f cx =
  let val bs' = map (lookup_binding cx o fst) bs
         val cx2 = fold update_binding bs cx
         val _ = writeln (@{make_string} (map (lookup_binding cx2 o fst) bs))

  in
    cx
    |> fold update_binding bs
    |> f
    ||> fold2 (fn (name, _) => update_binding o pair name) bs bs'
  end
Everything printed is of Tree (not yet parsed)
datatype 'b shared = Tree of SMTLIB.tree | Term of term | Proof of 'b | None

The question is how to represent the end of a scope

Mathias Fleury (Oct 14 2024 at 13:10):

~~For verit we "open" a new context and can close is outside of a subproof)~~
I have to think about your text again

Mathias Fleury (Oct 14 2024 at 15:29):

You just duplicate context until you reach the end of a context

let a = b in (let b = a in a)    +   b
ctxt-----------------------x
           \----------------------->

irvin (Oct 14 2024 at 16:01):

Mathias Fleury said:

Doesn't z3 generate a new name for each binding?

I just checked again and z3 doesnt generate a new name for each binding

irvin (Oct 14 2024 at 16:57):

Ok finally got the z3 proofs to be parsed

irvin (Oct 15 2024 at 01:26):

image.png

irvin (Oct 15 2024 at 02:08):

So from what i understand. The proof-bind is not really a "proof method" and is handled at the parser level. Currently the implementation automatically does the free variables. So ignoring it is possible.

irvin (Oct 15 2024 at 02:13):

Mathias Fleury said:

irvin said:

Z3 seems to support lambdas expressions. Specifically that seems to be what this commit seems to add.

That does not mean that it must be a lambda in Isabelle. fix variable are usually not written as lambdas in Isabelle

In this case is it just !!a. P a

irvin (Oct 17 2024 at 02:38):

The current situation is the z3 rule rewrite failing. rewrite a rewrite which does not provide justification and according to z3 proof reconstruction should use internal decision provers to reconstruct the rewrite rule

irvin (Oct 17 2024 at 03:09):

Also does anyone know if there is any tooling to make isabelle build expose warning/ errors similar to how a compiler exposes the errors when compiling
Source of the issue is that the SMT_Examples_*.thy requires Complex_Main which results in every single edit requiring the whole state below to be parsed. Im guessing that it will be extremely hard to make isabelle graph based and only reloading the nodes affected below.
If there isnt where would i look to make a component to make it do this.

Mathias Fleury (Oct 17 2024 at 04:57):

It is not that bad actually in practise

Mathias Fleury (Oct 17 2024 at 04:58):

there are two ways to make it less horrible:

1. replace the import by HOL.SMT. Will not work for everything (mostly the first part of the file will work, but for debugging that is usually enough)

Mathias Fleury (Oct 17 2024 at 04:59):

you can also remove SMT and Sledgehammer and nitpick by replacing the point where there are imported by their own imports. Then you only import SMT in the example file. Just sorry the stuff that does not work

Mathias Fleury (Oct 17 2024 at 05:32):

make isabelle graph based and only reloading the nodes affected below[...] If there isnt where would i look to make a component to make it do this.

I am pretty sure that this is part of the "you do not want to do that because an error here can make Isabelle incorrect so no sane person would want to use that". Also the SMT method is used in List.thy anyway

Mathias Fleury (Oct 17 2024 at 05:35):

Also does anyone know if there is any tooling to make isabelle build expose warning/ errors similar to how a compiler exposes the errors when compiling

Usually I have SMT.thy open at the point of the SML import files and the ML files I am editing, then you see in the output panel all the error messages

irvin (Oct 17 2024 at 05:36):

Yup the graph based version is not something i would try to do. However im asking on the feasibility of making isabelle build output warning and errors

Mathias Fleury (Oct 17 2024 at 05:39):

image.png
here you can see the error message at the bottom. In the right theory you can see the follow-up places where there are errors

Mathias Fleury (Oct 17 2024 at 05:40):

This is much better than the alternative with isabelle build which stops at the first error

Mathias Fleury (Oct 17 2024 at 05:42):

$ ./bin/isabelle build -b HOL
Building HOL ...
HOL FAILED (see also "isabelle build_log -H Error HOL")
...
*** Failed to load theory "HOL.String" (unresolved "HOL.Bit_Operations", "HOL.Code_Numeral", "HOL.Enum")
*** Failed to load theory "HOL.BNF_Greatest_Fixpoint" (unresolved "HOL.String")
*** Failed to load theory "HOL.Predicate" (unresolved "HOL.String")
*** Failed to load theory "HOL.Typerep" (unresolved "HOL.String")
*** Failed to load theory "HOL.Random" (unresolved "HOL.Code_Numeral", "HOL.Groups_List", "HOL.List")
*** Failed to load theory "HOL.Lazy_Sequence" (unresolved "HOL.Predicate")
*** Failed to load theory "HOL.Limited_Sequence" (unresolved "HOL.Lazy_Sequence")
*** Failed to load theory "HOL.Code_Evaluation" (unresolved "HOL.Limited_Sequence", "HOL.Typerep")
*** Failed to load theory "HOL.Quickcheck_Random" (unresolved "HOL.Code_Evaluation", "HOL.Enum", "HOL.Random")
*** Failed to load theory "HOL.Quickcheck_Exhaustive" (unresolved "HOL.Quickcheck_Random")
*** Failed to load theory "HOL.Record" (unresolved "HOL.Quickcheck_Exhaustive")
*** Failed to load theory "HOL.Nitpick" (unresolved "HOL.GCD", "HOL.Record")
*** Failed to load theory "HOL.Nunchaku" (unresolved "HOL.Nitpick")
*** Failed to load theory "HOL.Quickcheck_Narrowing" (unresolved "HOL.Quickcheck_Random")
*** Failed to load theory "HOL.Random_Pred" (unresolved "HOL.Quickcheck_Random")
*** Failed to load theory "HOL.Random_Sequence" (unresolved "HOL.Random_Pred")
*** Failed to load theory "HOL.Predicate_Compile" (unresolved "HOL.Quickcheck_Exhaustive", "HOL.Random_Sequence")
*** Failed to load theory "HOL.Mirabelle" (unresolved "HOL.Predicate_Compile", "HOL.Sledgehammer")
*** Failed to load theory "Main" (unresolved "HOL.BNF_Greatest_Fixpoint", "HOL.Binomial", "HOL.GCD", "HOL.Mirabelle", "HOL.Nunchaku", "HOL.Predicate_Compile", "HOL.Quickcheck_Narrowing")
*** Failed to load theory "HOL.Archimedean_Field" (unresolved "Main")
*** Failed to load theory "HOL.Rat" (unresolved "HOL.Archimedean_Field")
*** Failed to load theory "HOL.Real" (unresolved "HOL.Rat")
*** Failed to load theory "HOL.Hull" (unresolved "Main")
*** Failed to load theory "HOL.Modules" (unresolved "HOL.Hull")
*** Failed to load theory "HOL.Vector_Spaces" (unresolved "HOL.Modules")
*** Failed to load theory "HOL.Topological_Spaces" (unresolved "Main")
*** Failed to load theory "HOL.Real_Vector_Spaces" (unresolved "HOL.Real", "HOL.Topological_Spaces", "HOL.Vector_Spaces")
*** Failed to load theory "HOL.Inequalities" (unresolved "HOL.Real_Vector_Spaces")
*** Failed to load theory "HOL.Limits" (unresolved "HOL.Real_Vector_Spaces")
*** Failed to load theory "HOL.Deriv" (unresolved "HOL.Limits")
*** Failed to load theory "HOL.NthRoot" (unresolved "HOL.Deriv")
*** Failed to load theory "HOL.Series" (unresolved "HOL.Inequalities", "HOL.Limits")
*** Failed to load theory "HOL.Transcendental" (unresolved "HOL.Deriv", "HOL.NthRoot", "HOL.Series")
*** Failed to load theory "HOL.Complex" (unresolved "HOL.Real_Vector_Spaces", "HOL.Transcendental")
*** Failed to load theory "HOL.MacLaurin" (unresolved "HOL.Transcendental")
*** Failed to load theory "Complex_Main" (unresolved "HOL.Complex", "HOL.MacLaurin")
*** ML error (line 129 of "~~/src/HOL/Tools/SMT/alethe/alethe_proof.ML"):
*** Expression expected but | was found
***
*** At command "ML_file" (line 688 of "~~/src/HOL/SMT.thy")
Unfinished session(s): HOL
0:00:49 elapsed time, 0:02:22 cpu time, factor 2.85

Mathias Fleury (Oct 17 2024 at 05:42):

(this output is not edited)

Mathias Fleury (Oct 17 2024 at 05:44):

$ ./bin/isabelle build_log -H Error HOL

Theory "HOL.Sledgehammer" (in HOL): MISSING
[...] #here removed many MISSING
Theory "Complex_Main" (in HOL): MISSING

Build errors:
*** Failed to load theory "HOL.Sledgehammer" (unresolved "HOL.SMT")
*** Failed to load theory "HOL.List" (unresolved "HOL.Sledgehammer")
*** Failed to load theory "HOL.Groups_List" (unresolved "HOL.List")
*** Failed to load theory "HOL.Bit_Operations" (unresolved "HOL.Groups_List")
*** Failed to load theory "HOL.Code_Numeral" (unresolved "HOL.Bit_Operations")
*** Failed to load theory "HOL.Factorial" (unresolved "HOL.Groups_List")
*** Failed to load theory "HOL.Binomial" (unresolved "HOL.Factorial")
*** Failed to load theory "HOL.GCD" (unresolved "HOL.Code_Numeral", "HOL.Groups_List")
*** Failed to load theory "HOL.Map" (unresolved "HOL.List")
*** Failed to load theory "HOL.Enum" (unresolved "HOL.Groups_List", "HOL.Map")
*** Failed to load theory "HOL.String" (unresolved "HOL.Bit_Operations", "HOL.Code_Numeral", "HOL.Enum")
*** Failed to load theory "HOL.BNF_Greatest_Fixpoint" (unresolved "HOL.String")
*** Failed to load theory "HOL.Predicate" (unresolved "HOL.String")
*** Failed to load theory "HOL.Typerep" (unresolved "HOL.String")
*** Failed to load theory "HOL.Random" (unresolved "HOL.Code_Numeral", "HOL.Groups_List", "HOL.List")
*** Failed to load theory "HOL.Lazy_Sequence" (unresolved "HOL.Predicate")
*** Failed to load theory "HOL.Limited_Sequence" (unresolved "HOL.Lazy_Sequence")
*** Failed to load theory "HOL.Code_Evaluation" (unresolved "HOL.Limited_Sequence", "HOL.Typerep")
*** Failed to load theory "HOL.Quickcheck_Random" (unresolved "HOL.Code_Evaluation", "HOL.Enum", "HOL.Random")
*** Failed to load theory "HOL.Quickcheck_Exhaustive" (unresolved "HOL.Quickcheck_Random")
*** Failed to load theory "HOL.Record" (unresolved "HOL.Quickcheck_Exhaustive")
*** Failed to load theory "HOL.Nitpick" (unresolved "HOL.GCD", "HOL.Record")
*** Failed to load theory "HOL.Nunchaku" (unresolved "HOL.Nitpick")
*** Failed to load theory "HOL.Quickcheck_Narrowing" (unresolved "HOL.Quickcheck_Random")
*** Failed to load theory "HOL.Random_Pred" (unresolved "HOL.Quickcheck_Random")
*** Failed to load theory "HOL.Random_Sequence" (unresolved "HOL.Random_Pred")
*** Failed to load theory "HOL.Predicate_Compile" (unresolved "HOL.Quickcheck_Exhaustive", "HOL.Random_Sequence")
*** Failed to load theory "HOL.Mirabelle" (unresolved "HOL.Predicate_Compile", "HOL.Sledgehammer")
*** Failed to load theory "Main" (unresolved "HOL.BNF_Greatest_Fixpoint", "HOL.Binomial", "HOL.GCD", "HOL.Mirabelle", "HOL.Nunchaku", "HOL.Predicate_Compile", "HOL.Quickcheck_Narrowing")
*** Failed to load theory "HOL.Archimedean_Field" (unresolved "Main")
*** Failed to load theory "HOL.Rat" (unresolved "HOL.Archimedean_Field")
*** Failed to load theory "HOL.Real" (unresolved "HOL.Rat")
*** Failed to load theory "HOL.Hull" (unresolved "Main")
*** Failed to load theory "HOL.Modules" (unresolved "HOL.Hull")
*** Failed to load theory "HOL.Vector_Spaces" (unresolved "HOL.Modules")
*** Failed to load theory "HOL.Topological_Spaces" (unresolved "Main")
*** Failed to load theory "HOL.Real_Vector_Spaces" (unresolved "HOL.Real", "HOL.Topological_Spaces", "HOL.Vector_Spaces")
*** Failed to load theory "HOL.Inequalities" (unresolved "HOL.Real_Vector_Spaces")
*** Failed to load theory "HOL.Limits" (unresolved "HOL.Real_Vector_Spaces")
*** Failed to load theory "HOL.Deriv" (unresolved "HOL.Limits")
*** Failed to load theory "HOL.NthRoot" (unresolved "HOL.Deriv")
*** Failed to load theory "HOL.Series" (unresolved "HOL.Inequalities", "HOL.Limits")
*** Failed to load theory "HOL.Transcendental" (unresolved "HOL.Deriv", "HOL.NthRoot", "HOL.Series")
*** Failed to load theory "HOL.Complex" (unresolved "HOL.Real_Vector_Spaces", "HOL.Transcendental")
*** Failed to load theory "HOL.MacLaurin" (unresolved "HOL.Transcendental")
*** Failed to load theory "Complex_Main" (unresolved "HOL.Complex", "HOL.MacLaurin")
*** ML error (line 129 of "~~/src/HOL/Tools/SMT/alethe/alethe_proof.ML"):
*** Expression expected but | was found
***
*** At command "ML_file" (line 688 of "~~/src/HOL/SMT.thy")

Return code: 1 (ERROR)

irvin (Oct 17 2024 at 05:47):

Ok i guess i spend time looking at the code to see how to add warnings

Mathias Fleury (Oct 17 2024 at 07:14):

usually you want to add printing, not warnings

Mathias Fleury (Oct 17 2024 at 07:15):

@{print} allows you to print pretty-much anything

irvin (Oct 18 2024 at 04:38):

Mathias Fleury said:

@{print} allows you to print pretty-much anything

Oh thanks i was doing writeln @{make_string}.
Is there any conventions regarding whether to use @{lemma ... by ...} or doing the proof in isar then using @{thm ....}

Mathias Fleury (Oct 18 2024 at 04:46):

Not that I am aware of. My convention: if it already exists or is long I use @{thm}. Otherwise I use @{lemma}.

But: Put it in a constant instead of evaluating in a function, just to be sure that it is not reproven whenever you run the function. (Yes, Polyml probably is able to optimize but I do not trust that because I do not understand the quotations enough to be sure of that)

irvin (Oct 18 2024 at 05:06):

Oh its because i see that smt.thy has a lot of verit theories and i wondered whether I should do the same for the z3 theorems i prove and move them to the smt file

Mathias Fleury (Oct 18 2024 at 05:16):

Yeah just put it there too

irvin (Oct 18 2024 at 08:05):

Do you have any guide on understanding the abs_context code in smt_replay_method.

Mathias Fleury (Oct 19 2024 at 06:00):

It is used to abstract over the structure of a term if you know that the reconstruction is needing some details of the term

Mathias Fleury (Oct 19 2024 at 06:01):

for example, if you know that you are reconstructing an arithmetic step, then if-then-else constructs are seen as black box and thus you can abstract over it naming it with a fresh name (like x12 or whatever)

Mathias Fleury (Oct 19 2024 at 06:02):

this improves the performance of the reconstruction and make it more robust (like if you use auto, it will not get lost on some unrelated part of the term)

Mathias Fleury (Oct 19 2024 at 06:02):

I never had to change it, except when it turns out that the assumption over the abstraction is wrong

Mathias Fleury (Oct 19 2024 at 06:03):

(like arithmetic steps actually reason below if-then-else)

irvin (Oct 30 2024 at 04:17):

Mathias Fleury said:

I never had to change it, except when it turns out that the assumption over the abstraction is wrong

Is there a way to deal with the abstraction over comm assoc or
I have a proof rule which has to to destructive equality resolution
which is a rewrite of
lemma "∀a. ¬(a = c) ∨ P a = P c"
except for that its a or chain and ¬(a = c) may not be the first in the or

irvin (Oct 30 2024 at 04:18):

Btw sorry for not replying lately my linux system broke and I had to spend time troubleshooting it

Mathias Fleury (Oct 30 2024 at 05:56):

my intuition says that abstraction is too naive to do that

Mathias Fleury (Oct 30 2024 at 05:58):

It is not even clear to me how easy it would to reorder the chains to have them before

Mathias Fleury (Oct 30 2024 at 05:58):

(for Alethe we know it is ordered)

Mathias Fleury (Oct 30 2024 at 05:59):

I would do a simp only: as just rewriting is enough. And only if performance is too bad, I would spend more thinking into it

Mathias Fleury (Oct 30 2024 at 06:02):

Mathias Fleury said:

It is not even clear to me how easy it would to reorder the chains to have them before

actually it should be easy on the perfect shared term as P a must have a bigger term number than a, but there is a lot of work in the parsing to fix the ordering (or at least extract the P which would be enough).

irvin (Nov 03 2024 at 11:22):

Mathias Fleury said:

I would do a simp only: as just rewriting is enough. And only if performance is too bad, I would spend more thinking into it

For now apparently most of the time just running auto on the goals seems to solve them. But pretty sure its going have a performance impact.

irvin (Dec 07 2024 at 16:38):

@Mathias Fleury Btw an update. Apparent HOL4 decided to deal with the "bug" in z3 output and i think im going to try and do the same and deal with it rather than fix it on the z3 side. The rest works I think

Mathias Fleury (Dec 07 2024 at 16:39):

So they are sure that this is the only bug?

irvin (Dec 07 2024 at 16:44):

theses are apparently the relevant commits that the HOL4 maintainer sent me. I havent figured it out but they seem to be able to handle define-fun at the top of the proof block.
https://github.com/HOL-Theorem-Prover/HOL/commit/8f8bd67b8c5a3d799144a14206aa8d4266edd36b
https://github.com/HOL-Theorem-Prover/HOL/commit/def62b7000cb313b19c84cabe8c1867e63a9c624 https://github.com/HOL-Theorem-Prover/HOL/commit/4324a79a32b7cccf11efbef4ecee637784ad28c4 https://github.com/HOL-Theorem-Prover/HOL/commit/313365a0e83c847c9767d67ab52b2f69135dcaba https://github.com/HOL-Theorem-Prover/HOL/commit/4b763209b040de35cf9d408e76a9c4898ce848d5 https://github.com/HOL-Theorem-Prover/HOL/commit/120e7bb43bc3ffcca4efb2cafbeed0605d620bff https://github.com/HOL-Theorem-Prover/HOL/commit/525694a1f1c7016dea954894bea6e6e396f7d6b3

Mathias Fleury (Dec 07 2024 at 16:46):

Ahh thanks for the links!

irvin (Dec 07 2024 at 16:48):

I guess it might be easier as they can be made schematic variables in isabelle?

Mathias Fleury (Dec 07 2024 at 16:50):

I always tried to avoid those in the reconstruction.

Mathias Fleury (Dec 07 2024 at 16:52):

Also a lot of the reconstruction is actively avoiding them too (by fixing them prior to proving anything). This also avoids accidentally instantiating them.

Last updated: Dec 21 2024 at 16:20 UTC