Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Qualified theory imports and isabelle jedit -l...

Email Gateway (Aug 22 2022 at 15:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,

when inspecting a »broken« session (let as assume, HOL-Number_Theory), I
used to invoke

isabelle jedit -l HOL-Number_Theory -R ../Number_Theory/Number_Theory.thy

and everything worked out smoothly.

With qualified theory imports emerged in future Isabelle2017, this is no
longer the case: theory »Residues« chokes on imports from HOL-Algebra.

Inspecting the corresponding session entry in src/HOL/ROOT:

session "HOL-Number_Theory" (timing) in Number_Theory = "HOL-Computational_Algebra" +
…
sessions
"HOL-Algebra"
…

it seems to be the case that -R operates on the direct ancestor session
HOL-Computational_Algebra but not on the »side path« HOL-Algebra.

Is that intended? I have the feeling that the current behaviour would
diminish the usability of -R considerably.

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 16:06):

From: Makarius <makarius@sketis.net>
This is indeed a bit strange. I have reverted this double interpretation
of "isabelle jedit -R" already (see Isabelle/e16b27bd3f76). So its
meaning is just this (see NEWS):

• Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
  entry of the specified logic session in the editor, while its parent is
  used for formal checking.

Errors in the exploration of dependencies are now merely shown as
warning on startup of the Prover IDE, so there is no special need for a
separate option to bypass that.

Makarius
signature.asc

Last updated: Apr 30 2024 at 04:19 UTC