Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP2017 preparations


view this post on Zulip Email Gateway (Aug 22 2022 at 16:10):

From: Lars Hupel <hupel@in.tum.de>

def check_afp(options: Options): Boolean =
Sessions.load(options).get("Example-Submission").isDefined

I was just trying to make this change and realized that this is not the
full story.

The "afp_check_roots" tool specifically tries to load all sessions from
the "$AFP" directory and checks whether they are all tagged correctly.

Assuming that "$AFP" is already added to a "ROOTS" file somewhere, how
am I supposed to obtain all sessions that have been defined in "$AFP"?

Previously, I used this:

val full_tree = Sessions.load(options, Nil, List(afp_dir))
val (selected, _) = full_tree.selection(Sessions.Selection.empty)

If I insert a conditional to use "Nil" instead of "List(afp_dir)" if
"Example_Submission" is defined, I (naturally) get the empty selection here.

Cheers
Lars


Last updated: Apr 26 2024 at 04:17 UTC