On Fri, 6 Jun 2014, Thomas Sewell wrote:
In case anyone else gets stuck in this situation, here is my best workaround:
cat thys/*/ROOT | grep session | cut -d' ' -f2 | xargs -n 10 isabelle build
-d thys
By focusing on (the dependencies of) 10 sessions at a time, isabelle seems to
get the job done.
The grepping and cutting is a bit ugly. Would it make sense to have an
equivalent of 'findlogics' which found sessions? That would allow
isabelle findsessions -d (DIR) | xargs -n 10 isabelle build -d (DIR)
I take this as a reminder that "isabelle findlogics" is actually legacy
for Proof General, which is to be discarded eventually.
Isabelle system programming is now done in Isabelle/Scala, starting
already 5 years ago, and working more and more smoothly as it is actually
being used. So no more bash, perl, ruby, python, sed, awk scripting, just
plain Scala programming with some Isabelle library operations.
For example, the recently updated build_doc tool (bc61161a5bd0) is now a
proper Isabelle/Scala tool, which merely happens to have a bash wrapper
for historical reasons (it is still required for some administrative bash
scripts).
For regular use, the tool can be used directly in the Console/Scala shell
of Isabelle/jEdit like this (e.g. in current f40ac83d076c):
import isabelle._
Build_Doc.build_doc(Options.init, new Build.Console_Progress(true), docs =
List("jedit"))
This has the advantages of statically-typed programming in an interactive
TTY loop, over an untyped scripting language like bash. It requires a bit
of practice and giving up old customs to become fluent with it, but then
it works surprisingly well. I've done that in the past few weeks
routinely, when working on the Isabelle manuals. It also saves a lot of
JVM process creation and warmup-time.
That approach might be a bit shocking to hardcore Linux users, but for
most Isabelle users it makes more and more sense. Isabelle/jEdit is an
IDE, which means "Integrated Development Environment", so it is not
surprising that it has an integrated system programming shell.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
