Email Gateway (Aug 22 2022 at 13:17): Email Gateway (Aug 22 2022 at 13:17):From: Makarius <makarius@sketis.net>
Certain reforms about locating theory sources via the formal session
structure have been in the pipeline for several years. I hope to get
that through before every release, and still do hope so for the one in
autumn 2016.
The general principle is that theories are no longer addressed via
file-system locations, but by logical names that stem from the
collective session definitions that are presently active. The main
mechanism to vary that session context is what you see as option -d in
"isabelle build" or "isabelle jedit", or the "dirs" in Isabelle/Scala
interfaces.
Lets see what comes out of that, when we are finally standing there.
Stay tuned and keep an eye on isabelle-dev ...
Makarius
Email Gateway (Aug 22 2022 at 13:24):From: Joachim Breitner <breitner@kit.edu>
Dear list,
I have a few entries in the AFP. These did not originate in the AFP:
They were developed outside, referencing the AFP using "$AFP/Foo/Bar",
as suggested in http://www.isa-afp.org/using.shtml
But when submitting them to the AFP, I have to change that to
"../Foo/Bar". From then on, when I want to merge changes from my
working repository to the AFP and back, I have to keep changing that.
An alternative would be to develop in the AFP repository, but that
feels quite wrong.
Another alternative is to add symbolic links to the used AFP entries to
the directory above my current project. This works, but is also not
nice, as it clutters my "projects" directory.
So I wonder: Is it not possible to device a way that allows the same
theories to work inside the AFP and outside? Why is it that within the
AFP, $AFP cannot be set appropriately (to ".." if you want)?
The reason for .. mentioned above is that "it interacts correctly with
multiple AFP installations side by side". But would setting AFP=.., if
one has to work with multiple installations, not do the same?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 13:24):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
So I wonder: Is it not possible to device a way that allows the same
theories to work inside the AFP and outside? Why is it that within the
AFP, $AFP cannot be set appropriately (to ".." if you want)?
Yes: you place the other AFP entries next to yours in the local directory structure, such that “../Entry/theory” refers to the correct theory.
This is indeed restrictive, because it determines your directory layout (some programming languages force that in any case), but once submitted to the AFP it is probably a good idea to at least keep it in its own isolated directory anyway, and having it organised such that AFP dependencies live next to it does make a certain sense.
I.e. something along the lines of
my-repo/
other-things/
AFP-things/
my-entry/
other-entry1/
other-entry2/
Of course, AFP-things/ could be the root level or anywhere else in your structure, and there could be non-AFP things underneath it as well - this is just an example.
The reason for .. mentioned above is that "it interacts correctly with
multiple AFP installations side by side". But would setting AFP=.., if
one has to work with multiple installations, not do the same?
Unfortunately not. $AFP is set as part of the component setup in the AFP itself - so whichever AFP installation you mention last in the component initialisation setup will be the one $AFP refers to.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 13:24):From: Lars Hupel <hupel@in.tum.de>
In consequence, this would also mean that AFP couldn't be used without
installing it (i.e. registering as a component).
Email Gateway (Aug 22 2022 at 13:24):From: Lars Hupel <hupel@in.tum.de>
There are mostly technical reasons for this, affecting both users and
the testing infrastructure. Gerwin has already explained the former.
The effect on the testing infrastructure is that building the AFP would
require component setup, which is problematic when paths are not known.
Isabelle would need to be aware of concrete paths of things on the build
servers (which are not constant).
Email Gateway (Aug 22 2022 at 13:24):From: Joachim Breitner <breitner@kit.edu>
Hi,
ok, let me phrase the question differently:
What could and should changed, either in Isabelle or the AFP component
setup, so that it _becomes_ possible to use the theories in both setups
(within the AFP directory structure, as well as stand-alone theories
using the registered AFP component)?
Greetings,
Joachim
signature.asc
Last updated: Apr 26 2024 at 16:20 UTC