Email Gateway (Aug 22 2022 at 17:45): Email Gateway (Aug 22 2022 at 17:45):From: Dominique Unruh <unruh@ut.ee>
Hi,
I am trying to understand the intended use of the new -A option to isabelle
jedit.
As far as I understand, the use case for -R XXX is to open jEdit with a
heap that contains already all theories that will be needed while editing
theories in XXX. (Specifically, that means that theories in XXX itself are
not prebuilt.)
Additionally there is the -A option. My first thought was that this is to
be used in the following situation: I have a more complex project
involving, say, two sessions XXX=HOL+... and YYY=XXX+... Without -R,-A,
I would have to run *jedit -l HOL *to be able edit theories in both
sessions. With jedit -R XXX, the theories from other sessions in YYY
would not be prebuilt. With jedit -R YYY, the theories from XXX would be
prebuilt and therefore cannot be edited. So I thought that is what *jedit
-R YYY -A XXX* would be for. I had expected/hoped that this would not build
the theories in sessions XXX and YYY, only the theories from other
sessions. Unfortunately, this is not what -A does, the sessions from XXX
are still prebuilt (it just changes where in the session graph they are
included).
What is the intended use case of -A? And is there a combination of
options that achieves what I had thought it was for (i.e., not prebuild any
theories from XXX and YYY, but all included theories from other sessions)?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:45):From: Makarius <makarius@sketis.net>
On 06/07/18 15:58, Dominique Unruh wrote:
I am trying to understand the intended use of the new -A option to isabelle
jedit.
It merely defines the starting point for building the auxiliary image
for options -R and -S. This sometimes helps to make it work more
smoothly, e.g. as follows.
(1) Using a rather small ancestor like HOL, instead of the endpoint of
a bigger stack like HOL, HOL-Library, HOL-Computational_Algebra,
HOL-Algebra, HOL-Number_Theory.
(2) Using a rather big ancestor to have more background material than
required, e.g. HOL-Analysis, HOL-Probability.
You can see option -A also as fine-tuning of occasionally convoluted
stacks seen in AFP: it contains more hardwired complexity than
necessary. Somehow people like to publish their private development
artifacts.
In the medium term, I would like to see a session image become merely
like a "cache" for ongoing work. E.g. there could be one image for the
Prover IDE, which contains whatever you have visited interactively. On
application shutdown it will be stored, on restart it will be reloaded.
The idea of session images as "build artifact" is a bit of a conceptual
mismatch: I am myself responsible for this confusion, because I've made
images de-facto read-only some decades ago. Reintroducing writable
images is technically difficult, but possible and definitely desirable.
Additionally there is the -A option. My first thought was that this is to
be used in the following situation: I have a more complex project
involving, say, two sessions XXX=HOL+... and YYY=XXX+...
I am unsure what the situation really is. Just some generic points:
* Do you really need so many intermediate sessions?
* Is it feasible to compose adhoc session definitions in
$ISABELLE_HOME_USER/ROOT for the purpose of certain development situations?
Makarius
Email Gateway (Aug 22 2022 at 17:45):From: Dominique Unruh <unruh@ut.ee>
Thanks for the explanation.
In the medium term, I would like to see a session image become merely
like a "cache" for ongoing work. E.g. there could be one image for the
Prover IDE, which contains whatever you have visited interactively. On
application shutdown it will be stored, on restart it will be reloaded.
The idea of session images as "build artifact" is a bit of a conceptual
mismatch: I am myself responsible for this confusion, because I've made
images de-facto read-only some decades ago. Reintroducing writable
images is technically difficult, but possible and definitely desirable.
Yes, those changes would be really nice I think. :)
I am unsure what the situation really is. Just some generic points:
* Do you really need so many intermediate sessions?
Yes, I don't see a way around it. It is in the context of a tool that uses
Isabelle in the backend (https://github.com/dominique-unruh/qrhl-tool/) via
libisabelle, and the binary distribution would only contain one of the
sessions, but the sources contains other session with, e.g., tests.
* Is it feasible to compose adhoc session definitions in
$ISABELLE_HOME_USER/ROOT for the purpose of certain development situations?
Yes. That is what I have been doing (and what still works with
Isabelle2018).
So there is no big problem, I just had hoped that the new -R,-A switches
would allow me to avoid this.
The disadvantage is that this ROOT needs to be added on every system that I
use, but that's not a big problem.
So if the current switches don't solve that, it's no problem.
I just wanted to check because they seemed to address a similar use case.
Best wishes,
Dominique.
Last updated: Apr 25 2024 at 04:18 UTC