Re: [isabelle-dev] Testing AFP at TUM [was: Isabelle cs. 70300f1b6835]
On Mon, 22 Oct 2012, Gerwin Klein wrote: On 22/10/2012, at 1:46 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Yes, I know. I already fixed Collections on Friday and I am going to go back to this problem on Monday. Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following on one of the lxbroy2…4 machines ISABELLE_FULL_TEST= isabelle afp_build -A -- -o browser_info -o document=pdf -o document_graph -j 2 You shouldn't need most of these options: afp_build already provides all but -j 2 In general -o document_graph does not make much sense on the command line: it is part of the configuration of a session, i.e. hardwired into its ROOT specification. I have already realized in several other situations that the scope of options is not always clear, and not formalized in any way. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing AFP at TUM
On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list (occasionally motivated by commits that apparently hadn't been tested very thoroughly). Perhaps it would be useful to distill these into a concise description of current best practice; either as part of README_REPOSITORY or in the Isabelle Wiki? Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing AFP at TUM
On Mon, 22 Oct 2012, Tjark Weber wrote: On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list (occasionally motivated by commits that apparently hadn't been tested very thoroughly). Perhaps it would be useful to distill these into a concise description of current best practice; either as part of README_REPOSITORY or in the Isabelle Wiki? This raises again a whole bunch of unsettled questions, like What is the Isabelle community wiki anyway? So far there have been mainly semi-official explanations on administrative processes, nothing relevant to a genuine Isabelle community. Professional use of professional systems means you use a stable release, not arbitrary snapshots. Apart from that we have a split into old-school manual testing (what used to be makeall all and is now build -a as shown in the System manual, vs. newer mira/testboard. Old isatest also has some purpose left -- I have recently started some tiny renovations here and there. So just the usual administrative chaos of the past few years ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing AFP at TUM
Am 22/10/2012 14:16, schrieb Tjark Weber: On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list (occasionally motivated by commits that apparently hadn't been tested very thoroughly). Perhaps it would be useful to distill these into a concise description of current best practice; either as part of README_REPOSITORY or in the Isabelle Wiki? We'll try and put something together, but this may take a little while. Thanks Tobias Best regards, Tjark ___ 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] Testing AFP at TUM
On Mon, 22 Oct 2012, Makarius wrote: Apart from that we have a split into old-school manual testing (what used to be makeall all and is now build -a as shown in the System manual, vs. newer mira/testboard. In Isabelle/8b50286c36d3 it is section 3.3 of the system manual, subsection Examples. These command lines are taken from real-life. What I normally do for testing is this: isabelle build -a # build all isabelle build -a -d '$AFP' # build all with AFP Add -j2 or -j4 or -j8 according to your hardware. Pretty obvious? I've developed the habit to test things both after pull and before push, since it saves more time than it costs. I usually run the full AFP test over lunch to see about its health. Recently AFP has become a testbed for heavy-duty interaction tests of Isabelle/jEdit. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
