Email Gateway (Oct 27 2025 at 19:23): Email Gateway (Oct 27 2025 at 19:23):From: Florian Haftmann <florian.haftmann@cit.tum.de>
isabelle: e9e3caa03b2e tip
afp: 06d77fc7c645 tip
$ isabelle build Elliptic_Functions
*** Cannot load theory "Polylog.Polylog_Library"
*** The error(s) above occurred for theory "Polylog.Polylog_Library"
*** (required by "Elliptic_Functions.Dedekind_Eta" via
"Elliptic_Functions.Theta_Inversion") (line 6 of
"/home/haftmann/data/tum/afp/master/thys/Elliptic_Functions/Theta_Inversion.thy")
*** Cannot load theory "Polylog.Polylog_Library"
*** No such file: "Polylog.Polylog_Library"
*** The error(s) above occurred in session "Elliptic_Functions" (line 3
of "/home/haftmann/data/tum/afp/master/thys/Elliptic_Functions/ROOT")
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Dec 24 2025 at 14:45):From: Florian Haftmann <florian.haftmann@cit.tum.de>
isabelle: 028c1567a44c tip
afp: 7f51ddf2b695 tip
$ isabelle build -b Pure
Building AFP/Tools (/home/haftmann/data/tum/isabelle/devel/../../afp/devel/tools/lib/classes/afp_tools.jar) ...
value init0 is not a member of object isabelle.Options - did you mean Options.init?
1 error found
-- [E008] Not Found Error: /home/haftmann/data/tum/isabelle/devel/../../afp/devel/tools/afp_structure.scala:139:39
139 | def apply(options: Options = Options.init0(), base_dir: Path = AFP.BASE): AFP_Structure =
| ^^^^^^^^^^^^^
|value init0 is not a member of object isabelle.Options - did you mean Options.init?
1 error found
*** Failed to compile Scala sources
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Dec 24 2025 at 15:28):From: Makarius <makarius@sketis.net>
On 24/12/2025 15:45, Florian Haftmann wrote:
isabelle: 028c1567a44c tip
afp: 7f51ddf2b695 tip$ isabelle build -b Pure
Building AFP/Tools (/home/haftmann/data/tum/isabelle/devel/../../afp/
devel/tools/lib/classes/afp_tools.jar) ...
value init0 is not a member of object isabelle.Options - did you mean
Options.init?
1 error found
-- [E008] Not Found Error: /home/haftmann/data/tum/isabelle/devel/../../afp/
devel/tools/afp_structure.scala:139:39 139 | def apply(options: Options =
Options.init0(), base_dir: Path = AFP.BASE): AFP_Structure =
| ^^^^^^^^^^^^^
|value init0 is not a member of object isabelle.Options - did you mean
Options.init?
1 error found
*** Failed to compile Scala sources
Thanks. I had forgotten to commit/push the following:
changeset: 16295:3bf07833448a
tag: tip
user: wenzelm
date: Wed Dec 24 16:24:33 2025 +0100
files: tools/afp_structure.scala
description:
adapted to Isabelle/622240a84dea;
diff -r 7f51ddf2b695 -r 3bf07833448a tools/afp_structure.scala
--- a/tools/afp_structure.scala Wed Dec 24 11:01:42 2025 +0100
+++ b/tools/afp_structure.scala Wed Dec 24 16:24:33 2025 +0100
@@ -136,6 +136,6 @@
}
object AFP_Structure {
def apply(options: Options = Options.init0(), base_dir: Path = AFP.BASE):
AFP_Structure =
def apply(options: Options = Options.defaults, base_dir: Path = AFP.BASE):
AFP_Structure =
new AFP_Structure(options, base_dir.absolute)
}
The confusion was actually caused by IntelliJ IDEA and its convenient
automatic renaming, while our project layout spans two repositories.
Makarius
Last updated: Jan 07 2026 at 16:34 UTC