Email Gateway (Aug 22 2022 at 15:58): Email Gateway (Aug 22 2022 at 15:58):From: Makarius <makarius@sketis.net>
Operations like Sessions.load or Sessions.selection provide an object of
type Sessions.T, which contains all session infos (with dependencies).
Such Session.Info entries contain the main session directory: it can be
used here to filter entries that are within the $AFP hierarchy like this:
val sessions = Sessions.load(options, dirs = List(Path.explode("$AFP")))
val afp_prefix = Path.explode("$AFP").canonical_file.toPath
val afp_sessions = for (info <- sessions.imports_topological_order if
info.dir.canonical_file.toPath.startsWith(afp_prefix)) yield info.name
Makarius
Email Gateway (Aug 22 2022 at 15:58):From: Lars Hupel <hupel@in.tum.de>
Does that work correctly wrt "in" clauses? In the past we had some
session that used "in ~~/..." or similar, and IIRC, the "info.dir" would
then point to the path specified by "in". The script should check that
no such thing is present in a "ROOT" file. (It currently does it, by
selecting all sessions from "$AFP" and looking at "info.dir".)
Email Gateway (Aug 22 2022 at 15:58):From: Makarius <makarius@sketis.net>
On 25/09/17 14:12, Lars Hupel wrote:
Operations like Sessions.load or Sessions.selection provide an object of
type Sessions.T, which contains all session infos (with dependencies).
Such Session.Info entries contain the main session directory: it can be
used here to filter entries that are within the $AFP hierarchy like this:Does that work correctly wrt "in" clauses?
info.dir correctly refers to the logical session directory, i.e.
whatever is specified implicitly or explicitly via 'in', but this is not
what you want here.
Note that systematic Isabelle/Scala operations on the syntax of
session ROOT entries would require access to Session_Entry, but that is
private to Sessions.Parser.
In the past we had some
session that used "in ~~/..." or similar, and IIRC, the "info.dir" >would
then point to the path specified by "in". The script should check that
no such thing is present in a "ROOT" file.
This sounds very odd.
I would say it belongs to the normal editorial routine to put ROOT
entries into a canonical form, such that oddities are easily spotted and
removed: i.e. a no-nonsense no-junk policy for AFP ROOT entries.
I've done such cleanup myself very often (apart from keeping AFP running
in the first place), but I've also seen a slight decline in this respect
in recent years.
Makarius
Email Gateway (Aug 22 2022 at 15:58):From: Lars Hupel <hupel@in.tum.de>
This sounds very odd.
The purpose of this script is to enforce canonical form of session
specifications. Or do you think the requirement to not use "in" is odd?
To clarify: as you have already said, we can't detect whether or not
"in" is syntactically present, but we can at least detect whether it
points to a subdirectory in "$AFP" or not. If it does, it is acceptable.
If not, it isn't.
I've done such cleanup myself very often (apart from keeping AFP running
in the first place), but I've also seen a slight decline in this respect
in recent years.
Great, but you're not the only one taking care of this. In the future
the "afp_check_roots" script might become part of the submission system.
After I've introduced this script there should be very little
non-canonical session specifications left.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:59):From: Makarius <makarius@sketis.net>
On 25/09/17 16:31, Lars Hupel wrote:
To clarify: as you have already said, we can't detect whether or not
"in" is syntactically present, but we can at least detect whether it
points to a subdirectory in "$AFP" or not. If it does, it is acceptable.
If not, it isn't.
We can't detect it in Isabelle2017, but in principle one could go back
to this later an look at the actual ROOT syntax (presently private). But
I am myself still unsure about this approach.
Another possibility is to revisit the duplicate session directory
problem after the release.
In the future the "afp_check_roots" script might become part of the submission system.
I have no proper overview of AFP admin tools and their requirements.
Maybe it all needs some general cleanup, and a bit more support in the
Isabelle/Scala library.
Concerning really hard checks on ROOT files, I would expect that as part
of the submission system in the first place. Anything pushed into AFP
should be somewhat sane already.
After I've introduced this script there should be very little
non-canonical session specifications left.
Non-canonical also means bad formatting and other informal garbage,
which such tools cannot easily detect.
I say this here, because the session-qualified theory names reform is
only half finished: I've spent a very long time struggling with odd AFP
ROOT entries, both syntactically and semantically.
Makarius
Email Gateway (Aug 22 2022 at 15:59):From: Lars Hupel <hupel@in.tum.de>
We can't detect it in Isabelle2017, but in principle one could go back
to this later an look at the actual ROOT syntax (presently private). But
I am myself still unsure about this approach.
In that case I will refrain from changing the scripts and will recommend
the AFP editors to continue using the AFP as a component and not
registering the "$AFP" directory as a session root.
Concerning really hard checks on ROOT files, I would expect that as part
of the submission system in the first place. Anything pushed into AFP
should be somewhat sane already.
AFP contributors can freely edit ROOT files in afp-devel after
acceptance, so more automation is better.
Email Gateway (Aug 22 2022 at 15:59):From: Peter Lammich <lammich@in.tum.de>
As I understand there are already a lot of AFP entries that have been edited
to use session qualified imports. These will not work if those sessions' ROOT
files are not registered
Peter
Email Gateway (Aug 22 2022 at 15:59):From: Lars Hupel <hupel@in.tum.de>
Normal AFP users and contributors have no need to follow this
recommendation, which only concerns AFP editors that run maintenance
scripts on the AFP.
Email Gateway (Aug 22 2022 at 15:59):From: Makarius <makarius@sketis.net>
Here is a slightly different approach, using the syntactic Position.T
field of Sessions.Info:
val infos =
for {
info <- sessions.imports_topological_order
file <- Position.File.unapply(info.pos)
if Path.explode(file).canonical_file.toPath.startsWith(afp_prefix)
} yield info.name
This use of Position.File is a bit fragile, though. It is not quite
canonical Isabelle/Scala systems programming. For the AFP admin tools it
should be OK for now.
Makarius
Last updated: Apr 23 2024 at 16:19 UTC