Re: [isabelle] AFP instructions



Indeed, "strange" was my main point. I have no strong opinion about how to make it more normal.

Stepan

On 24.2.2021 19:38, Makarius 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?

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.