Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Inconsistent behaviour between Isabelle/HOL in...

view this post on Zulip Email Gateway (May 17 2023 at 04:36):

From: Ian Hayes <Ian.Hayes@uq.edu.au>
We have a set of theory files that load into the JEdit version of
Isabelle/HOL with no problem but when we try to do the command line
build of the files, it fails with a "Failed to meet type constraint" error.

To further confuse the issue it fails under the Windows version of
Isabelle/HOL but is fine under the Linux version running under WSL.

To even further confuse the issue it fails on a very old MacBook*
(HighSierra) but is fine under a new MacBook M1 Pro (Ventura) and a
Intel iMac (Ventura).

Is this a bug in Isabelle/HOL or is there really a problem with our
theory files?

Does anyone have an idea of why the behaviour is inconsistent between
JEdit and command line build?

Thanks in advance
Ian Hayes

view this post on Zulip Email Gateway (May 17 2023 at 08:29):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

others on this list (e.g. Makarius, presumably) will probably be more
qualified to comment on your problem as such. But I'm happy to take a
few stabs in the dark.

Firstly, I'd just like to point out that it would probably be
tremendously helpful to anyone investigating this if you could provide a
minimum (non-)working example.

And, just to clarify what exactly you are experiencing: What you are
saying is that building it in Isabelle/JEdit works *always and
everywhere*, whereas building it with "isabelle build" consistently
fails on Windows and an old Macbook but consistently works on Linux,
WSL, and a new MacBook?

In any case: what architecture are you using? x86_64_32, x86_64, ARM?
The "new Macbook vs old Macbook" sounds like it could be an x86 vs ARM
issue (although that does not explain the Windows vs. Linux/WSL issue).
Have you tried switching to a different architecture? Have you tried
switching "isabelle build" to single-threaded? Have you tried isolating
the problematic segment of the relevant theory file and building that alone?

Okay, so here are some thoughts/theories:

  1. I recall that I personally had reproducibility issues with Isabelle
    two times. The first time it was a Poly/ML bug (a race condition in the
    ML runtime) that only manifested on Linux and only on some of the
    computers I tested it on and only with hyperthreading enabled and even
    then only sometimes. The second time it was a student who had
    overclocked his system a bit too eagerly (everything worked fine,
    including all normal stability tests, but Isabelle was too much for his
    poor CPU).

But in both cases what I got was a crash and not a "type error", and it
seems unlikely that an issue like this would cause something oddly
specific like that. I doubt that a hardware defect is the cause in your
case, but a threading issue is at least somewhat plausible.

  1. Your problem also reminds me of some reproducibility issues Peter
    Lammich had a few years ago with interactive build vs batch build that
    boiled down to some multithreading issues. As I recall, some tactics
    behaved differently with and without parallelism enabled, which caused
    some schematic variables to be instantiated in different orders, thus
    leading to a different result. I'm not sure if your issue could
    something similar.

  2. I heard of that there are some "non-official" packaged versions of
    Isabelle in various package managers which replace Isabelle's bundled
    versions of various libraries and components with packaged versions
    (presumably to save disc space/make the download smaller). That can of
    course cause all kinds of issues and is therefore heavily discouraged.
    But since you mentioned Windows being affected, I doubt that this is
    what is going on (I think this typically is more of a Linux/Mac thing).

  3. This is a real long shot but I'm mentioning it anyway just to be
    sure: I have seen all kinds of bizarre problems on Windows being caused
    by third-party antivirus software like Kaspersky, McAfee, etc. Not
    Isabelle-related and usually more in the sense of something crashing
    rather than a "semantic" error like yours, but still – it might be worth
    a shot to try and disable any antivirus software you might have (Windows
    Defender should be fine). Wouldn't explain the Mac issue though.

Cheers,

Manuel

view this post on Zulip Email Gateway (May 17 2023 at 11:31):

From: Makarius <makarius@sketis.net>
(I am presently busy with other things, but will come back to this thread later.)

Just a quick comment: Old Apple hardware works nicely and smoothly with Linux
--- sometimes Ubuntu Mate is easier to install than regular Ubuntu, with all
hardware drivers working immediately. I've recently refurbished several old
machines. Policies by Apple regarding macOS can be safely ignored.

In any case, you do need min. 8 GB RAM for Isabelle applications, better 16 GB.

Makarius

view this post on Zulip Email Gateway (May 17 2023 at 18:22):

From: Makarius <makarius@sketis.net>
jEdit is just a Java-based text editor --- you mean Isabelle/PIDE with the
Isabelle/jEdit front-end: That is a very complex interactive computer-game for
development of theories and proofs.

Many fine points differ in the interactive game vs. a batch-build via
"isabelle build". The latter counts as authentic, the former only as an
approximation.

Both use shared-memory multiprocessing by default: In very rare corner cases
that can cause problems that don't show up with "isabelle build threads=1"

Makarius

Last updated: Apr 27 2024 at 04:17 UTC