Re: [isabelle-dev] Fisher–Yates in AFP

Thanks and I have finally managed to push the entry. Unfortunately a problem like this seems to happen 30% of the time with new AFP entries… Larry > On 4 Oct 2016, at 12:23, Lars Hupel wrote: > >> If it’s no problem, maybe the submission system could check for such >>

Re: [isabelle-dev] Fisher–Yates in AFP

You may want to use   hg archive ~/Fishe-Yates.tar.gz in the future.   - Johannes Am Dienstag, den 04.10.2016, 13:18 +0200 schrieb Manuel Eberl: > Oh, that is quite possible. Sorry about that. I typically keep my > prospective AFP entries in private HG repositories and then simply > tarball

Re: [isabelle-dev] Fisher–Yates in AFP

> If it’s no problem, maybe the submission system could check for such > directories and delete them? I'm adding this to the list of additional checks (some are already in the works). I expect that the submission system will go through a maintenance period in the near future where this will get

Re: [isabelle-dev] Fisher–Yates in AFP

That is indeed the culprit. If it’s no problem, maybe the submission system could check for such directories and delete them? Larry > On 4 Oct 2016, at 12:18, Manuel Eberl wrote: > > Oh, that is quite possible. Sorry about that. I typically keep my prospective > AFP

Re: [isabelle-dev] Fisher–Yates in AFP

Oh, that is quite possible. Sorry about that. I typically keep my prospective AFP entries in private HG repositories and then simply tarball and submit them when it's time. I don't think that ever was a problem before, but it sounds like the most reasonably explanation so far. Good catch!

Re: [isabelle-dev] Fisher–Yates in AFP

> It isn’t only about SourceTree. As I mentioned, manually adding Fisher_Yates > had no effect, and even now "hg diff” shows nothing, even though Fisher_Yates > should appear as “added” or untracked (given that it’s on my machine and > nowhere else). I’ve also checked every .hgignore file. > >

Re: [isabelle-dev] Fisher–Yates in AFP

It isn’t only about SourceTree. As I mentioned, manually adding Fisher_Yates had no effect, and even now "hg diff” shows nothing, even though Fisher_Yates should appear as “added” or untracked (given that it’s on my machine and nowhere else). I’ve also checked every .hgignore file. Possibly my

Re: [isabelle-dev] Fisher–Yates in AFP

I've never used SourceTree, and it is, of course, very difficult to debug such things from afar. I could of course, with your permission, simply commit and push the entry myself. Cheers, Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

Hi Manuel, My point with "finite" was that for the current default setup, you don't need any type class instantiations (see the code equations below). Only if someone imports Card_UNIV from HOL/Library (e.g., for FinFun or for Containers), he or she has to do the instantiations for