Glad you brought up this topic (although it isn't "spam" for any
meaningful definition of "spam"). I wanted to do it anyway, because
somebody asked me about it privately.
> Jenkins sends lots of mails, and I find it hard to pay attention to them
> at all. Even when I do look, the long message
On 16/07/16 16:37, Lars Hupel wrote:
>> I am open to hear arguments why latex documents need to be continuously
>> available. So far there were none.
>
> That statement is unrelated to what you wrote afterwards, but let me
> give you an argument anyway: The generated PDFs are, as you probably
>
Jenkins sends lots of mails, and I find it hard to pay attention to them
at all. Even when I do look, the long message body makes it hard to find
the key points: What failed? Why did it fail?
Moreover, Isabelle + AFP get naturally out of sync, because pushes on
AFP are often done later, but
> I am open to hear arguments why latex documents need to be continuously
> available. So far there were none.
That statement is unrelated to what you wrote afterwards, but let me
give you an argument anyway: The generated PDFs are, as you probably
agree, formal documents. In that sense, they
On 16/07/16 14:26, Tobias Nipkow wrote:
> But it turns out you are
> right: combining -a and -o document=pdf is not a good idea, it breaks
> Logics_ZF.
In which way does it fail?
I am running "isabelle build -a -o document=pdf" frequently. It should
definitely work.
It might be just an example
On 16/07/16 14:26, Tobias Nipkow wrote:
>>
>> 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).
>
> Your notion of what is
Hallo,
sorry for the broken AFP – it's my fault, but I added a lot of new
material about rings and prime factor decomposition. The projects that
were affected by this the most are already fixed, and I will take care
of the rest on Monday.
Manuel
On 15/07/2016 20:33, Makarius wrote:
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
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".
This refers to Isabelle/6c46a1e786da. The main functionality is in
Isabelle/9f8d06f23c09, which also demonstrates how to do
