Asta Halkjær From (Dec 05 2024 at 12:14): Asta Halkjær From (Dec 05 2024 at 12:14):Hi! My email changed. Can I just update afp-devel/metadata/authors.toml or is there anything to be aware of? Similarly, I've updated the LaTeX abstract of an entry. Do I just update afp-devel/metadata/entries/X.toml correspondingly or is there more to it? Thanks! :-)
Fabian Huch (Dec 05 2024 at 12:55):If you change the metadata then make sure that you didn't break anything, e.g. by invoking isabelle afp_check_metadata.
And the abstract for entries is not latex but mathjax. If you want a preview of that, use isabelle afp_edit_metadata.
Asta Halkjær From (Dec 16 2024 at 10:23):Thanks, @Fabian Huch. Without changing anything, I cannot run either of those tools and I'm not quite sure why. Is this only supposed to be done by the initiated? :)
~/afp-devel (default)> isabelle afp_check_metadata
### Missing Isabelle component: "/Users/lnr875/.isabelle/contrib/hugo-0.119.0"
### Building AFP/Tools (/Users/lnr875/afp-devel/tools/lib/classes/afp_tools.jar) ...
Not found: Build_CI
Not found: type Isabelle_CI_Jobs
value ok is not a member of object isabelle.Mercurial.Hg_Sync
Not found: Build_CI
Not found: Build_CI
Not found: Build_CI
Not found: Build_CI
Not found: Build_CI
value ok is not a member of object isabelle.Mercurial.Hg_Sync
9 errors found
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:43:28
43 | val mail_system: Option[Build_CI.Mail_System],
| ^^^^^^^^
| Not found: Build_CI
|
| longer explanation available when compiling with `-explain`
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:245:22
245 |class CI_Jobs extends Isabelle_CI_Jobs(AFP_Build_CI.all, AFP_Build_CI.presentation)
| ^^^^^^^^^^^^^^^^
| Not found: type Isabelle_CI_Jobs
|
| longer explanation available when compiling with `-explain`
-- [E008] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:57:28
57 | if (Mercurial.Hg_Sync.ok(isabelle_path)) File.read(isabelle_path + Mercurial.Hg_Sync.PATH_ID)
| ^^^^^^^^^^^^^^^^^^^^
| value ok is not a member of object isabelle.Mercurial.Hg_Sync
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:71:43
71 | new Context(options, Store(options), Build_CI.Mail_System.try_open(options), afp)
| ^^^^^^^^
| Not found: Build_CI
|
| longer explanation available when compiling with `-explain`
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:84:20
84 | progress.echo(Build_CI.section("NOTIFICATIONS"))
| ^^^^^^^^
| Not found: Build_CI
|
| longer explanation available when compiling with `-explain`
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:145:18
145 | progress.echo(Build_CI.section("SITEGEN"))
| ^^^^^^^^
| Not found: Build_CI
|
| longer explanation available when compiling with `-explain`
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:193:4
193 | Build_CI.Job("all",
| ^^^^^^^^
| Not found: Build_CI
|
| longer explanation available when compiling with `-explain`
-- [E006] Not Found Error: /Users/lnr875/afp-devel/tools/afp_build_ci.scala:216:4
216 | Build_CI.Job("presentation",
| ^^^^^^^^
| Not found: Build_CI
|
| longer explanation available when compiling with `-explain`
-- [E008] Not Found Error: /Users/lnr875/afp-devel/tools/afp_structure.scala:130:26
130 | if (Mercurial.Hg_Sync.ok(base_dir)) File.read(base_dir + Mercurial.Hg_Sync.PATH_ID)
| ^^^^^^^^^^^^^^^^^^^^
| value ok is not a member of object isabelle.Mercurial.Hg_Sync
9 errors found
*** Failed to compile Scala sources
This looks like your afp-devel and isabelle-devel are out of sync. If you update both to the current version, you should be able to run it.
Last updated: Dec 21 2024 at 12:33 UTC