[isabelle-dev] Testboard
Hi, I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within reasonable time? -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] General code_abort'd constant
Hi Florian, in 2b761d9a74f5, I now have replaced Predicate.not_unique with Code.abort. I decided to leave Enum.the as is, because there is a special translation for the Eval target such that Enum.the raises Match instead of Fail (although I do not know whether the specific setup is important). Andreas On 26/09/13 17:50, Florian Haftmann wrote: Hi Andreas, See now 788730ab7da4, which replaces all code_abort in HOL/Library with Code.abort. There are still two code_aborts in HOL (in Predicate and Enum) that Code.abort should subsume, but Code.abort can only be defined in String.thy due to the error message parameter it takes, and Predicate and Enum do not import String. As I am not familiar with the HOL import graph, I don't know whether one could easily change it such that Code.abort is available in Predicate and Enum. But even if it is, this is probably not going to happen before the release. Making Predicate.thy dependent on String.thy is no problem. The reason why Enum.thy is bootstrapped before String.thy is that »enum« allows for a nice code setup which is also valid in presence of Code_Char.thy. However you arrange it, there is always one piece of code setup which cannot be bootstrapped from the beginning. Hope this helps, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
On 27.09.2013 09:16, Peter Lammich wrote: I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within reasonable time? Basically Mira is just watching the repository. If a test run finishes, it looks at the repository, takes the tip and tests it (if it was not already tested). In particular, this means that later pushes can take the focus away from your pushes. It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
I always thought that there are two use-cases of Testboard: 1. Whenever you push to the Isabelle repository, this is tested by testboard 2. You can push your changeset only to testboard, to check it before pushing it to the isabelle repo and perhaps breaking it. However, according to Lars' reply, the second use-case is almost not possible, as a particular changeset will quickly be hidden by a huge number of later pushes to the isabelle repository, and never be touched again. So here is my question: If I have some changeset, and want to check whether it breaks AFP before pushing it to the isabelle repository, how do I do it? Can I use Testboard? -- Peter On Fr, 2013-09-27 at 11:49 +0200, Lars Noschinski wrote: On 27.09.2013 09:16, Peter Lammich wrote: I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within reasonable time? Basically Mira is just watching the repository. If a test run finishes, it looks at the repository, takes the tip and tests it (if it was not already tested). In particular, this means that later pushes can take the focus away from your pushes. It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
Am 27.09.2013 um 12:29 schrieb Peter Lammich lamm...@in.tum.de: So here is my question: If I have some changeset, and want to check whether it breaks AFP before pushing it to the isabelle repository, how do I do it? Can I use Testboard? I don't know if you're using queues, but what I typically do in such (rare) cases is to qpop all, then pull and update, then qpush back to where I was, and then push the resulting new patch to Testboard again. This gives you a second shot and if you're lucky, it will get tested thoroughly. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Problem with transfer method
Hi, referring to 024fadbd03f0, at the end of the attached theory: context field_char_0 begin … lemma of_rat_minus: of_rat (- a) = - of_rat a apply transfer the »- _« (name uminus) gets replaced by a bound variable »uminusa«. There seems to be a problem with the context here. Sorry for not distilling a smaller example, but I have no idea how to restore this situation after the final declarations lifting_update rat.lifting lifting_forget rat.lifting in Rat.thy. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de Transfer_Context.thy Description: application/extension-thy signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
