Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] calling document build from Scala


view this post on Zulip Email Gateway (Aug 22 2022 at 10:46):

From: Gergely Buday <gbuday@gmail.com>
In an earlier message

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-January/msg00021.html

it is advised to run

$ isabelle scala
scala> import isabelle._
scala> Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), more_dirs = List((true,
Path.current)))

to call document preparation which is said to be the same as

isabelle build -D .

but faster. I get an error:

$ isabelle scala
Welcome to Scala version 2.11.2 (Java HotSpot(TM) 64-Bit Server VM,
Java 1.7.0_67).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import isabelle._
import isabelle._

scala> Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), more_dirs = List((true,
Path.current)))
<console>:11: error: not found: value more_dirs
Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), more_dirs = List((true,
Path.current)))

What is a running version of this, having Isabelle2014? I run this
version as I use theories that are no updated to Isabelle2015.

view this post on Zulip Email Gateway (Aug 22 2022 at 10:48):

From: Makarius <makarius@sketis.net>
On Fri, 3 Jul 2015, Gergely Buday wrote:

In an earlier message

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-January/msg00021.html

That refers to Isabelle2013-2 and is a bit outdated.

it is advised to run

$ isabelle scala
scala> import isabelle._
scala> Build.build(options = Options.init, progress = new
Build.Console_Progress(verbose = false), more_dirs = List((true,
Path.current)))

to call document preparation which is said to be the same as

isabelle build -D .

What is a running version of this, having Isabelle2014? I run this
version as I use theories that are no updated to Isabelle2015.

The Isabelle/Scala function Build.build has changed very little in
Isabelle2014 vs. Isabelle2015, so in both versions it works like this:

scala> Build.build(Options.init, new Build.Console_Progress(verbose = true), select_dirs = List(Path.explode("~/tmp/Test")))

This works best from the Scala console inside Isabelle/jEdit; see also
section 2.5 of the Isabelle/jEdit manual.

You can also look at src/Pure/Tools/build.scala to see the full arguments
of Build.build(). Scala allows named arguments with defaults, to get the
sane invocation as above, despite tons of other arguments.

It all corresponds closely to the "isabelle build" command-line tool,
which is documented in the "system" manual.

Makarius


Last updated: Mar 29 2024 at 08:18 UTC