Re: [isabelle] Error Building HOL-Word



Hello Mario.

It looks like z3 isn't working in your environment. There's a copy of z3 bundled with isabelle, which is meant to work on any given platform, but a colleague of mine has had it terminate like that when running on his Windows machine.

There was a patch we recommended a while back which replaces the two uses of "smt" in the standard Isabelle theories with other proof methods. I think that patch has now been accepted, but you might be using a version where you don't have it yet. You can probably hand apply it.

OK, found it. There was a discussion here in December, which you can see on the web here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-December/msg00004.html

You could hand-edit the two theories I quoted to replace the proofs with the ones I mentioned in that email. It's a dirty solution, but it should get you going for now.

An alternative would be to try to figure out what's up with executing z3 in your system. I don't know so much about that.

Cheers,
    Thomas.

________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Mario Alvarez <mmalvare at eng.ucsd.edu>
Sent: Thursday, March 22, 2018 5:30 AM
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] Error Building HOL-Word

Hi Isabelle-Users,

I am trying to compile some files from the eth-isabelle
<https://github.com/pirapira/eth-isabelle> project using the command-line
version of Isabelle (e.g. isabelle process -T TheoryName). It seems like
the error is due to a dependency on the HOL-Word library.

In fact, I notice that the HOL-Word library fails to build. When I run
isabelle build HOL-Word, I get a failure with the following error (at the
end):

### theory "HOL-Word.WordBitwise"
### 0.591s elapsed time, 2.297s cpu time, 0.234s GC time
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "apply" (line 284 of
"~~/src/HOL/Word/Bit_Representation.thy")
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 12 of "~~/src/HOL/Word/Misc_Numeric.thy")
Unfinished session(s): HOL-Word
0:00:37 elapsed time, 0:01:11 cpu time, factor 1.91

I assume this isn't expected behavior for trying to build HOL-Word (but let
me know if I'm wrong about that).

Strangely, this doesn't appear to be a problem when I open the files that
require this dependency in the JEdit interface to Isabelle: the file
processes successfully without any errors. Do you have any ideas why this
might be failing and what I can do to get it to build?

Best,
Mario




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.