[isabelle] Error Building HOL-Word



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.