Re: [isabelle-dev] \nexists

[Makarius]

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 accessing this information? At least it's
> Scala but it's also still the moral equivalent of grepping files, a
> technique I've managed to avoid so far.

It is already a bit more formal, due to the \f markers and the YXML data
representation.

One day it should all become PIDE document markup, i.e. YXML everywhere
without plain text 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

[Lars Hupel]

>> 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 it's also still the moral equivalent of grepping files, a
technique I've managed to avoid so far.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Makarius]

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 account? What registers as a spike
>> in build time for a session could either be a performance regression in
>> Isabelle or growing material.
> 
> Wouldn’t that be quite obvoius from the a quick glance at the changeset
> in question?
> 
> I manually watch https://perf.haskell.org/ghc/ when I see a regression
> I apply common sense to decide whether to notify the authors, or
> whether it is genuine.
> 
> Sure, something fully automatic and reliable would be nice, but having
> numbers and graphs is still useful, even if “graph goes up →
> performance regression happened” does not hold unconditionally.

Nicely plotted graphs and for a human to inspect are indeed the most
important tool.

When we still had good physical measurements (some years ago), I used to
look at the graphs every morning, even before checking my email. And
then at the corresponding changesets to figure out what happened.

Another important application works the other way round: changes are
introduced with the intention to make some difference in performance,
and in the coming days the graph hopefully develops a noticable step
upwards or downwards.


Makarius




signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Makarius]

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 presented?

It is emitted into the session log file. Build.parse_log may serve as an
example how to access it.

Presentation could be done as in the Monitor panel of Isabelle/jEdit.
The Isabelle/Scala modules ML_Statistics and Task_Statistics provide
further possibilities.

All this uses JFreeChart, which is a relatively wellknown and decent 2D
chart drawing framework. It is much less than gnuplot, though,
especially concerning interpolation and smoothing of curves.


>>> - 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 account? What registers as a spike
> in build time for a session could either be a performance regression in
> Isabelle or growing material.

The maximum and final heap size (from the above data) might serve well
as a single value.

Apart from that, the full chart is occasionally useful to understand
resource shortage better.


Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Lars Hupel]

> 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 size over time?
> 
> That is indeed important, although we have just ignored it historically.

Right. But how would we take it into account? What registers as a spike
in build time for a session could either be a performance regression in
Isabelle or growing material.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Makarius]

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
> agree, formal documents. In that sense, they need to be checked
> continuously.

I invented that notion of formal documents myself, but I don't see the
reasoning why the latex runs need to be continuously checked. Nothing
depends on the resulting PDFs. When there is something wrong with it, it
is usually just a matter of untyped/unscoped latex macros and not
formally relevant.

So Latex could be run once a week or once a month, and very little will
happen.


In contrast, a broken proof, definition, or ML programming interface
causes a complete halt of the subsequent sessions building on that.

Broken formal content is particularly annoying, because nothing can be
reasonably "pushed on top of it". It would make the formal holes bigger
and bigger.


> But the situation is completely clear. Jenkins gives you an overview of
> what exactly broke, by means of the "changes" page:
> 
>   
> 
> It even provides handy links to the changesets.

I still have problems reading these Jenkins web pages: they seem to
contain 90% irrelevant information.


> To give useful performance metrics, here are
> some questions off the top of my head:
> 
> - Measure the whole build time or just sessions?

Separate session build times is important, but overall times also useful
to know.


> - Which sessions? What should be the minimum threshold for session
> runtime to be considered useful?

There could be indeed a threshold, e.g. 10-20s minimum session build
time to show it at all.


> - Elapsed time or CPU time?

Both is important.

Also the detailed parallel runtime parameters that are emitted every
0.5s during a session running: number of active threads, pending futures
etc.


> - What about sessions that grow in size over time?

That is indeed important, although we have just ignored it historically.

The AFP/Collections sessions are pretty close to the inevitable concrete
wall. It would be better to see in some nice graph, how the approach
towards hard limits progresses, and how attempts to postpone the hit
come out as changed performance figures.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Lars Hupel]

> 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 need to be checked
continuously.

> Instead we have in Isabelle/76492eaf3dc1 + AFP/89fba56726d8 a typical
> situation where formal checking no longer works, due to changes in main
> Isabelle that are not immediately clear.

But the situation is completely clear. Jenkins gives you an overview of
what exactly broke, by means of the "changes" page:

  

It even provides handy links to the changesets.

> In the last 10 years, continuous testing of Isabelle + AFP had the
> following main purposes:
> 
>   * Make sure that formal checking of Isabelle always works 100% (main
> repository).

Still satisfied.

>   * Help to figure out quickly why a broken AFP stopped working. When
> did it work last time with Isabelle?

Still satisfied.

>   * Provide continuous performance measurements to keep everything going
> in the longer run: i.e. to avoid the "invisible concrete wall" that is
> always ahead of us, and moved occasionally further ahead.

The numbers are there, but we need some good way to evaluate them. I
have pointed that out multiple times.

Let me be very clear: I have invested a lot of time in a robust,
reliable, reproducible testing infrastructure. Almost everything now
uses standardized tools instead of ad-hoc Bash or Perl scripts and
consumes or produces structured data. But I cannot single-handedly
implement all the features. To give useful performance metrics, here are
some questions off the top of my head:

- Measure the whole build time or just sessions?
- Which sessions? What should be the minimum threshold for session
runtime to be considered useful?
- Elapsed time or CPU time?
- What about sessions that grow in size over time?

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Makarius]

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 of latex failure due to some odd latex
installation.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Makarius]

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 good for developers differs from their own
> notion, at least for the ones I talked to. But it turns out you are
> right: combining -a and -o document=pdf is not a good idea, it breaks
> Logics_ZF.

I am open to hear arguments why latex documents need to be continuously
available. So far there were none.

Instead we have in Isabelle/76492eaf3dc1 + AFP/89fba56726d8 a typical
situation where formal checking no longer works, due to changes in main
Isabelle that are not immediately clear.


In the last 10 years, continuous testing of Isabelle + AFP had the
following main purposes:

  * Make sure that formal checking of Isabelle always works 100% (main
repository).

  * Help to figure out quickly why a broken AFP stopped working. When
did it work last time with Isabelle?

  * Provide continuous performance measurements to keep everything going
in the longer run: i.e. to avoid the "invisible concrete wall" that is
always ahead of us, and moved occasionally further ahead.


Only little of that has been provided by the testing infrastructure in
recent years. The new Jenkins setup and the new hardware has improved
the sitation a bit, but we are still below the situation from some years
ago.

This is why I am doing more testing manually on my own machine than was
necessary in the past.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Tobias Nipkow]

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 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).


Your notion of what is good for developers differs from their own notion, at 
least for the ones I talked to. But it turns out you are right: combining -a and 
-o document=pdf is not a good idea, it breaks Logics_ZF.


Tobias



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





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

[Lars Hupel]

> 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

[Lars Hupel]

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

[Makarius]

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

[Makarius]

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

[Lars Hupel]

> 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

[Tobias Nipkow]

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

[Makarius]

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

[Lars Hupel]

> 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

[Lars Hupel]

> 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] \nexists

[Makarius]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Tobias 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 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

[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/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

[isabelle-dev] \nexists

[Lawrence Paulson]

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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev