[isabelle-dev] Time

Makarius makarius at sketis.net
Wed Aug 30 23:02:54 CEST 2017


On 30/08/17 21:50, Makarius wrote:
> On 30/08/17 09:21, Tobias Nipkow wrote:

> I still need to investigate the details, but it is probably just a very
> long failed attempt to find the hg root.

I have now improved that as follows:

changeset:   66558:37b16f8af351
tag:         tip
user:        wenzelm
date:        Wed Aug 30 22:48:50 2017 +0200
files:       src/Pure/General/mercurial.scala
description:
faster check for non-repository, especially relevant for find_repository
to avoid repeated invocation of "hg root";


A more profound approach to speed up repeated document builds works via
Isabelle/jEdit and the Console/Scala plugin.

The invocation of "isabelle build" within that already running Scala/JVM
environment works like this:

  Build.build(PIDE.options.value, new Console_Progress, select_dirs =
List(Path.explode("~/Slides/Curry-Club_Aug-2017")))

The second, third, ... run will be much faster.


That direct use of the Scala function also bypasses the repository
check, because check_unknown_files = false by default.

See also
http://isabelle.in.tum.de/repos/isabelle/file/37b16f8af351/src/Pure/Tools/build.scala#l342


	Makarius



More information about the isabelle-dev mailing list