[isabelle] Fwd: Error Building HOL-Word

(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 at gmail.com>
Date: Wed, May 2, 2018, 1:49 PM
Subject: Re: [isabelle] Error Building HOL-Word
To: <makarius at sketis.net>
Cc: Mario Alvarez <mmalvare at eng.ucsd.edu>, <isabelle-users at 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


On Wed, May 2, 2018 at 2:47 AM Makarius <makarius at 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

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