Problem in AFP

Makarius makarius at sketis.net
Wed Dec 24 16:27:49 CET 2025


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



More information about the isabelle-dev mailing list