Re: [isabelle] Error Building HOL-Word

Hi Thomas,

Thanks for the advice.

I am running the Windows Subsystem for Linux, which should be
binary-compatible with Linux. However, perhaps this binary compatibility
has a bug in the case of z3. I'll try manually editing those two theories
for now.


On Wed, Mar 21, 2018 at 5:27 PM, <Thomas.Sewell at> wrote:

> 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:
> 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 <
> cl-isabelle-users-bounces at> on behalf of Mario Alvarez <
> mmalvare at>
> Sent: Thursday, March 22, 2018 5:30 AM
> To: isabelle-users at
> Subject: [isabelle] Error Building HOL-Word
> Hi Isabelle-Users,
> I am trying to compile some files from the 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.