Email Gateway (Aug 22 2022 at 16:01): Email Gateway (Aug 22 2022 at 16:01):From: Matthew.Brecknell@data61.csiro.au
On Tue, 2017-08-22 at 11:15 +0200, Makarius wrote:
On 22/08/17 09:01, Matthew.Brecknell@data61.csiro.au wrote:
We have many theories and other source files which are generated at
various times during our lengthy build process. It seems that before I can
useisabelle jedit -dto load even our very first session, I must first
generate all files mentioned in all sessions accessible from the ROOTS
file, and all their theories.This sounds like a conflict of a legacy build process based on "make"
versus Isabelle session structure with "isabelle build" and now
increasingly inside Isabelle/jEdit.At some point you should try to overcome this tension, and do it all
within static theory sources (by loading other files into a theory from
within).Can this requirement be relaxed again, so that I only need the files for
the session I want to load?See the following NEWS entry:
- Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
image of the SESSION, with qualified theory imports restricted to that
portion of the session graph. Moreover, the ROOT entry of the SESSION is
opened in the editor.
Last week, I finished updating all our proofs to Isabelle2017-RC0,
without significant issues. I am still checking against RC1, but so far
so good.
However, I have noticed that in RC1, "isabelle jedit -R -l SESSION" no
longer ignores sessions that are not ancestors of SESSION. So now, we
really do need to generate all files mentioned in all sessions
accessible from the ROOTS file, and all their theories, before we can
open Isabelle/jEdit on any of our sessions.
This will make life very difficult for us.
I have thought about this since my previous email, and I doubt we can
ever escape what you describe as a "legacy build process" based on
"make".
One of the reasons for this: For our proofs about the seL4 C kernel, we
rely on the build process for the C kernel to generate preprocessed
sources. Our C parser, implemented in Isabelle/ML, then generates a C
specification from these preprocessed kernel sources. We need to mention
the preprocessed sources in a ROOT file, to ensure that Isabelle
rebuilds the session at the right times.
Without the leniency of the RC0 behaviour of "isabelle jedit -R", our
options appear to be:
There is also the chance that we find ourselves in a chicken-and-egg
situation, where we can't generate files because some theory is broken,
but we can't edit the theory because we haven't generated files! We
would need to temporarily patch our build system to bootstrap ourselves
out of such a situation.
Obviously, such a structure just re-encodes dependencies that are
already present in the ROOT files. So limiting the scope could be (and
indeed, was previously) automated by Isabelle/jEdit.
Neither of these options is attractive. We would really like some
mechanism to limit which sessions Isabelle/jEdit looks at, whether or not
that's "-R". There may be other options I have not considered, in which
case, I would welcome any reasonable suggestions!
Note that after Isabelle2017-RC0 (e.g. in current snapshots from
http://isabelle.in.tum.de/devel/release_snapshot) the session-qualified
imports are even more rigorous. It might cause additional problems for
your setup.
On the whole, session-qualified imports seem to be a very positive
change.
However, at least from the perspective of a user, they seem
unrelated to the
problem we're facing here.
Email Gateway (Aug 22 2022 at 16:02):From: Makarius <makarius@sketis.net>
On 05/09/17 08:02, Matthew.Brecknell@data61.csiro.au wrote:
I have noticed that in RC1, "isabelle jedit -R -l SESSION" no
longer ignores sessions that are not ancestors of SESSION. So now, we
really do need to generate all files mentioned in all sessions
accessible from the ROOTS file, and all their theories, before we can
open Isabelle/jEdit on any of our sessions.
The idea in Isabelle2017-RC1 actually is to tolerate session import
errors during startup of the application, and merely present a big
warning dialog. It came out a bit more strict than planned, but you can
try http://isabelle.in.tum.de/repos/isabelle/rev/1af360d1cad2 or wait a
couple of days for Isabelle2017-RC2.
- Before attempting to open Isabelle/jEdit, run a "make" step which
generates all the files for all our sessions. While not too
inconvenient, it's distasteful that we would need to generate
preprocessed kernel sources for a session near the top of our hierarchy,
just to work on our library sessions at the leaves.
You could also try to generate empty templates first.
On the whole, session-qualified imports seem to be a very positive
change.
However, at least from the perspective of a user, they seem
unrelated to the
problem we're facing here.
The full exploration of the session name space by Isabelle/jEdit is
required to map file names to logical theory names. Without that you
cannot refer to session-qualified theories.
Makarius
Email Gateway (Aug 22 2022 at 16:02):From: Matthew.Brecknell@data61.csiro.au
On Tue, 2017-09-05 at 14:41 +0200, Makarius wrote:
The idea in Isabelle2017-RC1 actually is to tolerate session import
errors during startup of the application, and merely present a big
warning dialog. It came out a bit more strict than planned, but you can
try http://isabelle.in.tum.de/repos/isabelle/rev/1af360d1cad2 or wait a
couple of days for Isabelle2017-RC2.
I've tried 1af360d1cad2, and confirm that it resolves our problem.
Your reply to Florian Haftmann in the thread "Qualified theory imports and
isabelle jedit -l … -R …" now also makes sense to me.
The full exploration of the session name space by Isabelle/jEdit is
required to map file names to logical theory names. Without that you
cannot refer to session-qualified theories.
Fair enough, although it's still not clear to me why it's necessary, or even
desirable, to do this full exploration eagerly at Isabelle/jEdit startup.
Although it would be more fiddly to arrange for the exploration to be done
on demand, surely it is at least possible?
Anyway, thanks for helping us out of this problem!
Matthew
Last updated: Apr 23 2024 at 20:15 UTC