[isabelle-dev] Fisher–Yates in AFP

Lawrence Paulson lp15 at cam.ac.uk
Tue Oct 4 12:40:16 CEST 2016


I have no idea at all what is going on here.

Normally I use the SourceTree app with Mercurial, and this time around I was puzzled to see that it did not show Fisher–Yates as an untracked file. So I added it manually instead:

~/isabelle/afp/devel/thys: hg add Fisher_Yates

It still didn’t show up but I thought surely that would take effect following the next commit. From what you say it didn’t, and the file remains completely invisible to Mercurial as well. If you see the attached screenshot, you will see SourceTree set to display “all files” in alphabetical order, and Fisher–Yates is not there. But if you look at the directory itself, bingo there it is. Also completely manually:

~/isabelle/afp/devel/thys: ls -l Fisher_Yates/
total 24
-rw-r--r-- 1 lp15 staff 16783 Sep 30 11:19 Fisher_Yates.thy
-rw-r--r-- 1 lp15 staff   149 Oct  3 16:21 ROOT
drwxr-xr-x 3 lp15 staff   102 Aug 30 12:45 document
~/isabelle/afp/devel/thys: hg diff
~/isabelle/afp/devel/thys: 

I’m afraid I have to give up.

Larry

> On 4 Oct 2016, at 10:41, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> Hallo,
> 
> I just wanted to point out that it appears that you accidentally did not commit Fisher–Yates to the afp-devel repository and now the build broke because of that.
> 
> Cheers,
> 
> Manuel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20161004/2a8af6de/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screen Shot 2016-10-04 at 11.17.06.png
Type: image/png
Size: 209911 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20161004/2a8af6de/attachment-0001.png>


More information about the isabelle-dev mailing list