Re: [isabelle] AFP instructions
- To: Gerwin Klein <kleing at unsw.edu.au>, Makarius <makarius at sketis.net>
- Subject: Re: [isabelle] AFP instructions
- From: "Fernandez, Matthew" <matthew.fernandez at intel.com>
- Date: Wed, 24 Feb 2021 23:07:16 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=intel.com; dmarc=pass action=none header.from=intel.com; dkim=pass header.d=intel.com; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=X7ZohsA6UeaVSLSy/nvgpT32OhJHG5uKOLewHHBELZs=; b=b6y/vh8pNM9/tglAhmZSiEpUS8MOBHINt7+FhUl70m2hXj+64gjM/Pn8BQmH+oIbrp+/aEX3pVPsZHNvUWScKs/s9D1iFjTMWyilLn4W/XWTbqbExf+yyIbH6BxdS7sGe9TRk5HOVWHB/fsPe45PnJER0/RvjTsAko9L9oHxkOi9P4wpLXJHpPGQUm/6aY+0viUdA8+kwAYzDd1OAaen35nxoUaMsUWbQGP6uMlo3Cj4J4XTrQ54X89V0w9EmnSUQvJDWNVK6W8olrj+f78IAeMOT7A8Kf0qv5JGEYPkOgu4KXZ664UjRqaGgnJpoIKYQSekbdx17qtIIDGj756vlg==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=b/DNAO2J/tloRKfRhUWPmWR0z7fIDNENI7Y7/p2qW3J9tL5V0EIHcUOpdnnSi7CDksLglYpgfqRT9FcyBVZb9lOWqCzRFwCGC8erwQXQ5sej/IVNyxoy8laqNXtkvbbIA5jfYAwtDT3PEg1bPmDefPrXHcw5k0mT9a2kqZCzRDthVqNrmR6UXYQ821UHcg6XgSoKJIshJb8OcecPhvdp822c5Gm4aPhbGL5yhA0huiPOi+DDYzJhFs+NS7YANVTSaN/Slaecjih/4lS3camTtaz+KafOESTIUOx9LIMjgnmAavcfUY8pqoWepYk5JPqIiMNy5k112O6o720KoBoEiQ==
- Authentication-results: unsw.edu.au; dkim=none (message not signed) header.d=none; unsw.edu.au; dmarc=none action=none header.from=intel.com;
- Cc: Stepan Holub <holub at karlin.mff.cuni.cz>, isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.5.1.3
- In-reply-to: <3065423E-F3E2-4FEB-9546-F99214820694@unsw.edu.au>
- Ironport-sdr: 3PeojfyH7bhMDeNr4IR2yoWDBJutZHA3xmcrj7jkK/K3OQij/dIZdMArYhodLgMvm0I9PDLsmE 37noG6FOGvZA==
- Ironport-sdr: x6Ga7MyM45YU1FZGiAxOOdDHnErE40ECf3NyriE6m/ESG4MTrSH1OlhgM5m7bj85phHV3RCbcW Ftfcmi0i0XaQ==
- References: <792413ed-5e82-70a3-9271-74c54d60fad4@karlin.mff.cuni.cz> <9e3de5f0-cac1-4ded-6e16-0a0c94cb0f66@sketis.net> <3065423E-F3E2-4FEB-9546-F99214820694@unsw.edu.au>
- Thread-index: AQHXCsv7oavmc+VpbUSXgMtTmQ7AnqpnosOAgAA8RgCAAAqQcA==
- Thread-topic: [isabelle] AFP instructions
> -----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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.