Re: [isabelle] AFP instructions



> cl-isabelle-users-bounces at lists.cam.ac.uk On Behalf Of Gerwin Klein
> 
> > On 25 Feb 2021, at 19:03, Stepan Holub <holub at 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?




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