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):
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
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
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 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
> 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
> 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
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
> 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.
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
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.
> 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
15 matches
Mail list logo
