Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Error Building HOL-Word


view this post on Zulip Email Gateway (Aug 22 2022 at 17:19):

From: Makarius <makarius@sketis.net>
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


Last updated: Apr 18 2024 at 08:19 UTC