Re: [isabelle] The instructions in AFP's "Using Entries" do not work



On 27/05/2021 01:27, Gerwin Klein wrote:
> 
> 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.

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 at 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 at 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 at 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
# HG changeset patch
# User wenzelm
# Date 1622918699 -7200
#      Sat Jun 05 20:44:59 2021 +0200
# Node ID 3a9c2004b599423dd7c3e90e8034fdebc5d5edee
# Parent  9f1d39da07c28f12b5bacc93c9c7362ca783d17f
more robust component setup for AFP/thys: support "isabelle components -u" and init $AFP_BASE on demand;
no ROOTS in $AFP_BASE: proper support for "isabelle build -a" with $AFP_BASE component, but without $AFP component;

diff -r 9f1d39da07c2 -r 3a9c2004b599 ROOTS
--- a/ROOTS	Mon May 31 20:30:44 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-thys
\ No newline at end of file
diff -r 9f1d39da07c2 -r 3a9c2004b599 thys/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/etc/settings	Sat Jun 05 20:44:59 2021 +0200
@@ -0,0 +1,6 @@
+# -*- shell-script -*- :mode=shellscript:
+
+if [ -z "$AFP_BASE" -a -f "$COMPONENT/../etc/settings" ]
+then
+  init_component "$(cd "$COMPONENT"; cd "$(pwd -P)"; cd ..; pwd)"
+fi


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.