Re: [isabelle-dev] Time
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
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] Time
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Time
On 30/08/17 09:21, Tobias Nipkow wrote: > I have intentionally not included anything from the AFP. However, importing > an AFP session does not seem to make matters worse (although adding -d > '$AFP' > to isabelle jedit does add 20 secs startup time.) That is a different thing: the Prover IDE potentially needs to edit everything, so all sessions with their theories need to be explored beforehand. This is apt to become a problem on Windows or on a networked file-system. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Time
On 30/08/17 09:21, Tobias Nipkow wrote: > I have a timing issue with b8a6f9337229 (and quite possibly other > revisons): > isabelle build takes 22 secs before it says "Running ...". Since creating > latex documents requires many, many iterations, this is extremely > painful. My > setup is the following: > > None of my files are part of a Mercurial repository. > > What am I doing wrong? How can I speed things up? On the spot, I would say: put all files into a local Mercurial repository. I still need to investigate the details, but it is probably just a very long failed attempt to find the hg root. Is this actually a networked file-system, or anything else that is somehow special? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] time specifications
On Tue, 2 Nov 2010, Makarius wrote: We can now move forward to standardize time specifications as follows: * Time is in seconds, as double precision floating point; users can write 1 or 1.0 or 1.5 etc. * A one-line function ML seconds: real -> Time.time deflates the many variations of Time.fromFoo (typical bulky NJ library design). * ISABELLE_HOME_USER acquires an extra prefix for *named* distributions, i.e. official releases or bightly builds (not compilations from the repository) to allow changing the meaning of former settings in milliseconds. (This helps robustness of installations in general, not just for timeouts.) There are still some fine points missing, but those using seconds as integers can easily upgrade to floats now, using the ML function called "seconds" together with Attrib.config_real or Parse.real. Also note that string_of_real helps to print reals in a simple way (without having to specify custom formats). Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] time specifications
Am 02.11.2010 um 17:30 schrieb Makarius: > Now (e.g. in version c753e3f8b4d6) you can use Parse.real to get the result > of the user using either integer or float notation. The Attrib.config_real > also does that internally. Great. Then I'm totally sold. :) Jasmin ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] time specifications
On Tue, 2 Nov 2010, Jasmin Christian Blanchette wrote: Am 02.11.2010 um 14:08 schrieb Makarius: A very minor issue is that I was never able to parse options like nitpick [timeout = 1.5] even with custom parsers, unless 1.5 is doubly-quoted. Users might not realize they need quoting and will most probably be confused by the resulting error. The above 1.5 was indeed hardly possible before my recent introduction of floating point as native outer syntax tokens, and might be the best posthoc explanation for your format of "s" and "ms". Now (e.g. in version c753e3f8b4d6) you can use Parse.real to get the result of the user using either integer or float notation. The Attrib.config_real also does that internally. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] time specifications
Am 02.11.2010 um 14:08 schrieb Makarius: > The scheme of seconds as float addresses the intuition of at least 3 others > on this thread, as well as Jasmin's requirement to re-scale numbers. > > It only makes sense to make this move, if we arrive at a single standard in > the end, instead of four of them. Floating-point numbers are a decent alternatives, and seconds, being the standard unit for time in physics and elsewhere, makes sense; hence, I will not stand in the way of standardization. (My personal preference does remain for a unit suffix, e.g., "s", for readability's sake, though.) A very minor issue is that I was never able to parse options like nitpick [timeout = 1.5] even with custom parsers, unless 1.5 is doubly-quoted. Users might not realize they need quoting and will most probably be confused by the resulting error. Jasmin ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
