Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] The instructions in AFP's "Using Entries" do n...

view this post on Zulip Email Gateway (May 26 2021 at 14:51):

From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,

at the Isabelle Zulip, we have just successfully troubleshot an issue
with getting Isabelle to recognize AFP component. As it turns out, the
path that should be included in $ISABELLE_HOME_USER/etc/components
(which is, by the way, incorrectly referred to by isabelle components --help
as $ISABELLE_HOME_USER/components, without the /etc/ path component),
is .../afp-2021-05-14/thys, and not just .../afp-2021-05-14.
Moreover, isabelle components -u will only accept the former,
rejecting the latter with

*** Bad component directory: "/home/kuba/formal/afp-2021-05-14/thys"

Manually editing $ISABELLE_HOME_USER/etc/components to include the path
to .../thys makes things work.

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (May 26 2021 at 23:28):

From: Gerwin Klein <kleing@unsw.edu.au>
Hi Jakub,

Thanks for helping out with that, I just looked at the Tulip discussion.

It seems like the component registration does work, but the AFP component does not make the AFP thys directory globally available.

After the instructions as they are, isabelle afp_build Example-Submission should work, but isabelle jedit alone will not pick them up.

IIRC we removed the global ROOTS from the component at some point, because including a ROOTS file twice led to problems. That is no longer the case, so including ROOTS again is probably the simplest solution.

The other lesson from the zulip discussion is that we should not assume that Isabelle is installed in the path. I remember now that I specifically avoided that in the old version of the instructions, but that had its own problems.

Cheers,
Gerwin

view this post on Zulip Email Gateway (Jun 05 2021 at 19:18):

From: Makarius <makarius@sketis.net>
As a "proof" for the formal record, here is the public archive of the Zulip
thread in question:
https://isabelle.systems/zulip-archive/238552BeginnerQuestions/77272afp.html

Already in 1990, I have resolved to ignore the real-time chat culture, so it
is indeed important to copy topics that might be relevant over to the official
mailing list.

First some minor notes, especially on the idealized situation for the next
release:

I will answer Gerwin's answer separately, especially for Isabelle2021 without
any of these changes.

Makarius

view this post on Zulip Email Gateway (Jun 05 2021 at 20:00):

From: Makarius <makarius@sketis.net>
We can be glad that the Isabelle + AFP repositories don't have Orwellian
manipulation of history
https://www.sparknotes.com/lit/1984/quotes/theme/manipulation-of-history ---
so it is easy to look up things formally when memory becomes unsure.

The initial AFP/etc/settings go back to Florian Haftmann in Aug-2011, where he
introduced $AFP_BASE for the main AFP directory and $AFP for AFP/thys. See also:

https://isabelle-dev.sketis.net/source/afp-devel/history/default/etc/settings

changeset: 2357:5b970f669325
user: haftmann
date: Tue Aug 30 23:36:37 2011 +0200
files: etc/settings tools/testafp
description:
rudimentary support for AFP as Isabelle component

The isabelle build setup with ROOT / ROOTS is by myself and Gerwin in
Aug/Sep-2012, when "isabelle build" emerged:

changeset: 2994:3fa9ca7f4a5e
user: wenzelm
date: Sun Aug 05 22:01:12 2012 +0200
files: thys/ROOT thys/ROOTS tools/afp_mkroot
description:
more formal ROOTS catalog file;

changeset: 3043:c2985e24d5f7
user: Gerwin Klein <gerwin.klein@nicta.com.au>
date: Sun Sep 02 15:15:04 2012 +1000
files: admin/regression
description:
include ROOTS file to actually build something

changeset: 11860:6d986a7dc22b
user: Gerwin Klein <kleing@unsw.edu.au>
date: Thu May 27 10:07:17 2021 +1000
files: ROOTS
description:
make AFP ROOTS globally available for component

My initial change 3fa9ca7f4a5e is where the thys/ROOTS file appears first. We
never had a ROOTS in the main AFP directory, not by accident but by design.
This was due to my re-interpretation of Florian's $AFP_BASE and $AFP settings
as follows:

* $AFP_BASE is the administrative base directory of AFP, providing settings,
isabelle command-line tools etc.

* $AFP is a symbolic handle on the actual session directories, with ROOTS as
overall catalog, and subdirectories with individual ROOT files.

By initializing only $AFP_BASE as component, but not yet $AFP, it is possible
to refer to AFP sessions symbolically on demand: the session name space
remains clear of AFP entries by default.

This is important for build management of Isabelle and AFP separately:

isabelle build -a # build all of Isabelle, without AFP

isabelle build -a -d '$AFP' # build all of Isabelle + AFP

isabelle build -D '$AFP' # build all of AFP, but only those images of
Isabelle that are required for it

The option -d '$AFP' has later become idiomatic for many other Isabelle tools,
to add the "AFP aspect" with minimal complexity. For example for the Prover IDE:

isabelle jedit -d '$AFP'

or relatives of "isabelle build" that require formal sessions, like "isabelle
export", "isabelle document" etc.

This well-understood and important behaviour of $AFP_BASE vs. $AFP has been
lost by the following "quick-fix" that has emerged from this thread:

changeset: 11677:6d986a7dc22b
user: Gerwin Klein <kleing@unsw.edu.au>
date: Thu May 27 10:07:17 2021 +1000
files: ROOTS
description:
make AFP ROOTS globally available for component

Note that I have already improved my "isabelle components -u" for the next
Isabelle release, to avoid such confusion in the future.

For Isabelle2021 + AFP, there are at least two possibilities, without the
deadly $AFP_BASE/ROOTS catalog:

(1) Just create AFP/thys/etc/settings as a dummy, to make it look like a
component directory for Isabelle2021/bin/isabelle components -u.

(2) Be more ambitious in having the AFP/thys/etc/settings initialize
$AFP_BASE if not yet done by the user. Thus users get two choices for AFP as
component:

(a) use component AFP, but not AFP/thys; thus the important "isabelle
build -a" versus "isabelle build -a -d '$AFP'" works properly

(b) use component AFP/thys and let its etc/settings init AFP if required
(otherwise users would have to init both AFP and AFP/thys manually).

This is a long explanation for a small change, see the attachment for afp-2021
(and merge into afp-devel).

It would be better to have fewer choices and less complexity: ultimately no
Isabelle/AFP user should be asked to tinker with component configuration: the
Prover IDE should just do it in a prospective "AFP" panel.

This will emerge eventually, but not in the next release (end of 2021).

Makarius
ch

view this post on Zulip Email Gateway (Jun 06 2021 at 00:36):

From: Gerwin Klein <kleing@unsw.edu.au>

On 6 Jun 2021, at 06:00, Makarius <makarius@sketis.net> wrote:

The initial AFP/etc/settings go back to Florian Haftmann in Aug-2011, where he
introduced $AFP_BASE for the main AFP directory and $AFP for AFP/thys. See also:
[..]

I agree with all of this.

This is important for build management of Isabelle and AFP separately:

isabelle build -a # build all of Isabelle, without AFP

True, I had not anticipated that isabelle build -a is called in contexts where the AFP is registered as component. You'd now have to explicitly exclude the afp group, and that is not very nice.

The option -d '$AFP' has later become idiomatic for many other Isabelle tools,
to add the "AFP aspect" with minimal complexity. For example for the Prover IDE:

isabelle jedit -d '$AFP'

Agree, that was the canonical way, but that was part of the problem. It doesn't work for users who don't use the command line.

We had discussions amongst the editors before about having AFP ROOTS available by default -- this what I was referring to about the ROOTS file. You can't find them in the history, because it didn't work when we discussed it, so it was never committed.

[..]

For Isabelle2021 + AFP, there are at least two possibilities, without the
deadly $AFP_BASE/ROOTS catalog:
[..]
(2) Be more ambitious in having the AFP/thys/etc/settings initialize
$AFP_BASE if not yet done by the user. Thus users get two choices for AFP as
component:

(a) use component AFP, but not AFP/thys; thus the important "isabelle
build -a" versus "isabelle build -a -d '$AFP'" works properly

(b) use component AFP/thys and let its etc/settings init AFP if required
(otherwise users would have to init both AFP and AFP/thys manually).

This is much better than my solution, and I'd be very happy with it.

This is a long explanation for a small change, see the attachment for afp-2021
(and merge into afp-devel).

Thanks for that, I'll include it and update the instruction (again ;-))

Cheers,
Gerwin

view this post on Zulip Email Gateway (Jun 06 2021 at 10:19):

From: Makarius <makarius@sketis.net>
Yes, I am aware of that extra assumption. It is part of the process to rethink
AFP within the Prover IDE.

There is another ongoing process of rethinking: how to allow Isabelle/Scala
modules within sessions and/or components.

Maybe I eventually get the right idea, when revisiting this more seriously.

Makarius

view this post on Zulip Email Gateway (Jun 06 2021 at 10:23):

From: Makarius <makarius@sketis.net>
Great.

I now see change 3a9c2004b599 both on afp-2021 and afp-devel.

Makarius

view this post on Zulip Email Gateway (Jun 07 2021 at 09:24):

From: Gerwin Klein <kleing@unsw.edu.au>
Integrating the AFP more will probably be the better way long-term, yes.

Cheers,
Gerwin

Last updated: Apr 20 2024 at 04:19 UTC