The Isabelle System Manual.pdf-资料库

chm9824-4221888-4744302543291956973.pdf-第1页.png

第1页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第2页.png

第2页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第3页.png

第3页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第4页.png

第4页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第5页.png

第5页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第6页.png

第6页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第7页.png

第7页 / 共38页

chm9824-4221888-4744302543291956973.pdf-第8页.png

第8页 / 共38页

The Isabelle System Manual Makarius Wenzel and Stefan Berghofer TU M¨unchen 30 January 2011 lﬁ"=Isabelleba

Contents 1 The Isabelle system environment 1.1 Isabelle settings 1.1.1 Bootstrapping the environment 1.1.2 Common variables 1.1.3 Additional components . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 The raw Isabelle process . . . . . . . . . . . . . . . . . . . . . 1.3 The Isabelle tools wrapper . . . . . . . . . . . . . . . . . . . 1 1 2 3 5 6 9 2 User interfaces 11 2.1 Plain TTY interaction . . . . . . . . . . . . . . . . . . . . . . 11 2.2 Proof General / Emacs . . . . . . . . . . . . . . . . . . . . . . 11 3 Presenting theories Invoking the graph browser 13 3.1 Generating theory browser information . . . . . . . . . . . . . 14 . . . . . . . . . . . . . . . . . . . . . 15 3.2 Browsing theory graphs 3.2.1 . . . . . . . . . . . . . . . 15 3.2.2 Using the graph browser . . . . . . . . . . . . . . . . . 16 3.2.3 Syntax of graph deﬁnition ﬁles . . . . . . . . . . . . . . 18 3.3 Creating Isabelle session directories . . . . . . . . . . . . . . . 19 3.4 Running Isabelle sessions . . . . . . . . . . . . . . . . . . . . 20 3.5 Preparing Isabelle session documents . . . . . . . . . . . . . . 24 . . . . . . . . 25 3.6 Running LATEX within the Isabelle environment 4 Miscellaneous tools Inspecting the settings environment Installing standalone Isabelle executables 27 4.1 Displaying documents . . . . . . . . . . . . . . . . . . . . . . 27 4.2 Viewing documentation . . . . . . . . . . . . . . . . . . . . . 27 . . . . . . . . . . . . . . . . . . . . . . . 28 4.3 Getting logic images 4.4 . . . . . . . . . . . . . . 28 4.5 . . . . . . . . . . . 29 4.6 Creating instances of the Isabelle logo . . . . . . . . . . . . . . 29 4.7 . . . . . . . . . . . . . . . . . . . . 30 4.8 Make all logics . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.9 Printing documents . . . . . . . . . . . . . . . . . . . . . . . . 31 4.10 Remove awkward symbol names from theory sources . . . . . 31 Isabelle’s version of make i

CONTENTS ii 4.11 Output the version identiﬁer of the Isabelle distribution . . . . 31 4.12 Convert XML to YXML . . . . . . . . . . . . . . . . . . . . . 32

Chapter 1 The Isabelle system environment This manual describes Isabelle together with related tools and user interfaces as seen from a system oriented view. See also the Isabelle/Isar Reference Manual [4] for the actual Isabelle input language and related concepts. The Isabelle system environment provides the following basic infrastruc- ture to integrate tools smoothly. 1. The Isabelle settings mechanism provides process environment variables to all Isabelle executables (including tools and user interfaces). 2. The raw Isabelle process (isabelle-process) runs logic sessions either interactively or in batch mode. In particular, this view abstracts over the invocation of the actual ML system to be used. Regular users rarely need to care about the low-level process. 3. The Isabelle tools wrapper (isabelle) provides a generic startup envi- ronment Isabelle related utilities, user interfaces etc. Such tools auto- matically beneﬁt from the settings mechanism. 1.1 Isabelle settings The Isabelle system heavily depends on the settings mechanism. Essen- tially, this is a statically scoped collection of environment variables, such as ISABELLE_HOME, ML_SYSTEM, ML_HOME. These variables are not intended to be set directly from the shell, though. Isabelle employs a somewhat more sophisticated scheme of settings ﬁles — one for site-wide defaults, another for additional user-speciﬁc modiﬁcations. With all conﬁguration variables in at most two places, this scheme is more maintainable and user-friendly than global shell environment variables. In particular, we avoid the typical situation where prospective users of a software package are told to put several things into their shell startup scripts, 1

CHAPTER 1. THE ISABELLE SYSTEM ENVIRONMENT 2 before being able to actually run the program. Isabelle requires none such ad- ministrative chores of its end-users — the executables can be invoked straight away. Occasionally, users would still want to put the $ISABELLE_HOME/bin directory into their shell’s search path, but this is not required. 1.1.1 Bootstrapping the environment Isabelle executables need to be run within a proper settings environment. This is bootstrapped as described below, on the ﬁrst invocation of one of the outer wrapper scripts (such as isabelle). This happens only once for each process tree, i.e. the environment is passed to subprocesses according to regular Unix conventions. 1. The special variable ISABELLE_HOME is determined automatically from the location of the binary that has been run. You should not try to set ISABELLE_HOME manually. Also note that the Isabelle executables either have to be run from their original location in the distribution directory, or via the executable objects created by the install utility. Symbolic links are admissible, but a plain copy of the $ISABELLE_HOME/bin ﬁles will not work! 2. The ﬁle $ISABELLE_HOME/etc/settings is run as a bash shell script with the auto-export option for variables enabled. This ﬁle holds a rather long list of shell variable assigments, thus pro- viding the site-wide default settings. The Isabelle distribution already contains a global settings ﬁle with sensible defaults for most variables. When installing the system, only a few of these may have to be adapted (probably ML_SYSTEM etc.). 3. The ﬁle $ISABELLE_HOME_USER/etc/settings (if it exists) is run in the same way as the site default settings. Note that the variable ISABELLE_HOME_USER has already been set before — usually to some- thing like $HOME/.isabelle/IsabelleXXXX. Thus individual users may override the site-wide defaults. See also ﬁle $ISABELLE_HOME/etc/user-settings.sample in the distribution. Typically, a user settings ﬁle would contain only a few lines, just the assigments that are really changed. One should deﬁnitely not start with a full copy the basic $ISABELLE_HOME/etc/settings. This could cause very annoying maintainance problems later, when the Isabelle installation is updated or changed otherwise.

CHAPTER 1. THE ISABELLE SYSTEM ENVIRONMENT 3 Since settings ﬁles are regular GNU bash scripts, one may use complex shell commands, such as if or case statements to set variables depending on the system architecture or other environment variables. Such advanced features should be added only with great care, though. In particular, external environment references should be kept at a minimum. A few variables are somewhat special: • ISABELLE_PROCESS and ISABELLE_TOOL are set automatically to the absolute path names of the isabelle-process and isabelle executa- bles, respectively. • ISABELLE_OUTPUT will have the identiﬁers of the Isabelle distribution (cf. ISABELLE_IDENTIFIER) and the ML system (cf. ML_IDENTIFIER) appended automatically to its value. Note that the settings environment may be inspected with the Isabelle tool getenv. This might help to ﬁgure out the eﬀect of complex settings scripts. 1.1.2 Common variables This is a reference of common Isabelle settings variables. Note that the list is somewhat open-ended. Third-party utilities or interfaces may add their own selection. Variables that are special in some sense are marked with ∗. ISABELLE_HOME∗ is the location of the top-level Isabelle distribution direc- tory. This is automatically determined from the Isabelle executable that has been invoked. Do not attempt to set ISABELLE_HOME yourself from the shell! ISABELLE_HOME_USER is the user-speciﬁc counterpart of ISABELLE_HOME. The default value is relative to $HOME/.isabelle, under rare circum- stances this may be changed in the global setting ﬁle. Typically, the ISABELLE_HOME_USER directory mimics ISABELLE_HOME to some ex- tend. In particular, site-wide defaults may be overridden by a private $ISABELLE_HOME_USER/etc/settings. ISABELLE_PLATFORM∗ is automatically set to a symbolic identiﬁer for the un- derlying hardware and operating system. The Isabelle platform identi- ﬁcation always refers to the 32 bit variant, even this is a 64 bit machine. Note that the ML or Java runtime may have a diﬀerent idea, depending on which binaries are actually run.

CHAPTER 1. THE ISABELLE SYSTEM ENVIRONMENT 4 ISABELLE_PLATFORM64∗ is similar to ISABELLE_PLATFORM but refers to the proper 64 bit variant on a platform that supports this; the value is empty for 32 bit. ISABELLE_PROCESS∗, ISABELLE_TOOL∗ are automatically set to the full path names of the isabelle-process and isabelle executables, respec- tively. Thus other tools and scripts need not assume that the $ISABELLE_HOME/bin directory is on the current search path of the shell. ISABELLE_IDENTIFIER∗ refers to the name of this Isabelle distribution, e.g. “Isabelle2011”. ML_SYSTEM, ML_HOME, ML_OPTIONS, ML_PLATFORM, ML_IDENTIFIER∗ specify There (see the Isabelle. the underlying ML system to be used for is only a ﬁxed set of admissable ML_SYSTEM names $ISABELLE_HOME/etc/settings ﬁle of the distribution). The actual compiler binary will be run from the directory ML_HOME, with ML_OPTIONS as ﬁrst arguments on the command line. The op- tional ML_PLATFORM may specify the binary format of ML heap im- ages, which is useful for cross-platform installations. The value of ML_IDENTIFIER is automatically obtained by composing the values of ML_SYSTEM, ML_PLATFORM and the Isabelle version values. ISABELLE_PATH is a list of directories (separated by colons) where Isabelle logic images may reside. When looking up heaps ﬁles, the value of ML_IDENTIFIER is appended to each component internally. ISABELLE_OUTPUT∗ is a directory where output heap ﬁles should be stored by default. The ML system and Isabelle version identiﬁer is appended here, too. ISABELLE_BROWSER_INFO is the directory where theory browser information (HTML text, graph data, and printable documents) is stored (see also §3.1). The default value is $ISABELLE_HOME_USER/browser_info. ISABELLE_LOGIC speciﬁes the default logic to load if none is given explicitely by the user. The default value is HOL. ISABELLE_LINE_EDITOR speciﬁes the default line editor for the tty interface. ISABELLE_USEDIR_OPTIONS is implicitly preﬁxed to the command line of any usedir invocation. This typically contains compilation options for

CHAPTER 1. THE ISABELLE SYSTEM ENVIRONMENT 5 object-logics — usedir is the basic utility for managing logic sessions (cf. the IsaMakefiles in the distribution). ISABELLE_FILE_IDENT speciﬁes a shell command for producing a source ﬁle identiﬁcation, based on the actual content instead of the full physical path and date stamp (which is the default). A typical identiﬁcation would produce a “digest” of the text, using a cryptographic hash func- tion like SHA-1, for example. ISABELLE_LATEX, ISABELLE_PDFLATEX, ISABELLE_BIBTEX, ISABELLE_DVIPS refer to LATEX related tools for Isabelle document preparation (see also §3.6). ISABELLE_TOOLS is a colon separated list of directories that are scanned by isabelle for external utility programs (see also §1.3). ISABELLE_DOCS is a colon separated list of directories with documentation ﬁles. ISABELLE_DOC_FORMAT speciﬁes the preferred document format, typically dvi or pdf. DVI_VIEWER speciﬁes the command to be used for displaying dvi ﬁles. PDF_VIEWER speciﬁes the command to be used for displaying pdf ﬁles. PRINT_COMMAND speciﬁes the standard printer spool command, which is ex- pected to accept ps ﬁles. ISABELLE_TMP_PREFIX∗ is the preﬁx from which any running isabelle-process derives an individual directory for temporary ﬁles. The default is some- where in /tmp. 1.1.3 Additional components Any directory may be registered as an explicit Isabelle component. The general layout conventions are that of the main Isabelle distribution itself, and the following two ﬁles (both optional) have a special meaning: • etc/settings holds additional settings that are initialized when boot- strapping the overall Isabelle environment, cf. §1.1.1. As usual, the content is interpreted as a bash script. It may refer to the component’s enclosing directory via the COMPONENT shell variable.

资料库

The Isabelle System Manual.pdf

相关推荐

课程资源

热门标签

最新资料