[isabelle-dev] Cannot compile the latest version

[Fabian Huch]

On which version of Isabelle/AFP are you on? Isabelle/be0865060346 + 
AFP/1e0f664cffc8 works for me.


Fabian

On 7/7/22 18:00, Lawrence Paulson wrote:
> See the error messages below. Presumably something to do with Scala?
>
> Larry
>
> searching for changes
> no changes found
> src/HOL: isabelle components -a
> src/HOL: isabelle build  HOL-Complex_Analysis
> ### Building AFP/Tools (/Users/lp15/isabelle/afp/devel/tools/lib/classes/afp_tools.jar) ...
> `inline` must be followed by an `if` or a `match`
> `inline` must be followed by an `if` or a `match`
> non-private method make_author_id in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (name: String, context: afp.migration.AFP_Migrate_Metadata.Context): String
> non-private method author_urls in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (name_urls: String, context: afp.migration.AFP_Migrate_Metadata.Context): (
>    String
> , List[String])
> non-private method add_email in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (author: afp.Metadata.Author, address: String, context:
>    afp.migration.AFP_Migrate_Metadata.Context
> ): (afp.Metadata.Author, afp.Metadata.Email)
> non-private method get_affiliations in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (name_url: String, context: afp.migration.AFP_Migrate_Metadata.Context):
>    List[afp.Metadata.Affiliation]
> non-private method get_email_affiliation in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (address: String, context: afp.migration.AFP_Migrate_Metadata.Context,
>    progress
> : isabelle.Progress): afp.Metadata.Email
> non-private method update_author in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (name_urls: String, context: afp.migration.AFP_Migrate_Metadata.Context): Unit
> non-private method map_entry in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (entry: isabelle.AFP.Entry, releases:
>    Map[afp.Metadata.Entry.Name, List[afp.Metadata.Release]]
> , topics: Map[afp.Metadata.Topic.ID, afp.Metadata.Topic], sitegen_ignore:
>    Boolean
> , context: afp.migration.AFP_Migrate_Metadata.Context, progress:
>    isabelle.Progress
> ): afp.Metadata.Entry
> non-private method parse_change_history in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (history: String, context: afp.migration.AFP_Migrate_Metadata.Context):
>    afp.Metadata.Change_History
> non-private method parse_releases in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (releases: List[String], isabelle_releases: List[String], all_entries:
>    List[afp.Metadata.Entry.Name]
> , context: afp.migration.AFP_Migrate_Metadata.Context):
>    List[afp.Metadata.Release]
> non-private method migrate_metadata in object AFP_Migrate_Metadata refers to private class Context
> in its type signature (base_dir: isabelle.Path, overwrite: Boolean, context:
>    afp.migration.AFP_Migrate_Metadata.Context
> , options: isabelle.Options, progress: isabelle.Progress): Unit
> Missing parameter type
>
> I could not infer the type of the parameter x$1 of expanded function:
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev