Email Gateway (Aug 22 2022 at 16:06): Email Gateway (Aug 22 2022 at 16:06):From: Peter Lammich <lammich@in.tum.de>
Hi,
While porting some of my theories, I was stopped by this:
theory Scratch imports
"$AFP/Show/Show"
begin
The theory panel indicates an error in Show, and when investigating, it
is the following:
theory Show
imports
Main
Deriving.Generator_Aux
Deriving.Derive_Manager
begin
*** Bad theory import "Deriving.Generator_Aux"
What is going on here, and how can I use AFP-entries without setting up
a base-image for them?
Cheers,
Peter
p.s. Isabelle107/RC2 with $AFP pointing to dfb6f8bc70e3 as indicated in
the RC2 release email
Email Gateway (Aug 22 2022 at 16:06):From: Peter Lammich <lammich@in.tum.de>
Update:
I could use
isabelle jedit -d '$AFP"
from the command line to bring up an Isabelle that understands the
long import name.
Is this the intended/correct approach?
If yes, shouldn't this setting be done by the AFP component itself?
Email Gateway (Aug 22 2022 at 16:06):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Indeed, since now the AFP-ROOTS-file is mandatory for building, it
sounds reasonable to put the ROOTS-file into the AFP-component.
Cheers,
René
PS: alternatively to the “-d $AFP”,
you can add your own .isabelle/Isabelle2017-RC2/ROOTS file and
enter the path to the AFP at that point.
Email Gateway (Aug 22 2022 at 16:06):From: Peter Lammich <lammich@in.tum.de>
It still seems a bit odd to me importing the theory by "$AFP/xxx", as this is
an old- style by path import, making the imported file belonging to the
importing session, etc ...
Peter
Email Gateway (Aug 22 2022 at 16:06):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
It still seems a bit odd to me importing the theory by "$AFP/xxx", as this is an old- style by path import, making the imported file belonging to the importing session, etc …
Indeed, but why do you do that at all?
For instance, with AFP in the ROOTS file, and starting Isabelle via “isabelle jedit”
theory Scratch
imports
Show.Show
begin
works perfectly fine without any path-, but session-qualifier “Show.” instead.
I’m not sure whether I completely understood where your problem is.
Cheers,
René
Email Gateway (Aug 22 2022 at 16:06):From: Peter Lammich <lammich@in.tum.de>
I only wanted to figure out what the preferred way of using AFP entries is in
2017. So far, I have found out from this thread:
Put a reference to AFP somewhere to your user- local config (ROOTS file, -d
option), and then use session names in the import.
So is there any advantage in having AFP installed as a component, or is the
component concept just superseded by session qualified imports?
Perhaps the answer may be implied by this question:
Moreover, how do I refer to AFP in portable projects? Can I put $AFP into the
ROOTS file of my project? Or is there a better/more standard way?
Peter
Email Gateway (Aug 22 2022 at 16:06):From: Lars Hupel <hupel@in.tum.de>
Indeed, since now the AFP-ROOTS-file is mandatory for building, it
sounds reasonable to put the ROOTS-file into the AFP-component.
This has already been discussed, with the connclusion being that it's
not such a good idea:
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-August/msg00052.html>.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:07):From: Makarius <makarius@sketis.net>
On 15/09/17 12:14, Peter Lammich wrote:
I only wanted to figure out what the preferred way of using AFP entries
is in 2017. So far, I have found out from this thread:Put a reference to AFP somewhere to your user- local config (ROOTS file,
-d option), and then use session names in the import.So is there any advantage in having AFP installed as a component, or is
the component concept just superseded by session qualified imports?
The AFP component has two main purposes:
- provide $AFP_BASE and $AFP which are occasionally useful
- provide administrative tools and settings
None of this is strictly necessary for using AFP with session-qualified
theory names, which are already the default for Isabelle2017-RC2 everywhere.
So there is no need to init the AFP component. It is sufficient to
activate the AFP directory formally, e.g. by the actual directory name
without any variables in $ISABELLE_HOME_USER/ROOTS.
Moreover, how do I refer to AFP in portable projects? Can I put $AFP
into the ROOTS file of my project? Or is there a better/more standard way?
I've seen IsaFoR including $AFP in ROOTS. But this only works exactly
once for a tree of project directories.
There is presently no standard way to specify such "project
dependencies" permanently. The official approach is to tell users that
they should have certain directories in ROOTS.
Makarius
Last updated: Apr 30 2024 at 01:06 UTC