Email Gateway (Aug 19 2022 at 14:04): Email Gateway (Aug 19 2022 at 14:04):From: John Wickerson <johnwickerson@cantab.net>
Dear all,
I wanted to share what I found to be quite a surprising observation: there are .thy files in the AFP that have errors.
Consider the following AFP entry:
I downloaded the entry, and found a file listing all of the .thy files that go into that session.
theory Slicing
imports
"Basic/Postdomination"
"Basic/CFGExit_wf"
"Basic/SemanticsCFG"
"Dynamic/DynSlice"
"StaticIntra/CDepInstantiations"
"StaticIntra/ControlDependenceRelations"
"While/DynamicControlDependences"
"While/NonInterferenceWhile"
"JinjaVM/JVMControlDependences"
"JinjaVM/SemanticsWF"
beginend
All of those .thy files, and all of the .thy files on which they depend, work fine. However, the entry actually contains several other files, such as "Basic/DynDataSlice", on which no file in the list above depends, and which actually has errors in.
I found this situation a bit unsettling. I assumed that when I downloaded something from the AFP, I could automatically depend on any lemma in any .thy file therein, but it seems that this is not the case -- I first must check that the .thy file is in the session.
If this is a problem unique to the Slicing entry, then I apologise to the authors for singling them out! But I suspect that there will be other entries in the AFP that contain spare .thy files lying around. And if my analysis of the situation is correct thus far, can I suggest that it might be a good thing to audit the AFP, and ensure for each entry that the set of .thy files that are actually part of the session is identical to the set of .thy files in the entry's directory?
Best wishes,
John
Email Gateway (Aug 19 2022 at 14:04):From: Peter Lammich <lammich@in.tum.de>
Some time ago, when the new Isabelle build system was introduced,
some files in an AFP entry of mine where accidently excluded from the
session due to conversion errors of the old Makefiles. I only noticed
that by chance some time later.
So before deleting seemingly unused files, one should also audit the
VCS-history of those entries whether these files used to be in the
session at some point, and, if so, why/by whom they where removed.
Email Gateway (Aug 19 2022 at 14:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi John,
Looking back at the original submission in 2009 reveals that the Slicing theory
Basic/DynDataSlice has never been checked at all. It really seems to be a bogus theory,
because the theory Dynamic/DynPDG contains all of DynDataSlice under the section data
slice. I've deleted this theory from the AFP (b1fac8197a56), and the next release will no
longer contain it.
Thanks for reporting this,
Andreas
Email Gateway (Aug 19 2022 at 14:05):From: Makarius <makarius@sketis.net>
The administrative scripts for AFP are still using rather old-fashioned
scripts. With a little bit of Isabelle/Scala the above should be quite
easy to do, e.g. using isabelle.File.find_files and operations from
isabelle.Build that correspond to "isabelle build -nal" on the command
line.
I leave it as an exercise to the AFP editors, or anybody else who wants to
learn some higher-order functional-objected-oriented system programming.
The "system" manual explains how to use the Scala script wrapper for
hash-bang compile-and-run (which is a bit slow, but this should not be a
problem for a batch job).
Makarius
Last updated: Nov 21 2024 at 12:39 UTC