[isabelle-dev] Time

Tobias Nipkow nipkow at in.tum.de
Thu Aug 31 07:47:17 CEST 2017


That did the job, many thanks.

Tobias

On 30/08/2017 23:02, Makarius wrote:
> 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170831/34d403ca/attachment.bin>


More information about the isabelle-dev mailing list