Re: [isabelle] AFP instructions



On 27/02/2021 10:28, Stepan Holub wrote:
> Dear Gerwin,
> 
> thank you. I believe that the current form is much clearer, almost as clear as
> needed.

... and still wrong. The text now says:

"""
 For Windows, the idea is the same just the path is slightly different. If the
AFP is in C:\afp, you should be able to run the following in a Cygwin terminal.

    echo "/cygdrive/c/afp/thys" >> ~/.isabelle/Isabelle2021/ROOTS
"""

but there are 2 paths in the command-line, and both deviate from Linux.


Concerning "a Cygwin" terminal: it has an underlying Cygwin installation and
each has its own idea of "~" within its root file-system.

In contrast, Isabelle expands "~" to $USER_HOME, which should be normally the
Windows user home directory.


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

Yes, and that "other" way should be Isabelle/jEdit: it tries its best to
provide a uniform cross-platform view that always works.


Gerwin wrote:
>> 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.

I usually don't even know myself what $ISABELLE_HOME and $ISABELLE_HOME_USER
refer to on an arbitrary Isabelle installations.

This is why I added convenient "Favorites" to the Isabelle/jEdit file-dialog
some years ago: it tells explicitly what the expanded form of the directory is
(in native path notation understandable by every Windows user).


Yet another proposal to approximate instructions that actually work:

  * Use "isabelle -u MY_RELATIVE_PATH_TO_AFP" to register the main AFP
directory as Isabelle component (there is also "isabelle -x ..." to remove it.
(These operations are idempotent.)

  * Use command-line options "isabelle build -d '$AFP' ..." or "isabelle jedit
-d '$AFP' ..."

  * Or make this persistent by adding $AFP literally as a line in
$ISABELLE_HOME_USER/ROOTS (I never do that myself).


For Windows everything shoukd be done in the Cygwin-Terminal from the Isabelle
distribution, for reproducible results.


	Makarius




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