Re: [isabelle-dev] Notes on Isabelle/Scala systems programming
On Tue, 29 Apr 2014, Makarius wrote:
I've just done again to update all Isabelle + AFP ROOT files, using standard
Isabelle functions that are already there, but also adding a few more bits
like Isabelle_System.hg for Mercurial command line tools.
Maybe this needs an example how it works (on the Scala console):
import isabelle._
val afp_base = Path.explode("$AFP_BASE")
val afp_files = Isabelle_System.hg("manifest", afp_base).check_error.out_lines
Now we can operate systematically on the real AFP files, not the junk that
happens to lie around in the file-system. E.g. like this:
for { a <- afp_files; if a.endsWith(".thy") || a.endsWith(".ML") }
Check_Source.check_file(afp_base + Path.explode(a))
Normally I don't write such exceedingly long source lines, but the Scala
console might need just one line to copy-paste.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Notes on Isabelle/Scala systems programming
As everybody knows, Isabelle/Scala is the standard language for systems programming in Isabelle. Their might be deep reflexes for "scripting" in perl, python, ruby etc. but the real gems are elsewhere. It is an interesting experience to do that properly in Scala. I've just done again to update all Isabelle + AFP ROOT files, using standard Isabelle functions that are already there, but also adding a few more bits like Isabelle_System.hg for Mercurial command line tools. http://isabelle.in.tum.de/repos/isabelle/raw-file/23883e1879c5/src/Pure/Tools/check_source.scala may serve as an arbitrary example (which is only vaguely related). It is not necessary to include Isabelle/Scala tools into the Pure.jar like that: the isabelle_scala_script wrapper allows to invoke indepdendent tools on the spot. It is documented in the "system" manual. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: session 'document_files'
On Tue, 22 Apr 2014, Makarius wrote: So if nothing happens in between, I will convert all Isabelle + AFP ROOT files systematically at the end of this week. After some canonical delays, this is now in Isabelle/23883e1879c5 and AFP/23883e1879c5. I have also updated the "isabelle mkroot" tool to produce document_files as expected. In the absence of document_files and presence of some document directory, there is an educated guess to imitate the old behaviour, with some legacy warning about it. We can remove that after the release -- it does not pose any problems to users to update their ROOT files on the spot. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
On Tue, 29 Apr 2014, Andreas Lochbihler wrote: * What are your exact hardware parameters: CPU, main memory? Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory That is a recent high-end laptop or a midrange desktop machine. JinjaThreads is *the* biggest Isabelle application on the planet, it deserves a proper workstation or server, lets say with 8 cores and 16 GB minimum (which is still small by today's standards). ML_PLATFORM="x86-linux" ML_HOME="~/.isabelle/contrib/polyml-5.5.1-1/x86-linux" ML_SYSTEM="polyml-5.5.1" ML_OPTIONS="-H 500" That is OK for batch mode, but in interactive mode the GC time of the Poly/ML RTS will be quite noticable. I will make a few experiments with x86_64 and some real memory beyond 16 GB, and report my experience later. * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and JEDIT_JAVA_OPTIONS ? JEDIT_JAVA_OPTIONS="-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" This looks OK for that situation. Note that you can strip the "actors" properties, since I have removed that altogether some days ago (e.g. 326e8a7ea287). The new JVM thread pool is hardwired to the *virtual* number of CPU cores, which is a bit high by default, but it is not used very much in Isabelle/Scala. * What are the options "threads" and "parallel_proofs" ? threads = 0, parallel_proofs = 2 Here we have the standard overloading / overheating of Intel hyperthreaded CPUs. I reckon that most users have that problem, and experience bad reacticity that I never see myself, because I know more about multicore system tuning. The maximum that makes sense on this hardware is threads = "4", as well as ML_OPTIONS="-H 500 --gcthreads 4" In the next Poly/ML release, David Matthews provides the means to have this as default. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of Proof General?
>> What is funny is that Proof General was actually one of the main >> reasons of moving only >> slowly in such token language reforms. > I am glad that PG still works for most of my theories and I try to keep > that state as long as feasible. There are already problems with new > keywords declared by AFP entries that are not listed in the keywords > file. 'isabelle keywords $SESSION' can be used to generate a new keywords file with all keywords of $SESSION. - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 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
