[isabelle-dev] NEWS: toplevel theorem statements

*** General *** * Toplevel theorem statements have been simplified as follows: theorems ~> lemmas schematic_lemma ~> schematic_goal schematic_theorem~> schematic_goal schematic_corollary ~> schematic_goal Command-line tool "isabelle update_theorems" updates

Re: [isabelle-dev] HOL-Proofs broken?

Hi Makarius, > My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of > resources and fail. I've made approx. 3 runs in the vicinity -- it always > takes very long. > > Is that another failure to do a full "isabelle build -a" before pushing > anything? I did "isabelle

Re: [isabelle-dev] HOL-Proofs broken?

As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64 Dmitriy > On 06 Oct 2015, at 21:54, Jasmin Blanchette > wrote: > > Hi Makarius, > >> My

Re: [isabelle-dev] HOL-Proofs broken?

On Tue, 6 Oct 2015, Dmitriy Traytel wrote: As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. This conforms to my expectations: HOL-Proofs is slow, but works. I am presently on a side-branch starting from 5b5656a63bd6, and that works as well:

Re: [isabelle-dev] HOL-Proofs broken?

On Tue, 6 Oct 2015, Makarius wrote: On Tue, 6 Oct 2015, Dmitriy Traytel wrote: As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. This conforms to my expectations: HOL-Proofs is slow, but works. I am presently on a side-branch starting from

Re: [isabelle-dev] HOL-Proofs broken?

> On 06.10.2015, at 22:37, Makarius wrote: > >> On Tue, 6 Oct 2015, Dmitriy Traytel wrote: >> >> So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71. > > More results on macbroy2: > > 5b5656a63bd6 > Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28

[isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle

What is the situation with mira reports? The website shows a default Mercurial view, without any test results. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] HOL-Proofs broken?

My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of resources and fail. I've made approx. 3 runs in the vicinity -- it always takes very long. Is that another failure to do a full "isabelle build -a" before pushing anything? I've actually violated this principle

Re: [isabelle-dev] http://isabelle.in.tum.de/reports/Isabelle

> What is the situation with mira reports? The website shows a default > Mercurial view, without any test results. The situation is that Mira (including testboard) appears to be broken beyond repair. On Monday, I have taken over responsibility for our continuous integration builds and am already

[isabelle-dev] Broken AFP sessions

Here are some more proof failures (Isabelle/5b5656a63bd6 and AFP/21bdf9fbf229): Integration FAILED *** At command "by" (line 1724 of "~/isabelle/afp-devel/thys/Integration/Integral.thy") Markov_Models FAILED *** At command "done" (line 1038 of

[isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2

The title says it all. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2

Thanks, sorry (24b5e7579fdd). Jasmin > On 06.10.2015, at 11:42, Dmitriy Traytel wrote: > > The title says it all. > > Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] Scrollbar, where are thou?

Hi, I’m not sure if this is rather something for the jEdit mailing list, but I try here first. The attached theory is an empty 500+ lines long file where everything is normal. However, if I add one new line the scrollbar disappears. The above applies to 2007ea8615a2 but I believe I saw this

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities. I don't think HOL Light supports comments at this level. HOL4 does, using SML's (* ... *). So, if you want to write the escaped *, you have to use our older syntax for the same (using a $ for "op": $*), or

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

On Tue, 22 Sep 2015, Tobias Nipkow wrote: The "op" noation is idiosyncratic, but there are examples (not in individual formulae) where I find some such notation convenient. I would welcome Haskell's "(+)", but that has a problem with "(*)". Unless we can make that notation work, I don't think

Re: [isabelle-dev] Scrollbar, where are thou?

On Tue, 6 Oct 2015, Dmitriy Traytel wrote: I’m not sure if this is rather something for the jEdit mailing list, but I try here first. The attached theory is an empty 500+ lines long file where everything is normal. However, if I add one new line the scrollbar disappears. The above applies

Re: [isabelle-dev] Notes on GHC an mutable data structures

On Tue, 22 Sep 2015, Florian Haftmann wrote: http://www.aosabook.org/en/ghc.html, section starting with »Crime Doesn't Pay« – from The Architecture of Open Source Applications (Volume 2): The Glasgow Haskell Compiler That is indeed a very interesting document. About half of the points