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.

--Mario

On Wed, Mar 21, 2018 at 5:27 PM, <Thomas.Sewell at data61.csiro.au> 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:
> 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.