Re: [isabelle-dev] \nexists
> In contrast, a full "build -a" for the formal content is vital. The > shorter that takes, the more it becomes second nature to do it > frequently -- I often do it for every single changeset (before the local > commit). Not all of us have the appropriate hardware to do that. Speaking about TUM, everyone has at most a quad-core laptop. That's why the testboard is equipped with a total core count of 22, so that "hg push -f testboard" may become "second nature". > That also depends on good physical measurements: that was historically > done without Latex getting in between. I would be the first person to decouple LaTeX processing from the build, but it is impossible as it stands today. You cannot run LaTeX standalone without also running a full build. Speaking about physical measurements: Here are the last build times of JinjaThreads from the past five days: 0:57:36 elapsed time, 3:48:46 cpu time, factor 3.97 0:57:30 elapsed time, 3:48:31 cpu time, factor 3.97 0:58:36 elapsed time, 3:51:08 cpu time, factor 3.94 0:58:36 elapsed time, 3:51:08 cpu time, factor 3.94 0:57:43 elapsed time, 3:48:49 cpu time, factor 3.96 (timings on a VM with threads=8) And for another arbitrary session (Incompleteness): 0:12:08 elapsed time, 0:22:53 cpu time, factor 1.89 0:12:03 elapsed time, 0:22:39 cpu time, factor 1.88 0:12:00 elapsed time, 0:22:52 cpu time, factor 1.90 0:12:26 elapsed time, 0:23:43 cpu time, factor 1.91 0:11:52 elapsed time, 0:22:39 cpu time, factor 1.91 (dedicated machine with threads=2) I'll let others judge whether the variance here is small enough to be useful. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
Hi, > if you have the telemetry data you want to visualize, and just need a > tool for rendering them nicely, you can have a look at the tool I wrote > for GHC: > > GHC instance: https://perf.haskell.org/ghc/ > Tool website: https://github.com/nomeata/gipeda Gipeda does indeed look highly relevant, thanks for mentioning it. > It targets git, but you could either replace the git-specifics by > equivalent code targeting mercurial (they are similar enough in these > matters), or run it over a git mirror of the repositories. I just had a brief look at the sources and concluded that I don't have enough time to adapt them to Mercurial. So: I'm calling for volunteers. Anybody who knows a little Haskell and a little Mercurial, you're more than welcome to turn Gipeda into Hgpeda. If necessary I can provide any kind of output (CSV, JSON, ...) to feed into the tool and also any kind of assistance. (I would rather avoid using the hg-git bridge for it would create a complex workflow.) Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
On 15/07/16 17:08, Tobias Nipkow wrote: > For me a default is something that a) is beneficial for the majority of > users and b) can be overwritten if you don't like it. Isn't that > possible here? That is the existing default of not insisting in Latex documents in every single point of history. When there is something wrong with Latex, it is usually easy to repair afterwards. Asking everybody to test Latex every time imposes a burden with little benefit. In contrast, a full "build -a" for the formal content is vital. The shorter that takes, the more it becomes second nature to do it frequently -- I often do it for every single changeset (before the local commit). The current Isabelle Jenkins setup has changed focus slightly. There are more continuously built "artifacts", like documents, but important "telemetry" data visualization is missing. So we are flying blind concerning performance figures, not just for AFP (as we do for many years), but also for the main repository. What is really needed now, is a replacement for Admin/isatest/isatest-statistics. That also depends on good physical measurements: that was historically done without Latex getting in between. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
On 15/07/16 17:21, Lars Hupel wrote: > > macOS: Problematic because we currently have no appropriate hardware > available to hook into Jenkins. Apple just doesn't offer anything > suitable these days. There is still macbroy2. That is required for administrative purposes, e.g. when preparing a release, but it can be also used for systematic testing. That was also done with isatest in the past. OS X is actually more important for systematic testing than linux, because de-facto I do the Linux testing continuously on my own machine. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
> It is unclear if and how we could get this platform zoo back: it was > rather accidental due to different administration regimes. OpenSUSE: Maybe. I can check how well my Ansible scripts work there, but no promises. Gentoo: Unlikely. macOS: Problematic because we currently have no appropriate hardware available to hook into Jenkins. Apple just doesn't offer anything suitable these days. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
On 15/07/2016 15:32, Makarius wrote: On 15/07/16 13:53, Johannes Hölzl wrote: Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow: LaTeX build problems are not infrequent and could be avoided easily if "build" produced the document by default. +1 -10 Every minute counts in the routine tests that I run continuously all the time. We are in fact again above 30min for "isabelle build -a" for my 12 core machine, which is where the pain starts. For me a default is something that a) is beneficial for the majority of users and b) can be overwritten if you don't like it. Isn't that possible here? Tobias Latex tests add very little information for the extra time. It is usually easy to figure out what needs to be done to make a broken document work again. Moreover, the test often fails because of bad latex installations, not because of bad documents. This old problem has come back on us now, because the Jenkins test always produces documents -- and thus a lot of mails if something is broken there. Latex should be tested occasionally, but it could be done in a less intrusive manner. E.g. only once a day or once week. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
On 15/07/16 15:46, Lars Hupel wrote: >> Latex tests add very little information for the extra time. It is >> usually easy to figure out what needs to be done to make a broken >> document work again. Moreover, the test often fails because of bad latex >> installations, not because of bad documents. > > I disagree. 0% of LaTeX failures observed on the new infrastructure are > spurious, so I'm inclined to keep them running. That is probably because of a very homogenous test environment. The isatest setup had a diversity of platforms and installations, e.g. strange OS X and exotic Linux (SuSE, Gentoo). That was often annoying, but also a reality check to some extent. It is unclear if and how we could get this platform zoo back: it was rather accidental due to different administration regimes. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
> LaTeX build problems are not infrequent and could be avoided easily if > "build" produced the document by default. The quickest way to achieve that would be to set that in the ISABELLE_BUILD_OPTIONS environment variable in ~/.isabelle/etc/settings. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
> Latex tests add very little information for the extra time. It is > usually easy to figure out what needs to be done to make a broken > document work again. Moreover, the test often fails because of bad latex > installations, not because of bad documents. I disagree. 0% of LaTeX failures observed on the new infrastructure are spurious, so I'm inclined to keep them running. Even more so because I will flip the switch to have Jenkins generate devel.isa-afp.org including browser_info and documents this weekend. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax
On 15/07/16 11:49, Lawrence Paulson wrote: > It’s great, but can I pester you about my pet wish? It would be some sort of > “auto-complete” e.g. I type “proof (cases blah)” and somehow automatically > the full “case True show … next case False show … qed” skeleton could be > generated? The same for induction? I know this is far from easy, given the > amount of contextual information involved. It is probably rather trivial. I will come back to variations on sendback information eventually. One reason it was not done very often so far is rather profane: lack of indentation for the inserted text. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
On 15/07/16 13:53, Johannes Hölzl wrote: > Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow: >> LaTeX build problems are not infrequent and could be avoided easily >> if "build" >> produced the document by default. > > +1 -10 Every minute counts in the routine tests that I run continuously all the time. We are in fact again above 30min for "isabelle build -a" for my 12 core machine, which is where the pain starts. Latex tests add very little information for the extra time. It is usually easy to figure out what needs to be done to make a broken document work again. Moreover, the test often fails because of bad latex installations, not because of bad documents. This old problem has come back on us now, because the Jenkins test always produces documents -- and thus a lot of mails if something is broken there. Latex should be tested occasionally, but it could be done in a less intrusive manner. E.g. only once a day or once week. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
Am Freitag, den 15.07.2016, 11:30 +0200 schrieb Makarius: > On 14/07/16 17:50, Lawrence Paulson wrote: > > > > > What’s unfortunate is that the “negated exists” quantifier is > > available > > both for input and output in Isabelle, just not as a TeX macro. > The macro is available here (nipkow 2005-05-30): > http://isabelle.in.tum.de/repos/isabelle/annotate/d51a0a772094/lib/te > xinputs/isabellesym.sty#l224 > > It only needs the amssymb package. > Added amssymb to HOL-MV_A. And reintroduced \nexists in ef794d2e3754. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow: > LaTeX build problems are not infrequent and could be avoided easily > if "build" > produced the document by default. > > Tobias +1 - Johannes > On 14/07/2016 17:50, Lawrence Paulson wrote: > > > > The recent failure in Multivariable_Analysis was caused by the > > \nexists macro, > > which is not defined: > > > > ! Undefined control sequence. > > \nexists > > > > The corresponding source line is here: > > > > Multivariate_Analysis/Brouwer_Fixpoint.thy:have nog: > > "\g. > > continuous_on (S \ connected_component_set (- S) a) g \ > > > > What’s unfortunate is that the “negated exists” quantifier is > > available both for > > input and output in Isabelle, just not as a TeX macro. > > > > I’ve pushed a fix. However, ideally this macro should be defined > > somehow and my > > change reverted. > > > > Larry > > > > > > This body part will be downloaded on demand. > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
LaTeX build problems are not infrequent and could be avoided easily if "build" produced the document by default. Tobias On 14/07/2016 17:50, Lawrence Paulson wrote: The recent failure in Multivariable_Analysis was caused by the \nexists macro, which is not defined: ! Undefined control sequence. \nexists The corresponding source line is here: Multivariate_Analysis/Brouwer_Fixpoint.thy:have nog: "\g. continuous_on (S \ connected_component_set (- S) a) g \ What’s unfortunate is that the “negated exists” quantifier is available both for input and output in Isabelle, just not as a TeX macro. I’ve pushed a fix. However, ideally this macro should be defined somehow and my change reverted. Larry This body part will be downloaded on demand. smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \nexists
On 14/07/16 17:50, Lawrence Paulson wrote: > What’s unfortunate is that the “negated exists” quantifier is available > both for input and output in Isabelle, just not as a TeX macro. The macro is available here (nipkow 2005-05-30): http://isabelle.in.tum.de/repos/isabelle/annotate/d51a0a772094/lib/texinputs/isabellesym.sty#l224 It only needs the amssymb package. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
