Stream: Beginner Questions

Topic: Isabelle's build error

view this post on Zulip Hongjian Jiang (May 02 2025 at 10:35):

I am installing Isabelle 2025, and the recent version of afp. And when i run the isabelle -e -D . under the folder of FOL_Seq_Cal3, it raises an error: 

isabelle build -e -D .
Building HOL-Library ...
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:01:20 elapsed time, 0:07:16 cpu time, factor 5.42

While I test it with: 

isabelle build_log -H Error HOL-Library

Theory "HOL-Library.Disjoint_FSets" (in HOL-Library): MISSING

Theory "HOL-Library.Library" (in HOL-Library): MISSING

Build errors:
*** 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")

Return code: 1 (ERROR)

Any idea what happens here?

view this post on Zulip Fabian Huch (May 02 2025 at 10:45):

I assume your Isabelle and AFP versions don't match.

view this post on Zulip Hongjian Jiang (May 02 2025 at 12:06):

Well, I used afp-2025-05-01 and Isabelle2025 (March 2025)

view this post on Zulip Hongjian Jiang (May 02 2025 at 12:07):

Building HOL-Library ...
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:01:22 elapsed time, 0:07:23 cpu time, factor 5.35

view this post on Zulip Fabian Huch (May 02 2025 at 12:21):

Hm, those of course do match. Do you have some sort of non-standard config for that installation? E.g. what does isabelle getenv ISABELLE_SCALAC_OPTIONS return?

view this post on Zulip Hongjian Jiang (May 02 2025 at 12:24):

ISABELLE_SCALAC_OPTIONS=-encoding UTF-8 -feature -java-output-version 21 -source 3.3 -old-syntax -no-indent -color never -pagewidth 78 -J-Xms512m -J-Xmx4g -J-Xss16m

view this post on Zulip Fabian Huch (May 02 2025 at 12:34):

No, that looks good. Your problem doesn't seem to be related to the AFP -- I assume isabelle build -e HOL-Library would already fail.
If this is a unmodified Isabelle2025 installation then you should really report this problem to the mailing list, including more details about the system you're running this on

view this post on Zulip Hongjian Jiang (May 02 2025 at 12:38):

Okay, thanks for the help. I will try on my other pc to see whether the problem also exists, then write to the mailing list.

Last updated: May 09 2025 at 08:28 UTC