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:
isabelle serveron one terminal.isabelle client -n isabelleon another.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.