Re: [isabelle] AFP instructions



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?

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.

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


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

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


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


> Also, the quotation marks are no more needed for the import, right?

Quotes are needed for non-identifiers in the session-qualified name. By
historical accident, we have a lot of session names like "HOL-Library". I
would rather like to see proper identifiers everywhere, but this would cause a
lot of extra trouble.


	Makarius




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