[isabelle-dev] NEWS: split!

[Tobias Nipkow]

* Splitter in simp, auto and friends:
- The syntax "split add" has been discontinued, use plain "split".
- For situations with many conditional or case expressions,
there is an alternative splitting strategy that can be much faster.
It is selected by writing "split!" instead of "split". It applies
safe introduction and elimination rules after each split rule.
As a result the subgoal may be split into several subgoals.

If you have long-running simp or auto calls in situations with a number of if 
and case expressions, split! could help. If you find it does, drop me a line, 
thanks.


Tobias

In f8e79d14d61f.



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] Build statistics

[Lars Hupel]

> I did not know of this JSON API yet. In Isabelle/74604a9fc4c8 there are
> Isabelle/Scala operations to access that information. (It is an
> interesting experience to work with these untyped JSON things; reminds
> me of LISP expressions.)

Having HTTP APIs is one of the perks of running standard software. There
is even a schema describing the possible attributes:

  

Although my usual approach of figuring out anything Jenkins is to dive
into the sources.

> I will later work out, if this is going to be a batch tool (like former
> isatest-stats) or a PIDE GUI panel. It might be actually easier to make
> proper a GUI application than a web application from it.

Web application is probably overkill; a more reasonable approach would
be a set of static pages, not unlike how the current AFP site generator
works.

I can see the appeal of a GUI panel, but bear in mind that gathering all
the data could certainly take a while (even though log files can be
fetched from Jenkins in parallel) – each log file requires one HTTP
round trip.

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