Email Gateway (Aug 22 2022 at 15:54): Email Gateway (Aug 22 2022 at 15:54):From: Matthew.Brecknell@data61.csiro.au
Hi Makarius,
I've run into the first hurdle updating the l4-verified proofs for Isabelle2017-RC0.
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 use isabelle jedit -d to 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.
Otherwise, I get errors like this, with a corresponding error dialog:
$ isabelle jedit -d .
4:00:38 PM [main] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin
4:00:38 PM [main] [error] PluginJAR: *** No such file: "/home/matthewb/verification/isa2017/l4v/spec/machine/ARM/MachineTypes.thy"
4:00:38 PM [main] [error] PluginJAR: *** The error(s) above occurred for theory "CKernel.MachineTypes"
4:00:38 PM [main] [error] PluginJAR: *** (required by "CKernel.Kernel_C") (line 13 of "/home/matthewb/verification/isa2017/l4v/spec/cspec/ARM/Kernel_C.thy")
4:00:38 PM [main] [error] PluginJAR: *** The error(s) above occurred in session "CKernel" (line 84 of "/home/matthewb/verification/isa2017/l4v/spec/ROOT")
<snip>
4:00:38 PM [main] [error] PluginJAR: at isabelle.Sessions$.deps(sessions.scala:144)
4:00:38 PM [main] [error] PluginJAR: at isabelle.Sessions$.session_base(sessions.scala:280)
4:00:38 PM [main] [error] PluginJAR: at isabelle.jedit.JEdit_Sessions$.session_base(jedit_sessions.scala:59)
4:00:38 PM [main] [error] PluginJAR: at isabelle.jedit.Plugin.init_resources(plugin.scala:74)
4:00:38 PM [main] [error] PluginJAR: at isabelle.jedit.Plugin.start(plugin.scala:415)
4:00:38 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.startPlugin(PluginJAR.java:1740)
4:00:38 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:951)
4:00:38 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:1021)
4:00:38 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.jEdit.main(jEdit.java:550)
<snip>
4:00:38 PM [main] [error] PluginJAR: at isabelle.Main.main(main.scala)
4:00:38 PM [main] [error] ErrorListDialog$ErrorEntry: /home/matthewb/verification/isa2017/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
4:00:38 PM [main] [error] ErrorListDialog$ErrorEntry: Cannot start:
4:00:38 PM [main] [error] ErrorListDialog$ErrorEntry: *** No such file: "/home/matthewb/verification/isa2017/l4v/spec/machine/ARM/MachineTypes.thy"
4:00:38 PM [main] [error] ErrorListDialog$ErrorEntry: *** The error(s) above occurred for theory "CKernel.MachineTypes"
4:00:38 PM [main] [error] ErrorListDialog$ErrorEntry: *** (required by "CKernel.Kernel_C") (line 13 of "/home/matthewb/verification/isa2017/l4v/spec/cspec/ARM/Kernel_C.thy")
4:00:38 PM [main] [error] ErrorListDialog$ErrorEntry: *** The error(s) above occurred in session "CKernel" (line 84 of "/home/matthewb/verification/isa2017/l4v/spec/ROOT")
Can this requirement be relaxed again, so that I only need the files for the session I want to load?
Regards,
Matthew
Email Gateway (Aug 22 2022 at 15:54):From: Makarius <makarius@sketis.net>
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 use
isabelle 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:
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.
Makarius
Email Gateway (Aug 22 2022 at 15:54):From: Lars Hupel <hupel@in.tum.de>
Dear Matthew, Makarius,
I'd like to add another (tangential) observation to this thread.
Previously, when editing some theories in the AFP, it was sufficient to
just open Isabelle/jEdit – no special command line flags required
(assuming HOL as a base image). To ensure this, AFP policy states that
imports from other entries should be relative (i.e.
"../Other_Entry/Thy") instead of absolute (i.e. "$AFP/Other_Entry/Thy").
While I appreciate the sentiment behind qualified imports (no more
incoherent imports!), this workflow doesn't work anymore. It is
necessary to start Isabelle/jEdit from the command line as follows:
isabelle jedit -d 'path/to/afp/thys' ...
Even if the AFP is registered as a component, this is still necessary.
While components are automatically registered as session roots, the AFP
base directory is not a session root.
I'd like to make a suggestion to mitigate this situation: make the AFP
base directory a session root, by adding a "ROOTS" file pointing to
"thys" [0]. This might come with a performance penalty because on every
tool invocation, Isabelle/Scala has to traverse the sessions graph.
Makarius might be able to estimate that penalty.
Maybe there is also another way to include session roots.
Cheers
Lars
[0] This is basically the approach I took in
<https://github.com/larsrh/afp>.
Email Gateway (Aug 22 2022 at 15:54):From: Makarius <makarius@sketis.net>
On 22/08/17 12:15, Lars Hupel wrote:
Previously, when editing some theories in the AFP, it was sufficient to
just open Isabelle/jEdit – no special command line flags required
(assuming HOL as a base image). To ensure this, AFP policy states that
imports from other entries should be relative (i.e.
"../Other_Entry/Thy") instead of absolute (i.e. "$AFP/Other_Entry/Thy").
This actually needs to be updated for Isabelle2017:
* Users of AFP need to formally provide its session name space to
Isabelle tools, e.g. via "isabelle build -d 'path/to/afp/thys'" or
"isabelle jedit -d 'path/to/afp/thys'" or by adding a line with
"path/to/afp/thys" to $ISABELLE_HOME_USER/ROOTS to make this persistent.
* Imports of theories from other sessions should always use the formal
session-qualified name, e.g. "HOL-Library.AList" or
"Coinductive.Coinductive_List". This requires to specify the other
sessions as parent or as imported 'sessions' in ROOT.
* The command-line tool "isabelle imports -U -d ... My_Session" helps
to standardize imports in .thy and ROOT files in this respect.
While I appreciate the sentiment behind qualified imports (no more
incoherent imports!), this workflow doesn't work anymore. It is
necessary to start Isabelle/jEdit from the command line as follows:isabelle jedit -d 'path/to/afp/thys' ...
It is possible to use option -d, and there are other ways.
Maybe we should advertize $ISABELLE_HOME_USER/ROOTS to users more
prominently. At some point the Prover IDE might provide an editor for
that: at the moment it just means to open that text file directly using
the above symbolic name (maybe I should add a menu item for that).
Even if the AFP is registered as a component, this is still necessary.
While components are automatically registered as session roots, the AFP
base directory is not a session root.
The component has de-facto no relevance to AFP users. It merely contains
various administrative settings and tools that have accumulated over
time, without a specific plan behind it.
I am using the component myself only to get a symbolic handle $AFP for
various command-line invocations like "isabelle build -d '$AFP' -a" to
build Isabelle + AFP as a whole.
I'd like to make a suggestion to mitigate this situation: make the AFP
base directory a session root, by adding a "ROOTS" file pointing to
"thys" [0]. This might come with a performance penalty because on every
tool invocation, Isabelle/Scala has to traverse the sessions graph.
Makarius might be able to estimate that penalty.
Performance is one problem, and polluting the logical session name space
another (i.e. the important option "-a" becomes hardly usable).
Since the component is not required to refer to path/to/afp/thys, it can
be ignored for this purpose (and maybe not even advertized to users
anymore).
Makarius
Email Gateway (Aug 22 2022 at 15:54):From: Lars Hupel <hupel@in.tum.de>
Maybe we should advertize $ISABELLE_HOME_USER/ROOTS to users more
prominently. At some point the Prover IDE might provide an editor for
that: at the moment it just means to open that text file directly using
the above symbolic name (maybe I should add a menu item for that).
Alternatively, another possibility could be to provide an Isabelle tool
and/or jEdit action to do it automatically. It could be as simple as
isabelle add_root /path/to/afp
... and/or a corresponding action in jEdit. I posit that that could be
useful to many users. Using the AFP is a disruption to the otherwise
quite nice workflow of "extract Isabelle and it just works".
Performance is one problem, and polluting the logical session name space
another (i.e. the important option "-a" becomes hardly usable).
Is the latter really a problem? I thought this is what session groups
are for, i.e. "build -g afp" instead of "build -D $AFP".
But surely adding the AFP to "$ISABELLE_HOME_USER/ROOTS" would also give
these drawbacks.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:55):From: Matthew.Brecknell@data61.csiro.au
Right, thanks. I had seen this, but misunderstood its purpose. I see
now that it should allow us to proceed with updating our proofs for
Isabelle2017, independently of any examination of our build process.
Regards,
Matthew
Email Gateway (Aug 22 2022 at 15:55):From: Makarius <makarius@sketis.net>
Not quite. The session groups are more like "tags" that mark certain
aspects of sessions. Directory structure is more rigid than that
(structurally more reliable for exhaustive testing).
In recent years, I have increasingly understood directories (with their
internal wiring of ROOTS and ROOT files) for composition of big
projects, via options like -d or -D or entries in $ISABELLE_HOME_USERS/ROOTS
This explains the general direction of the system implementation in the
past 5 years.
Makarius
Email Gateway (Aug 22 2022 at 16:07):From: Makarius <makarius@sketis.net>
I've tried with a menu, i.e. "Favorites" in the jEdit file dialog, but
it did not work for $ISABELLE_HOME_USER/ROOTS as plain file, as opposed
to the existing $ISABELLE_HOME_USER for the directory.
So users need to be directed to that important file by other means.
Note that the Isabelle/jEdit startup sequence already generates a
template for the file if it does not exists yet (see Isabelle/6e35cf3ce869).
Makarius
Last updated: Apr 23 2024 at 16:19 UTC