Re: [isabelle] AFP instructions

Dear Gerwin,

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 trouble, right? 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> 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 MHonArc.