Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] About isabelle build's error using afp version...

view this post on Zulip Email Gateway (May 02 2025 at 13:19):

From: Hongjian Jiang <jianghongjian87@gmail.com>
Hi all,

I'm currently trying to learn how to generate executable code and understand
aspects of proof systems. For this purpose, I'm exploring the AFP entry
FOL_Seq_Calc (1–3).

However, I encountered an error when attempting to build the theory using the
command listed in FOL_Seq_Calc3/export.thy: isabelle build -e -D ..

The error message is as follows:

HOL-Library FAILED (see also "isabelle build_log -H Error HOL-Library")
*** Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-
Library.Finite_Map")
*** Failed to load theory "HOL-Library.Library" (unresolved "HOL-
Library.Disjoint_FSets", "HOL-Library.Finite_Map")
*** Code check failed for Scala: isabelle_scala scalac
$ISABELLE_SCALAC_OPTIONS ROOT.scala
*** At command "export_code" (line 1408 of "~~/src/HOL/Library/
Finite_Map.thy")
FOL_Seq_Calc3 CANCELLED
Unfinished session(s): FOL_Seq_Calc3, HOL-Library
0:04:50 elapsed time, 0:22:20 cpu time, factor 4.61

For your information, I tried this on two machines, and both fail:

  1. A MacBook running macOS 14.6.1 with a 2.6 GHz 6-Core Intel Core i7

  2. A Mac Studio with an M1 chip

view this post on Zulip Email Gateway (May 02 2025 at 13:39):

From: Asta Halkjær From <cl-isabelle-users@lists.cam.ac.uk>
Hi,

This is my entry, but the error seems to happen before Isabelle even gets that far, so that seems to be irrelevant.
I cannot reproduce the issue with my Isabelle2025 on Intel hardware, where the listed command succeeds.

Maybe it looks familiar to someone else?

Best,
Asta

From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Hongjian Jiang <jianghongjian87@gmail.com>
Sent: 02 May 2025 15:19:02
To: cl-isabelle-users@lists.cam.ac.uk
Subject: [isabelle] About isabelle build's error using afp version 2025 and isabelle 2025

[Du får ikke ofte mails fra jianghongjian87@gmail.com. Få mere at vide om, hvorfor dette er vigtigt, på https://aka.ms/LearnAboutSenderIdentification ]

Hi all,

I'm currently trying to learn how to generate executable code and understand
aspects of proof systems. For this purpose, I'm exploring the AFP entry
FOL_Seq_Calc (1–3).

However, I encountered an error when attempting to build the theory using the
command listed in FOL_Seq_Calc3/export.thy: isabelle build -e -D ..

The error message is as follows:

HOL-Library FAILED (see also "isabelle build_log -H Error HOL-Library")
*** Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-
Library.Finite_Map")
*** Failed to load theory "HOL-Library.Library" (unresolved "HOL-
Library.Disjoint_FSets", "HOL-Library.Finite_Map")
*** Code check failed for Scala: isabelle_scala scalac
$ISABELLE_SCALAC_OPTIONS ROOT.scala
*** At command "export_code" (line 1408 of "~~/src/HOL/Library/
Finite_Map.thy")
FOL_Seq_Calc3 CANCELLED
Unfinished session(s): FOL_Seq_Calc3, HOL-Library
0:04:50 elapsed time, 0:22:20 cpu time, factor 4.61

For your information, I tried this on two machines, and both fail:

  1. A MacBook running macOS 14.6.1 with a 2.6 GHz 6-Core Intel Core i7

  2. A Mac Studio with an M1 chip

view this post on Zulip Email Gateway (May 04 2025 at 10:29):

From: Hongjian Jiang <jianghongjian87@gmail.com>
Hi Asta,

It appears to work on the Linux system. However, after compiling with ghc -O2 -i./program Main.hs.

I receive the following error:

[1 of 3] Compiling Arith            ( program/Arith.hs, program/Arith.o )

program/Arith.hs:28:33: error:
    Module ‘Data.Bits’ does not export ‘(.^.)’
   |
28 | import Data.Bits ((.&.), (.|.), (.^.));
   |                                 ^^^^^

Best

Hongjian

Asta Halkjær From <asfr@di.ku.dk> 于2025年5月2日周五 15:39写道：

Hi,

This is my entry, but the error seems to happen before Isabelle even gets
that far, so that seems to be irrelevant.
I cannot reproduce the issue with my Isabelle2025 on Intel hardware, where
the listed command succeeds.

Maybe it looks familiar to someone else?

Best,
Asta

From: cl-isabelle-users-request@lists.cam.ac.uk <
cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Hongjian Jiang <
jianghongjian87@gmail.com>
Sent: 02 May 2025 15:19:02
To: cl-isabelle-users@lists.cam.ac.uk
Subject: [isabelle] About isabelle build's error using afp version 2025
and isabelle 2025

[Du får ikke ofte mails fra jianghongjian87@gmail.com. Få mere at vide
om, hvorfor dette er vigtigt, på
https://aka.ms/LearnAboutSenderIdentification ]

Hi all,

I'm currently trying to learn how to generate executable code and
understand
aspects of proof systems. For this purpose, I'm exploring the AFP entry
FOL_Seq_Calc (1–3).

However, I encountered an error when attempting to build the theory using
the
command listed in FOL_Seq_Calc3/export.thy: isabelle build -e -D ..

The error message is as follows:
HOL-Library FAILED (see also "isabelle build_log -H Error HOL-Library") *** Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL- Library.Finite_Map") *** Failed to load theory "HOL-Library.Library" (unresolved "HOL- Library.Disjoint_FSets", "HOL-Library.Finite_Map") *** Code check failed for Scala: isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala *** At command "export_code" (line 1408 of "~~/src/HOL/Library/ Finite_Map.thy") FOL_Seq_Calc3 CANCELLED Unfinished session(s): FOL_Seq_Calc3, HOL-Library 0:04:50 elapsed time, 0:22:20 cpu time, factor 4.61

For your information, I tried this on two machines, and both fail:

  1. A MacBook running macOS 14.6.1 with a 2.6 GHz 6-Core Intel Core i7

  2. A Mac Studio with an M1 chip

view this post on Zulip Email Gateway (May 04 2025 at 11:12):

From: Asta Halkjær From <cl-isabelle-users@lists.cam.ac.uk>
Hi,

Are you running an old GHC? I can compile the exported code on version 9.6.7.

It seems you need at least base-4.17:

https://hackage.haskell.org/package/base-4.21.0.0/docs/Data-Bits.html#v:.-94-.

Best,
Asta

From: Hongjian Jiang <jianghongjian87@gmail.com>
Sent: 04 May 2025 12:29:03
To: Asta Halkjær From
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] About isabelle build's error using afp version 2025 and isabelle 2025

Du får ikke ofte mails fra jianghongjian87@gmail.com. Få mere at vide om, hvorfor dette er vigtigt<https://aka.ms/LearnAboutSenderIdentification>

Hi Asta,

It appears to work on the Linux system. However, after compiling with ghc -O2 -i./program Main.hs.

I receive the following error:

[1 of 3] Compiling Arith            ( program/Arith.hs, program/Arith.o )

program/Arith.hs:28:33: error:
    Module ‘Data.Bits’ does not export ‘(.^.)’
   |
28 | import Data.Bits ((.&.), (.|.), (.^.));
   |                                 ^^^^^

Best

Hongjian

Asta Halkjær From <asfr@di.ku.dk<mailto:asfr@di.ku.dk>> 于2025年5月2日周五 15:39写道：
Hi,

This is my entry, but the error seems to happen before Isabelle even gets that far, so that seems to be irrelevant.
I cannot reproduce the issue with my Isabelle2025 on Intel hardware, where the listed command succeeds.

Maybe it looks familiar to someone else?

Best,
Asta

From: cl-isabelle-users-request@lists.cam.ac.uk<mailto:cl-isabelle-users-request@lists.cam.ac.uk> <cl-isabelle-users-request@lists.cam.ac.uk<mailto:cl-isabelle-users-request@lists.cam.ac.uk>> on behalf of Hongjian Jiang <jianghongjian87@gmail.com<mailto:jianghongjian87@gmail.com>>
Sent: 02 May 2025 15:19:02
To: cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] About isabelle build's error using afp version 2025 and isabelle 2025

[Du får ikke ofte mails fra jianghongjian87@gmail.com<mailto:jianghongjian87@gmail.com>. Få mere at vide om, hvorfor dette er vigtigt, på https://aka.ms/LearnAboutSenderIdentification ]

Hi all,

I'm currently trying to learn how to generate executable code and understand
aspects of proof systems. For this purpose, I'm exploring the AFP entry
FOL_Seq_Calc (1–3).

However, I encountered an error when attempting to build the theory using the
command listed in FOL_Seq_Calc3/export.thy: isabelle build -e -D ..

The error message is as follows:

HOL-Library FAILED (see also "isabelle build_log -H Error HOL-Library")
*** Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-
Library.Finite_Map")
*** Failed to load theory "HOL-Library.Library" (unresolved "HOL-
Library.Disjoint_FSets", "HOL-Library.Finite_Map")
*** Code check failed for Scala: isabelle_scala scalac
$ISABELLE_SCALAC_OPTIONS ROOT.scala
*** At command "export_code" (line 1408 of "~~/src/HOL/Library/
Finite_Map.thy")
FOL_Seq_Calc3 CANCELLED
Unfinished session(s): FOL_Seq_Calc3, HOL-Library
0:04:50 elapsed time, 0:22:20 cpu time, factor 4.61

For your information, I tried this on two machines, and both fail:

  1. A MacBook running macOS 14.6.1 with a 2.6 GHz 6-Core Intel Core i7

  2. A Mac Studio with an M1 chip

Last updated: May 06 2025 at 08:28 UTC