Re: [isabelle] AFP instructions



On 24/02/2021 23:13, Gerwin Klein wrote:
>>
>> I find the instructions a bit strange, even for Linux. Why use "echo" to edit
>> a file --- with a somewhat accidental location ~/.isabelle/Isabelle2021/ROOTS?
> 
> Because instructions for editing a file generated too many questions and failure. (What if it doesn't exist? What if it does exist? Adding it at the end or the beginning or the middle? None of that matters, but all of it generates questions and confusion).

Here are again my points about that special ROOTS file again:

>> In my own documentation, I usually refer symbolically to
>> $ISABELLE_USER_HOME/etc/ROOTS --- this can be used literally in Isabelle/jEdit
>> on all platforms, and the ROOTS file even has inlined explanations for that
>> situation.

Here is the relevant repository reference from 31-Aug-2017 where the main
Isabelle entry point ensures that ROOTS is present:
https://isabelle-dev.sketis.net/rISABELLE6e35cf3ce869


Note that in Isabelle2021 there is even some PIDE support for ROOTS files,
with C-hover-
click on the directory entries.

Neither the 4-5 versions of "echo" nor 2-3 versions of "vi" can do that.


	Makarius




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