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




> On 6 Jun 2021, at 06:00, Makarius <makarius at 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





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