Email Gateway (Aug 22 2022 at 16:58): Email Gateway (Aug 22 2022 at 16:58):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
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):
*** 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
Email Gateway (Aug 22 2022 at 16:59):From: Thomas.Sewell@data61.csiro.au
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.
Email Gateway (Aug 22 2022 at 16:59):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
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
Email Gateway (Aug 22 2022 at 17:12):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
(Re-sending because I sent this from the wrong address originally, sorry if
both posts end up getting through)
---------- Forwarded message ---------
From: Mario Alvarez <mariomcgilvrayalvarez@gmail.com>
Date: Wed, May 2, 2018, 1:49 PM
Subject: Re: [isabelle] Error Building HOL-Word
To: <makarius@sketis.net>
Cc: Mario Alvarez <mmalvare@eng.ucsd.edu>, <isabelle-users@cl.cam.ac.uk>
Hi Makarius,
Thanks for checking this out.
In case you're curious to know more about my development environment: I use
WSL for command-line interaction, but a windows-native version of
Isabelle/JEdit for actual development. This works mostly fine except for
this issue around Z3 integration, which I've managed to work around now by
changing some proofs in the standard library. When I get a chance (which
may not be for a while) I may play around with Z3 a little more on WSL to
see when/why it's failing.
Also, if you really want a GUI environment for WSL, you can install a
Windows-native X-server. I've gotten Isabelle/JEdit to work this way, but
it tends to be slower (especially UI interactions) than the Windows-native
Isabelle/JEdit.
--Mario
On Wed, May 2, 2018 at 2:47 AM Makarius <makarius@sketis.net> wrote:
On 22/03/18 01:30, Mario Alvarez wrote:
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.*** 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")I have now experimented with the new Windows Subsystem for Linux (on
Windows 10 with Ubuntu from the MS app store). It is interesting that
Windows has now become another platform for Linux. It generally looks
fine, but there are some restrictions:- there is no GUI environment, only a bash command-line
- I did not manage to run x86-linux executables, only x86_64-linux
(this is relevant for poly)For z3, I had to install libgomp1, but it still produced error code 110
as above.I have also made a quick experiment with Z3 4.6.0
https://github.com/Z3Prover/z3/releases -- it does not crash, but causes
other problems, e.g. in ~~/src/HOL/SMT_Examples/SMT_Tests.thy like
"Unsupported: trans*" and many timeouts.Makarius
Email Gateway (Aug 22 2022 at 17:46):From: Makarius <makarius@sketis.net>
The subsequent problem is still open for Isabelle2018-RC1, i.e. Z3 does
not work with the Linux Subsystem for Windows 10. This is particularly
sad, since HOL-Algebra now requires it, too.
Note that Larry Paulson and/or Jasmin Blanchette need to say what to do
about it for the Isabelle2018 release.
Makarius
Email Gateway (Aug 22 2022 at 17:47):From: Makarius <makarius@sketis.net>
On 6 Jul 2018, at 21:40, Makarius <makarius@sketis.net> wrote:
The subsequent problem is still open for Isabelle2018-RC1, i.e. Z3 does
not work with the Linux Subsystem for Windows 10. This is particularly
sad, since HOL-Algebra now requires it, too.Note that Larry Paulson and/or Jasmin Blanchette need to say what to do
about it for the Isabelle2018 release.
Last updated: Apr 18 2024 at 20:16 UTC