Email Gateway (Feb 24 2021 at 16:40): Email Gateway (Feb 24 2021 at 16:40):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hello,
concerning the successful launch of AFP2021:
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
Also, the quotation marks are no more needed for the import, right?
Best regards
Stepan
Email Gateway (Feb 24 2021 at 18:38):From: Makarius <makarius@sketis.net>
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
Email Gateway (Feb 24 2021 at 18:47):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Indeed, "strange" was my main point. I have no strong opinion about how
to make it more normal.
Stepan
Email Gateway (Feb 24 2021 at 22:15):From: Gerwin Klein <kleing@unsw.edu.au>
On 25 Feb 2021, at 05:38, Makarius <makarius@sketis.net> 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\ROOTSI find the instructions a bit strange, even for Linux. Why use "echo" to edit
a file --- with a somewhat accidental location ~/.isabelle/Isabelle2021/ROOTS?
Because instructions for editing a file generated too many questions and failure. (What if it doesn't exist? What if it does exist? Adding it at the end or the beginning or the middle? None of that matters, but all of it generates questions and confusion).
I'm not saying the current version is ideal, but it has been fairly quiet on this topic since we changed it to that. Of course that could also be because everyone is even more confused and is just giving up.
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?
There is also $ISABELLE_USER_HOME/etc/components to add components.
There are indeed many choices, you could also add something to etc/setting and so on. We wanted to pick one. People who know that there are multiple options don't really need these instructions.
A remaining problem are the Cygwin paths required for Isabelle:
/cygdrive/c/afp/thys
That is probably the information that is missing from the page.
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
People who know what $ISABELLE_HOME and $ISABELLE_HOME_USER are have read the manual ;-)
Rather soon the Prover IDE should take care of AFP, that we don't need extra
explanations any more.
That'd be nice. Basically, either users already know how to add components, because they have read the manual, know the concepts, and understand how to modify their setup, or they are missing one of these sources of information, and just want to use something in the AFP without further research. There is of course a whole spread of experience between those two, but the idea was to have something that needs no further knowledge.
Cheers,
Gerwin
Email Gateway (Feb 24 2021 at 23:07):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
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.
Email Gateway (Feb 24 2021 at 23:47):From: Gerwin Klein <kleing@unsw.edu.au>
Awesome! Thanks for the remote Windows execution ;-)
I think if the instructions include that it should be a Cygwin64 terminal, this might work, since you need Cygwin anyway for Isabelle.
The one remaining question would be, which path do I need to put in, is it just "/cygdrive/c/afp/thys" or does it need anything else? I.e. is /cygdrive/c the right prefix for Isabelle?
Cheers,
Gerwin
Email Gateway (Feb 25 2021 at 08:03):From: Stepan Holub <holub@karlin.mff.cuni.cz>
I'm not saying the current version is ideal, but it has been fairly quiet on this topic since we changed it to that. Of course that could also be because everyone is even more confused and is just giving up.
Giving up was indeed my reaction for quite some time. For two reasons:
So unless users like me are not supposed to use AFP, the instruction is
useless for them.
Stepan
Email Gateway (Feb 25 2021 at 09:48):From: Gerwin Klein <kleing@unsw.edu.au>
Absolutely happy to add the Windows example now that I know what it should be.
Cheers,
Gerwin
Email Gateway (Feb 25 2021 at 11:20):From: Makarius <makarius@sketis.net>
Cygwin is already bundled with Isabelle. Using that increases chances that
terminal-tinkering actually works. But note that "~" ($HOME) outside of
Isabelle is not necessarily "~" ($USER_HOME) inside Isabelle, even worse
$ISABELLE_HOME_USER can be somewhere else.
The proper way to refer to $ISABELLE_HOME_USER/etc/ROOTS is literally via that
symbolic name inside Isabelle (e.g. the desktop applocation on Windows, or any
other platform).
BTW, even on macOS application-specific config directories should not be
directly in $HOME/.foobar but somewhere else (we don't do this yet).
Makarius
Email Gateway (Feb 25 2021 at 11:25):From: Makarius <makarius@sketis.net>
On 24/02/2021 23:13, Gerwin Klein wrote:
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?Because instructions for editing a file generated too many questions and failure. (What if it doesn't exist? What if it does exist? Adding it at the end or the beginning or the middle? None of that matters, but all of it generates questions and confusion).
Here are again my points about that special ROOTS file again:
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.
Here is the relevant repository reference from 31-Aug-2017 where the main
Isabelle entry point ensures that ROOTS is present:
https://isabelle-dev.sketis.net/rISABELLE6e35cf3ce869
Note that in Isabelle2021 there is even some PIDE support for ROOTS files,
with C-hover-
click on the directory entries.
Neither the 4-5 versions of "echo" nor 2-3 versions of "vi" can do that.
Makarius
Email Gateway (Feb 25 2021 at 19:07):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
cl-isabelle-users-bounces@lists.cam.ac.uk On Behalf Of Gerwin Klein
On 25 Feb 2021, at 19:03, Stepan Holub <holub@karlin.mff.cuni.cz> wrote:
I'm not saying the current version is ideal, but it has been fairly quiet
on this topic since we changed it to that. Of course that could also be
because everyone is even more confused and is just giving up.Giving up was indeed my reaction for quite some time. For two reasons: 1. I
rarely use command line, and I never used echo to edit any file (this may be
embarrassing confession, I am aware) 2. I had no idea how to figure out
"/cygdrive/c/..."
I too must make the same embarrassing confession. I usually use the POSIX printf command or a magnetized needle and a steady hand ;) I had to do some internet searching to find /cygdrive clues and you don't want to know how many foo.txt files I accidentally sprayed across my file system trying to find the right incantation.
So unless users like me are not supposed to use AFP, the instruction is
useless for them.Absolutely happy to add the Windows example now that I know what it should be.
Maybe I'm just an uncivilized fool, but what is wrong with a unified prose "append /home/myself/afp/thys to the contents of ~/.isabelle/Isabelle2021/ROOTS" instructions? Won't *nix wizards be able to figure out the echo command themselves if need be?
Email Gateway (Feb 25 2021 at 21:42):From: David Cock <david.cock@inf.ethz.ch>
Or even have both? I hear bits are fairly cheap these days.
David
Email Gateway (Feb 25 2021 at 22:00):From: Gerwin Klein <kleing@unsw.edu.au>
We did have that other version before (people complained about it, so we have this now), and yes, both is what I'm planning to do.
It is absolutely amazing how hard this bit of instruction seems to be. It's a perfect example of "completely trivial when you know and very hard if you don't".
Definitely looking forward to the more direct integration Makarius mentioned.
Cheers,
Gerwin
Email Gateway (Feb 26 2021 at 05:44):From: Gerwin Klein <kleing@unsw.edu.au>
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.
Cheers,
Gerwin
Email Gateway (Feb 27 2021 at 09:28):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear Gerwin,
thank you. I believe that the current form is much clearer, almost as
clear as needed.
That said, one more remark about what the "echo" advice is worth of. If
an inexperienced user makes a typo in the path (like
"/home/myself/afp/thy" instead of "/home/myself/afp/thys") when first
trying to use the suggested command, he or she is in quite a big
trouble, right?
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.
Best
Stepan
Email Gateway (Feb 27 2021 at 11:18):From: Makarius <makarius@sketis.net>
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
Email Gateway (Feb 27 2021 at 11:34):From: Makarius <makarius@sketis.net>
This should be "isabelle components -u MY_RELATIVE_PATH_TO_AFP".
See also the following Isabelle2021/NEWS entry:
* System *
Makarius
Email Gateway (Feb 27 2021 at 12:00):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Absolutely! Now I understand what Makarius says.
The right instruction is
"Open user setting file in jEdit by: File > Open > Favorites >
$ISABELLE_HOME_USER
and add the line ...
"
Stepan
Email Gateway (Feb 27 2021 at 12:29):From: Makarius <makarius@sketis.net>
With the minor correction that it needs to be Isabelle/jEdit, not just "jEdit"
--- both for formal correctness and respect for the original jEdit project,
which is quite different from our Prover IDE.
Makarius
Email Gateway (Feb 28 2021 at 21:25):From: Gerwin Klein <kleing@unsw.edu.au>
Nice, that is sufficiently simple.
And I had not noticed isabelle components -u in the NEWS, which is also better than the command line instructions we have now. Things are indeed getting better over time.
Cheers,
Gerwin
Last updated: Jul 15 2022 at 23:21 UTC