[isabelle] Isabelle2017-RC0: jEdit plugin insists all files for all sessions are present



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.