[isabelle-dev] NEWS: SQL database access in Isabelle/Scala

2017-05-15 Thread Makarius 
*** System ***

* Isabelle/Scala: the SQL module supports access to relational
databases, either as plain file (SQLite) or full-scale server
(PostgreSQL via local port or remote ssh connection).

* Results of "isabelle build" are recorded as SQLite database (i.e.
"Application File Format" in the sense of
https://www.sqlite.org/appfileformat.html). This allows systematic
access via operations from module Sessions.Store in Isabelle/Scala.


This refers to Isabelle/82add6bf8a42. There are also some administrative
notes of PostgreSQL in Admin/build_log/README.

SQL database access opens many possibilities for the near future. E.g.
PIDE markup that is stored persistently; it would allow to browse formal
sources of Isabelle + AFP in the Prover IDE (or some other client)
without reprocessing.


The implementation in src/Pure/General/sql.scala is relatively
unexciting: it shows that simple things can be done in a simple way,
without too much boilerplate of JDBC. Moreover, I did not pull in any of
the more ambitious Scala/JDBC projects that are emerging elsewhere.


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

Re: [isabelle-dev] Poly/ML 5.7

2017-05-15 Thread Makarius 
On 15/05/17 14:24, Makarius wrote:
> On 15/05/17 12:29, Lawrence Paulson wrote:
>> Version 5.7 doesn’t even build on my main workstation, though it works
>> on my MacBook Pro running broadly similar software. No idea what is
>> going on here, but I’m not happy about it.
> 
> There are already some mail threads on the Poly/ML list, where various
> people have helped out to consolidate the situation.
> 
> Anyone who is proficient with C/C++ and various platforms (Linux,
> Windows, Mac OS X varieties) is invited to join there -- not just now,
> but also in the longer term.

Some of this activity is actually on the HOL and ProofPower mailing
list, apart from the Isabelle side here.

We should make sure that everything relevant to Poly/ML also goes over
its official mailing list:
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


Makarius

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

Re: [isabelle-dev] Poly/ML 5.7

2017-05-15 Thread Makarius 
On 15/05/17 12:14, Makarius wrote:
> Some results can be seen here:
> 
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
> 
> The test hardware is similar or actually the same as "Linux A", but this
> needs to be investigated further. It is also important to compare
> timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task
> is still busy digging into older history.

I have now changed that here:

changeset:   65840:8d7b2ac9a245
tag: tip
user:wenzelm
date:Mon May 15 14:27:14 2017 +0200
files:   src/Pure/Admin/isabelle_cronjob.scala
description:
history parameters like "Linux A", for more comparable results;


Maybe I also manage to get ml_statistics into the charts soon. Then we
can look at heap, task, thread details etc.


Makarius

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

Re: [isabelle-dev] Poly/ML 5.7

2017-05-15 Thread Makarius 
On 15/05/17 12:29, Lawrence Paulson wrote:
> Version 5.7 doesn’t even build on my main workstation, though it works
> on my MacBook Pro running broadly similar software. No idea what is
> going on here, but I’m not happy about it.

There are already some mail threads on the Poly/ML list, where various
people have helped out to consolidate the situation.

Anyone who is proficient with C/C++ and various platforms (Linux,
Windows, Mac OS X varieties) is invited to join there -- not just now,
but also in the longer term.


Note that for Isabelle, the build process works via "isabelle
build_polyml" from recent repository versions, see also
http://isabelle.in.tum.de/repos/isabelle/annotate/8007f10195af/src/Pure/Admin/build_polyml.scala

Going through Isabelle/Scala has the slight disadvantage of obscuring
the description of the build process, but it is more robust and
repeatable on all these platform variations.


Makarius

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

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-05-15 Thread Makarius 
On 25/04/17 09:41, Mathias Fleury wrote:
>  
>> What is good about it?
> (I don't remember enough of the previous system to compare it to Jenkins.)

Lets go back to some points on this thread, now that I have finished
more implementation work.


>   * automatic testing (I have forgotten to add files a couple of times).

Forgetting to add files in a commit was one of the few cases where the
remote test actually had a benefit. The start of this thread was such an
incident, see Isabelle/006a274cdbc2.

Thinking once more about the problem, it is clear that the standard
"isabelle build" tool can do that check on the spot.  See now:

changeset:   65829:2fb85623c386
user:wenzelm
date:Sun May 14 20:16:13 2017 +0200
files:   src/Pure/General/mercurial.scala src/Pure/Tools/build.scala
description:
implicitly check for unknown files (not part of a Mercurial repository);

 src/Pure/General/mercurial.scala |  31 +++
 src/Pure/Tools/build.scala   |  15 +++
 2 files changed, 46 insertions(+), 0 deletions(-)



>   * timings
> 
> (https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html).
> It is useful to see how it evolves over time.

I actually made this myself in reminiscence of the old isatest
statistics, see also various mails in the vicinity of
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-August/007070.html

In that discussion it also became clear that Jenkins lacks scalable test
data management: queries via its API are very slow. This ultimately
motivated the PostgreSQL database server that is now behind
http://isabelle.in.tum.de/devel/build_status/index.html (PostgreSQL is a
great product that does its job very well without much ado.)


To reintegrate the old data source, I have added a function to download
Jenkins logs into the same log directory as the other build_status
information, see:

http://isabelle.in.tum.de/repos/isabelle/rev/2773b6859c55
http://isabelle.in.tum.de/devel/build_status/jenkins_isabelle-nightly-benchmark_64bit_6_threads/index.html
http://isabelle.in.tum.de/devel/build_status/jenkins_isabelle-nightly-slow_64bit_8_threads/index.html

This replaces the former chart plotting directly from Jenkins, so Lars
can now dismantle https://ci.isabelle.systems/statistics (which still
says "Generated at Tue, 18 Apr 2017 00:02:04 GMT").


Makarius

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

Re: [isabelle-dev] Poly/ML 5.7

2017-05-15 Thread Lawrence Paulson 
Version 5.7 doesn’t even build on my main workstation, though it works on my 
MacBook Pro running broadly similar software. No idea what is going on here, 
but I’m not happy about it.
Larry

> On 15 May 2017, at 11:14, Makarius  wrote:
> 
> David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago
> (see https://github.com/polyml/polyml/releases/tag/v5.7), but announced
> it only last week.
> 
> I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that
> is only for testing, not for production use. Some results can be seen here:
> 
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
> 
> The test hardware is similar or actually the same as "Linux A", but this
> needs to be investigated further. It is also important to compare
> timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task
> is still busy digging into older history.
> 
> 
> After the substantial changes of the code generator and representation
> of ML values in memory, there are various open questions concerning
> performance and robustness of Isabelle applications.
> 
> This means, we need to skip the Poly/ML 5.7 release and stay on the last
> Poly/ML 5.6 until the situation becomes more clear.
> 
> 
> This is how to use the polyml-5.7 component locally:
> 
>  $ edit $ISABELLE_HOME_USER/etc/settings
> 
>  init_component "$HOME/.isabelle/contrib/polyml-5.7"
> 
>  $ isabelle components -a
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[isabelle-dev] Poly/ML 5.7

2017-05-15 Thread Makarius 
David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago
(see https://github.com/polyml/polyml/releases/tag/v5.7), but announced
it only last week.

I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that
is only for testing, not for production use. Some results can be seen here:

http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html

The test hardware is similar or actually the same as "Linux A", but this
needs to be investigated further. It is also important to compare
timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task
is still busy digging into older history.


After the substantial changes of the code generator and representation
of ML values in memory, there are various open questions concerning
performance and robustness of Isabelle applications.

This means, we need to skip the Poly/ML 5.7 release and stay on the last
Poly/ML 5.6 until the situation becomes more clear.


This is how to use the polyml-5.7 component locally:

  $ edit $ISABELLE_HOME_USER/etc/settings

  init_component "$HOME/.isabelle/contrib/polyml-5.7"

  $ isabelle components -a


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