Re: [isabelle] AFP instructions

["Fernandez, Matthew" <matthew.fernandez at intel.com>]

> -----Original Message-----
> From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-
> bounces at lists.cam.ac.uk> On Behalf Of Gerwin Klein
> Sent: Wednesday, February 24, 2021 14:14
> To: Makarius <makarius at sketis.net>
> Cc: Stepan Holub <holub at karlin.mff.cuni.cz>; isabelle-users <cl-isabelle-
> users at lists.cam.ac.uk>
> Subject: Re: [isabelle] AFP instructions
> 
> 
> 
> > On 25 Feb 2021, at 05:38, Makarius <makarius at sketis.net> 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 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?

Not sure I've got the exact meaning of your question right, but here are some Windows 10 results:

  Command Prompt (cmd.exe):
    $ echo "hello world" >> ~/foo-cmd.txt
    The system cannot find the path specified.

  PowerShell:
    $ echo "hello world" >> ~/foo-pwsh.txt
    $ type C:\Users\mfernan2\foo-pwsh.txt
    hello world

  Cygwin64 Terminal:
    $ echo "hello world" >> ~/foo-cygwin.txt
    $ cat /home/mfernan2/foo-cygwin.txt
    hello world

  Git Bash (for completeness/curiosity):
    $ echo "hello world" >> ~/foo-gbash.txt
    $ cat /c/Users/mfernan2/foo-gbash.txt
    hello world

Even if you can get the CMD version to work, "hello world" comes out including the surrounding quote characters.