Isabelle Server HOL-Library Build Failed

50 views Asked by At

I'm trying to build a session through isabelle server on Isabelle 2023. The sessions itself are pretty long, but I have narrowed the problem down into HOL-Library.

It outputs the following log on isabelle client:

...
NOTE {
   "task":"c8838e1c-0189-4647-a5a0-892bb33cbe62",
   "message":"HOL-Library: theory HOL-Library.RBT_Set",
   "kind":"writeln",
   "session":"HOL-Library",
   "theory":"HOL-Library.RBT_Set"
}
...
NOTE {
   "kind":"writeln",
   "message":"HOL-Library FAILED 
(see also \"isabelle build_log -H Error HOL-Library\")",
   "verbose":"false",
   "task":"c8838e1c-0189-4647-a5a0-892bb33cbe62"
}
...
NOTE {
   "kind":"writeln",
   "message":"*** Failed to load theory \"HOL-Library.Library\" 
(unresolved \"HOL-Library.Pattern_Aliases\")\n*** exception Fail raised 
(line 205 of \"~~/src/HOL/Library/Pattern_Aliases.thy\"): Assertion failed\n*** 
At command \"ML\" (line 197 of \"~~/src/HOL/Library/Pattern_Aliases.thy\")",
   "verbose":"false",
   "task":"c8838e1c-0189-4647-a5a0-892bb33cbe62"
}
...
NOTE {
   "kind":"writeln",
   "message":"Unfinished session(s): HOL-Library",
   "verbose":"false",
   "task":"c8838e1c-0189-4647-a5a0-892bb33cbe62"
}
...

isabelle build_log produces the following:

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

Build errors:
*** Failed to load theory "HOL-Library.Library" 
    (unresolved "HOL-Library.Pattern_Aliases")
*** exception Fail raised 
    (line 205 of "~~/src/HOL/Library/Pattern_Aliases.thy"): Assertion failed
*** At command "ML" (line 197 of "~~/src/HOL/Library/Pattern_Aliases.thy")

Return code: 1 (ERROR)

HOL-Library.Pattern_Aliases exists in the src directory of Isabelle. This is a fresh install from the mirror website. I'm using a WSL2 install of Ubuntu 22.04.3 LTS.

These are the steps that I used:

  1. isabelle server on one terminal.
  2. isabelle client -n isabelle on another.
  3. session_build { "session": "HOL-Library", "options": ["document=false", "show_question_marks=false", "quick_and_dirty"], "dirs": [], "include_sessions": [], "verbose": true }

It shouldn't give an error, especially if it's only building the HOL-Library. However, Isabelle jEdit runs fine, and can build the theory from the sessions that I'm using.

0

There are 0 answers