Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bug report Isabelle 2019 and Isabelle 2020


view this post on Zulip Email Gateway (Nov 21 2020 at 05:56):

From: Peter Reitinger <peter.reitinger@gmail.com>
Hi,

sorry for recently reporting just confusing behavior because of
polymorphism as a bug.

But this time, I am very sure to have observed a bug, if creation of a
memory dump characterizes a bug. ;-)

First the screenshot:

[image: image.png]

The theory reproducing this bug is attached. The try at the end of the
experimental proof (sorry about the mess there, I am still experimenting
with Word & Co theories) produces the error.

Best regards
Peter Reitinger
image.png
Show_bug2.thy

view this post on Zulip Email Gateway (Nov 21 2020 at 12:03):

From: Makarius <makarius@sketis.net>
On 21/11/2020 06:56, Peter Reitinger wrote:

sorry for recently reporting just confusing behavior because of
polymorphism as a bug.

But this time, I am very sure to have observed a bug, if creation of a memory
dump characterizes a bug. ;-)

The "bug" terminology does not make much sense beyond a certain complexity of
systems (or rather a multi-system compound like the Isabelle ecosystem). You
do have a large space that is "inhabitable", but you also have uncharted areas
where things don't work.

First the screenshot:

image.png

I recommend to copy paste actual source text and output, unless this is a
problem of GUI rendering or interaction.

The relevant part of the error is this:

/home/makarius/lib/Isabelle2020/contrib/z3-4.4.0pre-3/x86_64-linux/z3
smt.random_seed\=1 smt.refine_inj_axioms\=false -T:10 -smt2
/tmp/isabelle-makarius/process1270985018603270244/cache-io-3287480 >
/tmp/isabelle-makarius/process1270985018603270244/cache-io-3287482 2>&1

So this is a hard crash of the (rather old) version of z3 that we are using.

There have been other z3 inconveniences before, but I guess we can't upgrade
it easily.

Maybe an expert on the Isabelle/z3 can say more about the situation.

Makarius

view this post on Zulip Email Gateway (Nov 23 2020 at 03:23):

From: Peter Reitinger <peter.reitinger@gmail.com>
Hi again,

maybe this helps...

Here I could produce a crash in "cvc4" with modified Word_Examples:

theory Word_Examples
imports Word_Bitwise
begin
(* commented previous lemmas out *)
lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
(* BEGIN preitinger *)
declare [[show_sorts]]
lemma "takefill False (size (1::6 word) - (3::nat)) (to_bl (1::6 word)) =
[False, False, False]"
apply sledgehammer

Sledgehammering...
/tmp/isabelle-peter/process3745657003709610034/bash_script3287864: Zeile 1:
6505 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux/cvc4
--full-saturate-quant --inst-when\=full-last-call --inst-no-entail
--term-db-mode\=relevant --multi-trigger-linear --no-statistics
--random-seed\=1 --lang\=smt2 --continued-execution --tlimit 9990
/tmp/isabelle-peter/process3745657003709610034/cache-io-3287858 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3287860 2>&1
/tmp/isabelle-peter/process3745657003709610034/bash_script3292002: Zeile 1:
6520 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux/cvc4
--full-saturate-quant --inst-when\=full-last-call --inst-no-entail
--term-db-mode\=relevant --multi-trigger-linear --no-statistics
--random-seed\=1 --lang\=smt2 --continued-execution --tlimit 9845
/tmp/isabelle-peter/process3745657003709610034/cache-io-3291998 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3292000 2>&1
/tmp/isabelle-peter/process3745657003709610034/bash_script3298144: Zeile 1:
6618 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux/cvc4
--full-saturate-quant --inst-when\=full-last-call --inst-no-entail
--term-db-mode\=relevant --multi-trigger-linear --no-statistics
--random-seed\=1 --lang\=smt2 --continued-execution --tlimit 3923
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298140 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298142 2>&1
/tmp/isabelle-peter/process3745657003709610034/bash_script3298666: Zeile 1:
6626 Abgebrochen (Speicherabzug geschrieben)
/home/peter/isabelle/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux/cvc4
--full-saturate-quant --inst-when\=full-last-call --inst-no-entail
--term-db-mode\=relevant --multi-trigger-linear --no-statistics
--random-seed\=1 --lang\=smt2 --continued-execution --tlimit 3827
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298662 >
/tmp/isabelle-peter/process3745657003709610034/cache-io-3298664 2>&1
"e": Timed out
"cvc4": The prover crashed
"z3": Timed out
"vampire": Timed out

view this post on Zulip Email Gateway (Nov 23 2020 at 07:49):

From: Manuel Eberl <eberlm@in.tum.de>
Just a hunch, did you get your Isabelle distribtion from the official
website or from a package repository (e.g. installed using apt, pacman,
etc.)?

Manuel

view this post on Zulip Email Gateway (Nov 23 2020 at 08:15):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

I had a look and the problems comes from the generated SMT file. CVC4
does not accept a type annotation in the generated problem (and returns
a nice error message), while Z3 accepts it.

I don't know enough about the SMT-lib format to know who is right, but I
have asked experts to see which solver is wrong.

Thanks for reporting,

Mathias

view this post on Zulip Email Gateway (Nov 23 2020 at 10:13):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

Some explanation on the bug. The SMT-Lib format makes it possible to
write (_ bv4 9) to mean 4 :: 9 word. However, if the word does not fit,
like for 3 :: 1 word, it is not clear what this means.

If the solver accepts it, it has to discard the leftover bits
(truncating the number). But the SMT-Lib format is not explicit about
that and CVC4 rejects the problem file.

The solution is to generate 1:: 1 word (corresponding to _bv1 1) instead
of 3 :: 1 word (corresponding to _bv3 1).

I am currently testing a fix for that.

Mathias

view this post on Zulip Email Gateway (Dec 16 2020 at 08:53):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

the problem is now fixed
(https://isabelle-dev.sketis.net/rISABELLEf9424ceea3c33538bd3e52a12d9f8225c8256738).

Best,

Mathias

view this post on Zulip Email Gateway (Jan 02 2021 at 10:40):

From: Makarius <makarius@sketis.net>
Can you try this again with current Isabelle2021-RC1
https://isabelle.in.tum.de/website-Isabelle2021-RC1 ?

It will require to change the Word setup: the NEWS file contains some hints
about that.

Makarius

view this post on Zulip Email Gateway (Jan 24 2021 at 19:29):

From: Makarius <makarius@sketis.net>
Did you try anything in the meantime?

We already have https://isabelle.sketis.net/website-Isabelle2021-RC3 and
approx. 3 weeks left until everything becomes final and unchangeable.
(Isabelle releases don't have "patch-levels" after the deadline.)

Makarius


Last updated: Dec 05 2021 at 23:19 UTC