On 19/07/16 10:17, Lars Hupel wrote:
>>> How can I extract this information from within Isabelle/Scala? How would
>>> this information be presented?
>>
>> It is emitted into the session log file. Build.parse_log may serve as an
>> example how to access it.
>
> Is there no structured way of
>> How can I extract this information from within Isabelle/Scala? How would
>> this information be presented?
>
> It is emitted into the session log file. Build.parse_log may serve as an
> example how to access it.
Is there no structured way of accessing this information? At least it's
Scala but
On 18/07/16 11:05, Joachim Breitner wrote:
> Hi,
>
> Am Montag, den 18.07.2016, 10:39 +0200 schrieb Lars Hupel:
- What about sessions that grow in size over time?
>>>
>>> That is indeed important, although we have just ignored it historically.
>>
>> Right. But how would we take it into
On 18/07/16 10:39, Lars Hupel wrote:
>> Also the detailed parallel runtime parameters that are emitted every
>> 0.5s during a session running: number of active threads, pending futures
>> etc.
>
> How can I extract this information from within Isabelle/Scala? How would
> this information be
> Also the detailed parallel runtime parameters that are emitted every
> 0.5s during a session running: number of active threads, pending futures
> etc.
How can I extract this information from within Isabelle/Scala? How would
this information be presented?
>> - What about sessions that grow in
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
>
> 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
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
> 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,
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
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.
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
> 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
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
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.
> 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
> 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
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
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
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
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
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):
24 matches
Mail list logo
