Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Cannot compile the latest version

view this post on Zulip Email Gateway (Jul 07 2022 at 16:00):

From: Lawrence Paulson <lp15@cam.ac.uk>
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Jul 07 2022 at 16:03):

From: Fabian Huch <huch@in.tum.de>
On which version of Isabelle/AFP are you on? Isabelle/be0865060346 +
AFP/1e0f664cffc8 works for me.

Fabian

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Jul 07 2022 at 16:06):

From: Lawrence Paulson <lp15@cam.ac.uk>
Sorry I forgot one needs to have the latest version of the AFP as well. Thanks

Larry

Last updated: Apr 26 2024 at 16:20 UTC