Re: [isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

It’s nice that global theories don’t have to be qualified. But it’s a bit 
strange that it's forbidden to qualify them.

--lcp

> On 2 Nov 2017, at 17:21, Makarius  wrote:
> 
>> On 02/11/17 17:47, Lawrence Paulson wrote:
>> 
>> And I have triple checked that Probability is spelt correctly. Any hints?
> 
> Since Isabelle/f27488f47a47 you can use completion there (on the theory
> base name).
> 
> E.g. "ALi" completes "HOL-Library.AList".
> 
> 
>Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the new "imports" semantics

[Makarius]

On 02/11/17 17:47, Lawrence Paulson wrote:

> And I have triple checked that Probability is spelt correctly. Any hints?

Since Isabelle/f27488f47a47 you can use completion there (on the theory
base name).

E.g. "ALi" completes "HOL-Library.AList".


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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 02/11/17 16:11, Lars Hupel wrote:
> 
> Tobias and me have discovered an interesting discrepancy between your
> AFP slow setup and our AFP slow setup. They run on identical hardware
> with the only difference of 6 vs 8 threads. On 6 threads, it runs
> significantly faster. For example, Flyspeck-Tame requires 9:44:16
> (elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

It was merely my intuition about the virtual hardware that using less
resources than allocated might help. But I did not make any measurements
with 8 vs. 6 threads, so that guess might be still wrong.

The main observation so far: it works quite well and measurements are
reasonably stable.


> That difference aside, what I also find alarming is that the total
> runtime of Flyspeck-Tame increased by more than 20% after the switch to
> Poly/ML 5.7.

I've had some private email exchange with David Matthews about it. It is
a consequence of a bias towards FixedInt instead of IntInf (= Int) in
the ML code generator. There is some chance that Flyspeck-Tame actually
works with FixedInt, but I did not try it yet.

Which Isabelle codegen options are required to use FixedInt instead of
mathematical Int?

Here is also an experiment to make the present setup
(polyml-test-e8d82343b692) a bit faster:
https://github.com/polyml/polyml/tree/NewTestRegisterSave -- I have some
tests with that still running.


I am more worried about the factor 5 performance loss of Lorenz_C0: now
(3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
the problem is related to Flyspeck-Tame. I did not approach it yet,
because the HOL-ODE tower is really huge.

It would greatly help to see the problem in isolated spots. I usually
send David specimens produced by code_runtime_trace.


> This now means that the slow sessions rapidly approach 24 hours
> in build time, which makes it less feasible to run them every day.

That is already an old AFP tradition :-) Applications are constantly
pushing towards the end of it all, but so far the technology has managed
to keep up.

For the non-slow tests, I have already split AFP into two structually
quite stable parts:
http://isabelle.in.tum.de/repos/isabelle/file/fc87d3becd69/src/Pure/Admin/afp.scala#l86

In the worst case, we could split the slow sessions manually by extra
group tags.


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

Re: [isabelle-dev] the new "imports" semantics

[Dmitriy Traytel]

Hi Larry,

in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means 
that you must import it without any session qualification (just like Main or 
Complex_Main).

Dmitriy

> On 2 Nov 2017, at 17:47, Lawrence Paulson  wrote:
> 
> I’ve been converting some theories from the old pathname syntax to the new 
> setup. I have the line
> 
>   imports "HOL-Probability.Probability”
> 
> but it is rejected with the message
> 
>   Bad theory import "HOL-Probability.Probability"
> 
> If instead I import "HOL-Probability.Random_Permutations” or 
> "HOL-Probability.Central_Limit_Theorem” it works fine. And I have triple 
> checked that Probability is spelt correctly. Any hints?
> 
> Larry
> 
> ___
> 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] the new "imports" semantics

[Lawrence Paulson]

I’ve been converting some theories from the old pathname syntax to the new 
setup. I have the line

imports "HOL-Probability.Probability”

but it is rejected with the message

Bad theory import "HOL-Probability.Probability"

If instead I import "HOL-Probability.Random_Permutations” or 
"HOL-Probability.Central_Limit_Theorem” it works fine. And I have triple 
checked that Probability is spelt correctly. Any hints?

Larry

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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Lars Hupel]

> We are presently testing Poly/ML 5.7.1 by default (see
> Isabelle/aefaaef29c58) and there are already interesting performance
> figures, e.g. see:
> 
> http://isabelle.in.tum.de/devel/build_status
> http://isabelle.in.tum.de/devel/build_status/Linux_A
> http://isabelle.in.tum.de/devel/build_status/AFP
> 
> Overall, performance is mostly the same as in Poly/ML 5.6 from
> Isabelle2017, but there are some dropouts. In particular, loading heap
> images has become relatively slow: this impacts long heap chains like
> HOL-Analysis or big applications in AFP. E.g. see
> http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
> (timing vs. ML timing).

Tobias and me have discovered an interesting discrepancy between your
AFP slow setup and our AFP slow setup. They run on identical hardware
with the only difference of 6 vs 8 threads. On 6 threads, it runs
significantly faster. For example, Flyspeck-Tame requires 9:44:16
(elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

That difference aside, what I also find alarming is that the total
runtime of Flyspeck-Tame increased by more than 20% after the switch to
Poly/ML 5.7. This now means that the slow sessions rapidly approach 24
hours in build time, which makes it less feasible to run them every day.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[Fabian Immler]

I should have sent the message below also to isabelle-dev, sorry about that.
Has anything changed about integers in Poly/ML 5.7.1?

Lorenz_C0 did slow down by a factor of 5, which I find quite extreme.

Best,
Fabian

> Am 28.10.2017 um 23:57 schrieb Fabian Immler :
> 
> Lorenz_C0 is one of those "much slower" sessions.
> If it helps, this is how I would characterize it:
> It is essentially one long computation where the code (IIRC about 15000 lines 
> in SML) was generated in the parent session Lorenz_Approximation via 
> @{computation_check ...}). The computation depends heavily on IntInf 
> operations (but mostly in the <64 bit range)
> 
> Fabian
> 
>> Am 28.10.2017 um 22:45 schrieb Makarius :
>> 
>> On 28/10/17 22:26, Makarius wrote:
>>> We are presently testing Poly/ML 5.7.1 by default (see
>>> Isabelle/aefaaef29c58) and there are already interesting performance
>>> figures, e.g. see:
>>> 
>>> http://isabelle.in.tum.de/devel/build_status
>>> http://isabelle.in.tum.de/devel/build_status/Linux_A
>>> http://isabelle.in.tum.de/devel/build_status/AFP
>> 
>> The daily "AFP slow" timing has arrived just now, 4h hours later than
>> with Poly/ML 5.6:
>> http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads
>> 
>> I still need to investigate, why some sessions require much longer now.
>> It might be due massive amounts of generated code.
>> 
>> 
>>  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] Slow builds due to excessive heap images

[Makarius]

On 28/10/17 22:26, Makarius wrote:
>
> I still have some ideas for "isabelle build" in the pipeline (for
> several years) to skip building intermediate heaps in the first place.
> Then AFP (without the "slow" sessions) could shrink to 50% .. 20% build
> time.
> 
> Until that emerges, AFP contributors may want to double-check, which
> auxiliary heaps ("Base", "Lib", "Pre") are really needed and beneficial
> for overall build times.

That now came out as options for "isabelle jedit", instead of more
"isabelle build" technology (and complexity).


Here is a summary of the present situation:

  * Poly/ML 5.7.1 (testing version) is quite fast in loading heaps, but
there are also file-system accesses and time to build heaps in the first
place (which also means full sharing of live data: at the order of 30s).

  * It does not make sense to refer to a parent session and then use
only a few small theories that require < 10s. Above 30s a parent that is
itself not too bulky usually helps.

  * Building a heap with many ancestors is more expensive than a rather
flat hierarchy. There is a small overhead in the Poly/ML runtime system
for managing the dynamic hierarchy, but more relevant are redundant
imports: a big stack of heaps usually contains many theories that are
not needed in the final application.

  * http://isabelle.in.tum.de/devel/build_status/AFP/index.html shows
some of the data that accumulates in one big Isabelle test database.
There is more than than shown here, e.g. individual theory timings
(which are meaningful for these builds with threads=1).

In the exploration, I've occasionally emitted handwritten SQL statements
to the PostgreSQL engine via the web interface of phppgadmin. At some
point there might be more generated HTML output or some IDE interface to
query the data.


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

[isabelle-dev] NEWS: more options for "isabelle jedit"

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* The command-line tool "isabelle jedit" provides more flexible options
for session selection:
  - options -P opens the parent session image of -l
  - options -A and -B modify the meaning of -l to produce a base
image on the spot, based on the specified ancestor (or parent)
  - option -F focuses on the specified logic session
  - option -R has changed: it only opens the session ROOT entry
  - option -S sets up the development environment to edit the
specified session: it abbreviates -B -F -R -l

  Examples:
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis


This refers to Isabelle/b23adab22e67. It has the potential to save a lot
of interactive build time, and to reduce batch tests by removing old
development artifacts in AFP.

The performance measurements from
http://isabelle.in.tum.de/devel/build_status/AFP/index.html help to
decide which auxiliary session images are merely a waste of time
(probably most of them).

E.g. JNF-HOL-Lib with 37s elapsed time vs. 3s actually spent in ML.


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