Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [isabelle-dev] Towards the Isabelle2017 release

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

From: Gerwin.Klein@data61.csiro.au
My plan would be to fork the AFP 2017 release branch tomorrow (around midnight CET from Mon to Tue).

There still seems to be quite a bit of ongoing activity - if there is anything that needs to go into the afp-2017 release, please let me know.

Cheers,
Gerwin

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

From: Lars Hupel <hupel@in.tum.de>
Right, that's a problem of these tools. They include the "thys" folder internally, and because Isabelle/Scala doesn't deduplicate ROOTS entries, this leads to the clash you noticed. I'm unsure what the proper fix is.

Cheers
Lars

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

From: Makarius <makarius@sketis.net>
Actual deduplication would require a proper semantic equality on
directories, but that is in general unclear. There might be other
solutions emerging eventually.

For now, here is an approximative check for the presence of AFP in
Isabelle/Scala (the canonical Isabelle system programming language):

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

Makarius

Last updated: Nov 21 2024 at 12:39 UTC