Re: [isabelle] AFP instructions
thank you. I believe that the current form is much clearer, almost as
clear as needed.
That said, one more remark about what the "echo" advice is worth of. If
an inexperienced user makes a typo in the path (like
"/home/myself/afp/thy" instead of "/home/myself/afp/thys") when first
trying to use the suggested command, he or she is in quite a big
And then (at the latest) he or she has to figure out what "~" means (on
Windows something like "C:\Users\USERNAME") and edit the file anyway in
some other way. And this (again from my embarrassing point of view) is
far from trivial piece of information.
On 25 Feb 2021, at 22:25, Makarius <makarius at sketis.net> wrote:
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
I do appreciate that (and use it myself), but for the instructions it doesn't work: if, as a user, you don't know what $ISABELLE_USER_HOME refers to, you will not know which file to change, or how to adjust the path if you have put the AFP in a different location to what the instructions expect. If you have the concrete example, you have more information.
Tento e-mail byl zkontrolován na viry programem AVG.
This archive was generated by a fusion of
Pipermail (Mailman edition) and