Re: [isabelle] AFP instructions




> On 25 Feb 2021, at 05:38, Makarius <makarius at sketis.net> wrote:
> 
> On 24/02/2021 17:40, Stepan Holub wrote:
>> 
>> maybe, the instructions on
>> https://www.isa-afp.org/using.html#1
>> could be made less hostile towards Windows users. The instruction for Windows,
>> to my best knowledge, could be:
>> 
>> If you are using Isabelle2021, and have downloaded your AFP directory to |c:\afp|
>> you should add the line
>> /cygdrive/c/afp/thys
>> to the file
>> C:\Users\YourUserName\.isabelle\Isabelle2021\ROOTS
> 
> 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).

I'm not saying the current version is ideal, but it has been fairly quiet on this topic since we changed it to that. Of course that could also be because everyone is even more confused and is just giving up.


> 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.

Referring to a variable like $ISABELLE_USER_HOME also generated confusion, and esp Windows users are used to a different syntax for these. The hope was that, avoiding any concepts like variable syntax, it is easily recognisable what is going on (which seems to have worked, despite the complaint).

I don't have a Windows machine to test, but I do think it still works if you replace the path with what you need on Windows (as you have to do Linux/Mac as well), i.e. I don't really understand what is hostile to Windows users about it. Maybe all that is missing is adding `/cygdrive/c/afp/thys` as an example inside the `echo` for Windows. Having an extra example for Windows would be fine. Can someone with a Windows machine confirm if the result of that would work? Does `~` exist on Cygwin?


> There is also $ISABELLE_USER_HOME/etc/components to add components.

There are indeed many choices, you could also add something to etc/setting and so on. We wanted to pick one. People who know that there are multiple options don't really need these instructions.


> A remaining problem are the Cygwin paths required for Isabelle:
> /cygdrive/c/afp/thys

That is probably the information that is missing from the page.


> I often place AFP clones right into the corresponding Isabelle directory. Thus
> it could be referenced in a portable manner like this:
> 
>  $ISABELLE_HOME/AFP/thys
> 
> An alternative is to suggest $ISABELLE_HOME_USER

People who know what $ISABELLE_HOME and $ISABELLE_HOME_USER are have read the manual ;-)


> Rather soon the Prover IDE should take care of AFP, that we don't need extra
> explanations any more.

That'd be nice. Basically, either users already know how to add components, because they have read the manual, know the concepts, and understand how to modify their setup, or they are missing one of these sources of information, and just want to use something in the AFP without further research. There is of course a whole spread of experience between those two, but the idea was to have something that needs no further knowledge.

Cheers,
Gerwin



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