Re: [isabelle] AFP instructions



> On 26 Feb 2021, at 08:41, David Cock <david.cock at inf.ethz.ch> wrote:
> 
> 
>>>> So unless users like me are not supposed to use AFP, the instruction is
>>> useless for them.
>>> 
>>> Absolutely happy to add the Windows example now that I know what it should be.
>> Maybe I'm just an uncivilized fool, but what is wrong with a unified prose "append /home/myself/afp/thys to the contents of ~/.isabelle/Isabelle2021/ROOTS" instructions? Won't *nix wizards be able to figure out the echo command themselves if need be?
>> 
> Or even have both?  I hear bits are fairly cheap these days.

We did have that other version before (people complained about it, so we have this now), and yes, both is what I'm planning to do. 

It is absolutely amazing how hard this bit of instruction seems to be. It's a perfect example of "completely trivial when you know and very hard if you don't".

Definitely looking forward to the more direct integration Makarius mentioned.

Cheers,
Gerwin





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