CML2 Language Reference

Copyright

Permission is granted to copy, distribute and/or modify this document under the terms of the Open Publication License, version 2.0.

Abstract

This is a reference manual for CML2, the Configuration Menu Language designed to support Linux kernel configuration. For higher-level discussion of the language and the concepts behind it, see the paper The CML2 Language, available at the CML2 project website. Configuration hackers should read that paper first to get a feel for the language.


Table of Contents
Roadmap to This Document
Running the CML2 tools
CML2 Language Elements
CML2 configuration file format
Change history

Roadmap to This Document

First, there's a section on invoking the CML2 tools. Then there's a complete language reference. Then there's a description of the configuration file output formats. Finally, a document change history.

For tips on good menu design, see The CML2 Language.


Running the CML2 tools

The CML2 toolkit consists of two Python programs: cmlcompile and cmlconfigure. The compiler, cmlcompile, generates a pickled representation of a rulebase from one or more files of CML2 rules. The interpreter, cmlconfigure, reads in a rulebase and uses it to inform a configuration dialogue with the user.

The cmlconfigure program queries its environment to discover what I/O facilities are available. It will use X if it's on an X display and Tkinter can be found. Otherwise, it will look for the curses library and support a full-screen character interface. If it can't find curses and a TERM in the environment, it will fall back to a line-oriented mode.

The end result is a configuration file, consisting of comments and name-value pairs (see the section called CML2 configuration file format for complete specification). The defconfig consists of a set of variable definitions in shell syntax; it can be re-read by a future instance of cmlconfigure to set defaults. The macrofile is a list of C-style #define macros intended to be included in kernel C code.

The compiler, cmlcompiler, requires one or more CML2 rules files as arguments. It has two options:

-o filename

Set the file to which the compiled rulebase is written. By default, if no -o option is given, the rulebase goes to rules.out.

-v

Enable debugging output to stdout.

The interpreter, cmlconfigure, takes at most one filename argument: the rulebase to be interpreted. If no argument is specified, it reads from rules.out. The interpreter recognizes the following options:

-b

Batch mode. Read in a compiled rulebase, apply any other command-line options, and immediately write out the rulebase. Most useful with -D to change a single option or a small handful of options from the command line.

-B

Supply a banner string. Front ends may use this to modify the screen display. Can be used, for example, to pass in a version number of the system you are configuring.

-i configfile

Read in a configuration. The file is expected to be in the same defconfig format written by cmlconfigure. Values (including n) are set as though selected interactively by the user.

If the file does not exist, complain but continue. This behavior allows the configurator to look for defaults files which may not exist.

-I configfile

Read in a configuration. The file is expected to be in the same defconfig format written by cmlconfigure. Values (including n) are frozen and will be displayed but not modifiable during the configure run.

-l

List. Run in batch mode to generate a menu map (that is, a tree diagram of all the menus and question symbols in the system.)

-o outfile

Set the location to which cmlconfigure should write its defconfig file of shell variable settings. This file will be loadable by cmlconfigure. If there is no -o option, output is written to config.out.

-t

Force tty (line-oriented) mode.

-s

Force debugger mode. This is a variant of tty (line-oriented) mode designed for debugging rulesets.

-c

Force curses (screen-oriented) mode.

-x

Force X (GUI using Tk) mode.

-q

Force alternate X GUI mode based on a tree widget.

-s

Select the debugger mode. This is similar to the ordinary line-oriented mode, and shares many commands with it (type ? for complete list). Unlike -t mode, debugger mode never sets a symbol without an explicit command to do so, doesn't automatically traverse to the next symbol, and doesn't generate elaborate prompts. Instead it provides a richer set of commands for examining the theorem-prover's state. Use it to interpret scripts for reproducing bugs.

-v

Increment the debug flag. (Note: This was -d in earlier versions)

-d

Preset a symbol. -DFOO sets FOO=y at startup. -dFOO=xxx may be used to specify a value. The trit values y, m, n are understood.

-D

Preset a symbol and freeze it.

-S

Don't hide elided symbols. When this option is on, suppressions are ignored. Only symbols that have derived a frozen value from -D or constraints are skipped. This may be useful if you know that you want to set configuration symbols deep in the hierarchy and have their requirements propagate upwards, as opposed to the normal sequence in which you refine your way down from the top of the tree with symbols becoming visible only when they are unmasked by previous questions.

-V

Print the configurator version and exit.

The environment variable CML2OPTIONS may specify command-line switches (but not arguments). Switches taken from CML2OPTIONS are processed before switches specified on the actual command line.

The environment variable BROWSER may specify a colon-separated list of browser commands, to be used in making URLs in the help widgets live. Each command should have the string "%s" in it where the URL can be substituted. The CML2 front end will try the commands in succession until one succeeds. The default sequence is mozilla, then any netscape already running, then a new netscape instance, then lynx, then w3m.

The configurator returns the following status codes to the invoking program:

0

Normal save and exit.

1

Quit (exit without save).

2

Configurator aborted by interrupt.

3

Configurator aborted due to unsatisfiable rulebase.


CML2 Language Elements

Syntax

Lexically, a CML program consists of tokens: barewords, whitespace, strings and punctuation (there is one exception associated with the icon declaration). A bareword is a token composed of alphanumeric characters and _ (underscore). Whitespace is any mix of spaces, tabs, and linefeeds. A string is delimited by either single or double quotes and may contain whitespace. Everything else is punctuation. Some pairs of punctuation characters stick together; ==, !=, <=, >=. All other punctuation is treated as single-character tokens.

Here are lexical rules, regular expressions describing valid tokens:

 
<symbol>      ::= [A-Za-z][A-Za-z0-9_]*
<string>      ::= '[^']*'|"[^"]*";
<decimal>     ::= [0-9]+
<hexadecimal> ::= 0x[A-Fa-f0-9]+
<tritval>     ::= [ymn]
 

textdatais any number of lines of text data, terminated by a line containing a single period and newline. All lines beginning with periods must be byte-stuffed (that is, have an extra period prepended).

base64-data is any number of lines in RFC2045 base64 format, terminated by a newline or comment.

Also, note that there is a lexical-level inclusion facility. The token "source" is interpreted as a request to treat the immediately following token as a filename (string quotes are first stripped if it is a string). Upon encountering this directive, the compiler opens the file (which may be a relative or absolute pathname), and reads input from that file until EOF. On that EOF, the current input source is immediately popped back to the including file. Relative pathnames are interpreted relative to the directory of the including file.

Comments are supported, and run from a # to end-of-line.

Here is a BNF of the grammar. Following it, each language element will be described in detail.

 
;; A helpful thing to define up front...
;;
<int>     ::= <decimal> | <hexadecimal> ;; Integer literal

;; A CML system consists of a sequence of declarations.
;;
<system> ::= <declaration>*

;; A declaration may be of one of the following types:
;;
<declaration> ::= <symbols-declaration>
	      |   <property-name-declaration>
	      |   <property-declaration>
	      |   <visibility-rule>
	      |   <saveability-rule>
	      |   <menu-definition>
	      |   <choices-definition>
              |   <choicegroup-declaration>
	      |   <derive-definition>
	      |   <default-definition>
	      |   <requirement-definition>

	      |   <start-definition>
	      |   <prefix-definition>
	      |   <banner-definition>

	      |   <condition-declaration>
	      |   <warndepend-declaration>
	      |   <icon-definition>
	      |   <debug-definition>

;; A symbols definition creates configuration symbols, 
;; and associates prompt strings with them.
;;
<symbols-declaration> ::= 'menus' {<symbol> <string> 
                                    {'text' <textdata>|'like' <symbol>}?}*

;; A property declaration declares that the associated symbols should
;; have the specified property (a label in the output configuation).
;;
<property-declaration> ::= 'give' <symbol>* 'property' <symbol>

;; A propertty name declaration sets up aliases for a property
<property-name-declaration> ::= <symbol>* 'alias' <symbol>

;; A visibility rule associates a visibility predicate with symbols.
;; Optionally, it may declare that the suppressed symbols are constrained
;; in value by the predicate symbols.
;;
<visibility-rule> ::=  {'unless'|'when'} <logical> 'suppress' ['dependent'] <symbol>*;

;; A saveability rule associates a saveability predicate with symbols.
;; Optionally, it may declare that the suppressed symbols are constrained
;; in value by the predicate symbols.
;;
<saveability-rule> ::=  {'unless'|'when'} <logical> 'expose' <symbol>*;

;; A menu definition links a sequence or subtree of symbols with a 
;; menu identifier.  Subtrees generate implied dependency statements.
;;
<menu-definition> ::= 'menu' <symbol-tree>+

;; A symbol-tree is an optional label prefix followed by either a 
;; {}-enclosed list of symbol-trees or a single symbol-declaration.
<symbol-tree> ::= <label-prefix> '{' <symbol-tree>+ '}'
               |  <label-prefix> <symbol-declaration>

;; A symbol-declaration consists of a symbol name, followed by an 
;; optional type suffix.
<symbol-declaration> ::= <symbol> [<suffix>] 

;; A label prefix is any number of label bindings:
<label-prefix> ::= 
                | <symbol> ':' <label-prefix>
                | '~' <symbol> ':' <label-prefix>

;; Suffixes declare types
<suffix> ::= '?'      ;; declares trit type
           | '%'      ;; declares decimal type
           | '@'      ;; declares hexadecimal type
           | '$'      ;; declares string type


<symbol-or-subtree> ::= <symbol> <suffix>
                    |   <symbol> <suffix> 




;; A choices-menu definition links a choice of symbols with a menu identifier.
;;
<choices-definition> ::= 'choices' <symbol> <symbol>* ['default' <symbol>]

;; A choicegroup declaration constrains a group of symbols so that at most
;; one can have the y or m value.
;;
<choicegroup-declaration> ""= 'choicegroup' <symbol> <symbol>*

;; A derivation binds a symbol to a formula, so the value of that
;; symbol is always the current value of the formula.
;;
<derive-definition> ::= 'derive' <symbol> 'from' <expr>

;; A default definition sets the value a symbol will have unless it is
;; explicitly set by the user's answer to a question. It may have a 
;; range or enum specification attached.
;;
<default-definition> ::= 'default' <symbol> 'from' <expr> [<default-restrict>]

<default-restrict> ::= 'range' {<int> | {<int> '-' <int>}}+
                     | 'enum' {<symbol> '=' <int>}+

;; A requirement definition constrains the value of one or more symbols 
;; by requiring that the given expression be true in any valid configuration.
;;
<requirement-definition> ::=  {'require'|'prohibit'} <logical> 
                              ['explanation <symbol>']

;; We have to declare a start menu, for the beginning of execution
;;
<start-definition> ::= 'start' <symbol>

;; A prefix definition sets a string to be prepended to all symbols
;; when they are named in a configuration file.
;;
<prefix-definition> ::= 'prefix' <string>

;; A banner definition sets a string to used in the configurator
;; greeting line.
;;
<banner-definition> ::= 'banner' <symbol>

;; A condition statement sets a CML2 control flag or ties it to a symbol.
;;
<condition-declaration> ::= 'condition' <symbol> 'on' {<symbol>|<constant>}

;; A warndepend flags symbols that make dependents dangerous
;;
<warndepend-declaration> ::= 'warndepend' <symbol>*

;; An icon definition associates data for a graphic icon with the
;; rulebase.
;;
<icon-definition> := 'icon' <base64-data>

;; A debug definition enables debugging output.
;;
<debug-definition> ::= 'debug' <decimal>

;; An expression is a formula
;;
<expr> ::= <expr> '+' <expr>
        | <expr> '-' <expr>
        | <expr> '*' <expr>
        | <ternary>

<ternary> ::= <expr> '?' <expr> ':' <expr>
	   | <logical>

<logical> ::= <logical> 'or' <logical>
           | <logical> 'and' <logical>
           | <logical> 'implies' <logical>
           | <relational>

<relational> ::= <term> '==' <term>
              | <term> '!=' <term>
              | <term> '<=' <term>
              | <term> '>=' <term>
              | <term> '>' <term>
              | <term> '<' <term>
              | <term>
              | 'not' <relational>

<term> ::= <term> '|' <term>    ;; maximum or sum or union value 
        | <term> '&' <term>     ;; minimum or multiple or intersection value
        | <term> '$' <term>     ;; similarity value
        | <atom>

<constant> ::= <tritval>
            | <string>
            | <decimal>
            | <hexadecimal>

<atom> ::= <symbol>
        | <constant>
        | '(' <expr> ')'
 

Operators have the precedence implied by the above productions. From least to most binding, precedence classes are:

 
      1: ?:
      2: + -
      3: *
      4: implies
      5: or
      6: and
      7: not
      8: ==, !=, >=, <=, >, <
      9: &, |, $
 

Data types and classes

CML2 supports the following data types:

  • Booleans. These may have the values `y' or `n'

  • Tristates or trits. These may have the values `y', 'm', or `n'

  • Decimal integers. 32-bit signed integers with decimal I/O formatting.

  • Hexadecimal integers. 32-bit signed integers with hexadecimal I/O formatting.

  • Strings. Strings are literal data in the ASCII character set encoding.

Support for trits may be disabled at runtime. See the section called Condition statement for discussion of the condition/on declaration.

There are four classes of symbols; constant symbols, query symbols, derivation symbols, and frozen symbols.

A constant is one of the boolean/tristate literals y or m or n, or an integer literal, or a string literal.

A query symbol is an ordinary, mutable symbol with a prompt string. Each query must occur exactly once in the menu tree. Query symbols may be set by the user.

A derivation is a symbol bound to an expression. Derivation symbols cannot be set by the user, but may vary in value as the symbols in their formula change value (it may help to think of them as symbolic macros). Derived symbols have no associated prompt string and may not appear in the menu tree.

A frozen symbol is a query symbol which has been immutably bound to a particular value. Once frozen, the value of a symbol may not be changed (neither by user action nor by side effect).


Meaning of the language elements


Source statements

A source statement declares a file to be inserted in place of the source statement in the file, and treated as if the entire contents of that file were present in the current file at the point of their source statement.

Any implementation of CML2 must allow source statements to be nested to a depth of at least 15 levels. The reference implementation has no hard limit.


Symbol declarations

The body of a symbols section consists of pairs of tokens; a symbol (which may be an ordinary configuration symbol, a menu name, a message string, or an explanation string) and a prompt string. Each pair may optionally be followed by a text section declaring associated help text, or by the keyword like and a symbol specifying an existing symbol with help text.

Rationale: Having these name-to-prompt associations be separate from the dependency rules will help make the text parts of the system easier to localize for different languages. Declaring all query symbols up front means we can do better and faster sanity checks. Some symbols (derivations) are not pre-declared.


Property declarations

A property name declaration declares aliases for a given property. Usually these aliases are short (often one letter) and are intended to be embedded in menus.

Associating a property with a symbol means that property will be included in a comment following the symbol value dump on its line.

Rationale: Annotation label may be used as instructions to configuration-file postprocessors. The sets of symbols defined by properties may be used by configurators that have knowledge specific to a particular rulebase.


Visibility rules

A visibility declaration associates a visibility predicate with a set of configuration symbols. The fact that several symbols may occur on the right side of such a rule is just a notational convenience; the rule

      unless GUARD suppress SYMBOL1 SYMBOL2 SYMBOL3

is exactly equivalent to

      unless GUARD suppress SYMBOL1
      unless GUARD suppress SYMBOL2
      unless GUARD suppress SYMBOL3

Putting a menu on the right side of a visibility rule suppresses that menu and all its children. In general, suppressing a symbol also implicitly suppresses all its dependents.

If multiple visibility declarations touch a symbol on the right-hand side, the resulting test is the logical conjunction of all of them.

As a convenience,

      when GUARD suppress SYMBOL1 SYMBOL2 SYMBOL3

is syntactic sugar for

      unless GUARD==n suppress SYMBOL1 SYMBOL2 SYMBOL3

When a derived symbol is suppressed, this prevents its value from being written out to the configuration file.


Dependence

Optionally, a rule may declare that the suppressed symbols are constrained in value by the predicate symbols. That is, if there is a rule

      unless GUARD suppress dependent SYMBOL

then the value of SYMBOL is constrained by the value of GUARD in the following way:

Table 1. Effect of suppress depend

guardtritbool
yy,m,ny,n
mm,ny,n
nnn

The reason for this odd, type-dependent logic table is that we want to be able to have boolean option symbols that configure options for trit-valued ancestors. This is why the guard symbol value m permits a dependent boolean symbol (but not a dependent trit-valued symbol) to be y.

If the guard part is an expression, SYMBOL is made dependent on each symbol that occurs in a pure conjunction in the guard. Thus, if FOO and BAR and BAZ are trit symbols,

    unless FOO!=n and BAR==m suppress dependent BAZ

is equivalent to the following rules:

     unless FOO!=n and BAR==m suppress BAZ
     require BAZ <= FOO and BAZ <= BAR 

This rule, on the other hand,

    unless FOO!=n and (BAR==m or BAZ==y) suppress dependent QUUX

is equivalent to:

     unless FOO!=n and (BAR==m or BAZ==y) suppress QUUX
     require QUUX <= FOO

The compiler does not make symbols connected by disjunctions (or symbols connected by any logical-expression operator other than conjunction) into ancestors of symbols on the right-hand side.

Putting a menu on the right side of a visibility rule with `dependent' puts the constraint on all the configuration symbols in that menu. Any submenus will inherit the constraint and pass it downward to their submenus.

Dependency works both ways. If a dependent symbol is set y or m, the value of the ancestor symbol may be forced; see the section called Symbol Assignment and Side Effects for discussion.

Rationale: The syntax is unless...suppress rather than if...query because the normal state of a symbol or menu is visible. The dependent construction replaces the dep_tristate and dep_bool constructs in CML1.


Saveability rules

Normally, CML2 configurators save a symbol to the output configurator if it is either been set during the configuration session or is visible at save time.

Occasionally it is necessary to force the default of a symbol to be saved even when it is not visible at save time. For this purpose the language supports giving symbols an explicit saceability predicate:

      when GUARD1 save SYMBOL1 SYMBOL2 SYMBOL3
      unless GUARD2 save SYMBOL4 SYMBOL5 SYMBOL6

The guard expressions may be any legal expression.


Menu definitions

A menu definition associates a sequence of configuration symbols and (sub)menu identifiers with a menu identifier (and its banner string). It is an error for any symbol or menu name to be referenced in more than one menu.

If there are multiple menu definitions referring to the same menu name, the compiler builds a single menu from all of them listing their contents in the order they are compiled. This is explicitly permitted in order to allow menu add-ons in CML2 source files generated by concatenation.

Any implementation of CML2 must allow menus to be nested to a depth of at least 15 levels. The reference implementation has no hard limit.

Symbol references in menus may have suffixes which change the default boolean type of the symbol. The suffixes are as follows:

    ?      trit type
    %      decimal type
    @      hexadecimal type
    $      string type

A choices definition associates a choice of boolean configuration symbols with a menu identifier (and its banner string). It may optionally declare a default symbol to be set to y at the time the menu is instantiated; if there is no specified default, the first symbol in the menu becomes the default.

If the default symbol of a choices menu is invisible at menu instantiation time, the configurator is expected to search forward into the symbols following the default until a visible alternative is found. If a visible alternative is found, it is used. If no visible alternative is found, the behavior is undefined (but the recommended behavior is to throw an except and exit).

In a complete CML2 system, these definitions link all menus together into a single big tree, which is normally traversed depth-first (except that visibility predicates may suppress parts of it).

If the list of symbols has subtrees in it (indicated by curly braces) then the symbol immediately before the opening curly brace is declared a visibility and dependency guard for all symbols within the braces. That is, the menu declaration

    menu foo 
         SYM1 SYM2 {SYM3 SYM4} SYM5

not only associates SYM[12345] with foo, it also registers rules equivalent to

       unless SYM2 suppress dependent SYM3 SYM4

Such submenu declarations may be nested to any depth.

Normally, a symbol used as a sub-menu guard will be a bool or trit. They are also permitted to be numeric, in which case value zero is considered equivalent to boolean n and all other values are considered equivalent to boolean y.

It is perfectly legal for a menu-ID to have no child nodes. In CML2, this is how you embed text in menus, by making it the banner of a menu symbol with no children.


Choice groups

Declaring a group of logical symbols to be a choice group creates the constraint that at most one of those symbols can have the value y or m. Setting a symbol in a choicegroup to one of these values clears all other symbols in the group. It is a compile-time error for a choice group to contain symbols that are not of logical type.

Choices menus are a special case of choicegroups that are constrained always to have one choice selected.


Derivations

A derivation binds a symbol to a formula, so the value of that symbol is always the current value of the formula. Symbols may be evaluated either when a menu containing them is instantiated or at the time the final configuration file is written.

The compiler performs type inference to deduce the type of a derived symbol. In particular, derived symbols for which the top-level expression is an arithmetic operator are deduced to be decimal. Derived symbols for which the top level of the expression is a boolean operator are deduced to be bool. Derived symbols for which the top level of the expression is a trit operator are deduced to be trit.

Derived symbols are never set directly by the user and have no associated prompt string.


Defaults

A default definition sets the value a symbol will have until it is explicitly set by the user's answer to a question. The right-hand side of a default is not limited to being a constant value; it may be any valid expression.

Default expressions are treated as symbolic macros to be evaluated either when a menu containing the defaulted symbol is instantiated, or at the time the final configuration file is written, or during the evaluation of any formula (such as a derivation or visibility predicate) referring to the defaulted symbol.

Thus, the evaluated default of a symbol may differ depending on the timing of evaluation relative to other symbol settings (in particular, of the default expression's component symbols). This is intentional. The compiler detects circularities resulting from cycles of default expressions or derivations that would cause infinite recursion.

If a decimal or hexadecimal symbol is defaulted from a symbol or expression that has bool or trit values, the values y and m are cast to 1 and the value n is cast to 0. If a boolean or trit symbol is defaulted from a decimal- or hexadecimal-valued expression, a value of zero is cast to n and all other values are cast to y. The results of mixing other types are undefined, should be considered accidents of the implementation, and should not be relied on.

If a non-string symbol is not explicitly defaulted, it gets the zero value of its type; n for bools and trits, 0 for decimal and hexadecimal symbols. String symbols always require a default.

The optional range or enumeration part may be used to constrain legal values for decimal or hexadecimal-valued symbol. A default declaration may have either a range or an enumeration part, but not both.

A range specification consists of any number of either single values or paired upper and lower bounds separated by a dash, interpreted as inclusive ranges. The symbol has a legal value if it either matches a specified single value or is contained in one of the intervals.

An enumeration consists of a series of pairs separated by '='. Each pair associates a symbol (which must have been previously declared in an explanation statement) with an integer value. The symbol must match one of the values. The front end may use the prompt value of the symbol in each pair to stand in for the value (e.g. when generating a pull-down menu of alternatives.)


Requirements

Requirements as sanity checks

A requirement definition constrains the value of one or more symbols by requiring that the given expression be true in any valid configuration. All constraints involving a given configuration symbol are checked each time that symbol is modified. Every constraint is checked just before the configuration file is written.

If the optional explanation clause is present, the string associated with the specified symbol is taken to be an explanation that the front end can use if when the constraint is violated. Otherwise, the explanation will be a display of the constraint expression.

It is up to individual CML2 front ends to decide how to handle constraint violations. Here are some possible policies:

  • Complain and die. Not recommended, but perhaps appropriate for a batch-mode front end.

  • Conservative recovery: Disallow the modification that would violate the constraint. (Thus, earlier answers have priority over later ones.) Note that front ends using this policy should back out side-effects of symbol changes as well as the change to the primary symbol.

  • Flag-and-continue: visibly flag all symbols involved in a constraint violation (and unflag them whenever a constraint violation is fixed). Require the user to resolve all constraint violations before the configuration file is saved.

  • Backtracking: Present all the menus involved in the constraint. Accept modifications of any of them, but do not allow the modifications to be committed until all constraints are satisfied.

The reference implementation uses conservative recovery, with side-effects being backed out as well.

A prohibit definition requires that the attached predicate not be true. This is syntactic sugar, added to accommodate the fact that human beings have trouble reasoning about the distribution of negation in complex predicates.


Using requirements to force variables

Requirements have a second role. Certain kinds of requirements can be used to deduce values for variables the user has not yet set; the CML2 interpreter does this automatically.

Every time a symbol is changed, the change is tried on each declared constraint. The constraint is algebraically simplified by substituting in constant, derived and frozen symbols. If the simplified constraint forces an expression of the form A == B to be true, and either A is a query symbol and B is a constant or the reverse, then the assignment needed to make A == B true is forced.

Thus, given the rules

derive SPARC from SPARC32 or SPARC64
require SPARC implies ISA==n and PCMCIA==n and VT==y and VT_CONSOLE==y
    and BUSMOUSE==y and SUN_MOUSE==y and SERIAL==y and SERIAL_CONSOLE==y
    and SUN_KEYBOARD==y

when either SPARC32 or SPARC64 changes to y, the nine assignments implied by the right side of the second rule will be performed automatically. If this kind of requirement is triggered by a guard consisting entirely of frozen symbols, all the assigned symbols become frozen.

If A is a boolean or trit symbol and B simplifies to a boolean or trit constant (or vice-versa), assignments may be similarly forced by other relationals (notably A != B, A < B, A > B, A <= B, and A >= B). If forcing the relational to be true implies only one possible value for the symbol involved, then that assignment is forced.

Note that whether a relational forces a unique value may depend on whether trits are enabled or not.


Start declaration

The start definition specifies the name of the root menu of the hierarchy. One such declaration is required per CML2 ruleset.


Prefix declaration

A prefix declaration sets a string to be prepended to each symbol name whenever it is written out to a result configuration file. This prefix is also ignored when present as a prefix of symbol names, whether in a rule file or when read in from a defconfig file.

Rationale: This was added so the CML2 rule system for the Linux kernel would not have to include the common CONFIG_ prefix, which adds bulk and makes reading the rules file visually confusing. The alternative of wiring that prefix into the code would compromise CML2's potential usefulness for other applications. Prefix-stripping in rule files was added as a backward-compatibility hack to permit names such as CONFIG_3C515 that have leading numerics and would be treated as numbers if given without prefix.


Banner declaration

A banner definition sets the menu id banner string to used in the configurator greeting line. The string attached to the specified menu id should identify the system being configured.

Rationale: As for the prefix string.


Condition statement

The condition statement ties a CML2 feature flag to a query symbol; that is, the value of the feature flag is the value of the symbol. The initial value of the flag when a rulebase is read in is simply the associated symbol's default. If there is no symbol associated with the the flag, the flag's value is n.

The condition value may also be a constant, in which case the value of the feature flag is set to that constant.


The trit flag

A "trits" flag is supported. When this flag is n, trit-valued symbols are treated as booleans and may only assume the values y and n.

When this flag is y, modules are enabled and questions involving them will be issued normally.

If the flag is not tied to a symbol or constant, its value is y.

This flag may affect the front end's presentation of alternatives for trit-valued symbols. It also affects forcing of ancestor symbols. When the trits flag is m or y, setting a boolean symbol only forces its trit ancestors to the value m; when trits is off, they are forced to y. See the section called Symbol Assignment and Side Effects for discussion.


The nohelp flag

A "nohelp" flag is supported. When this flag is n, symbols without associated help are invisible. When it is y, symbols without help are visible. If the flag is not tied to a symbol, its value is y.

Rationale: This flag is intended to be tied to a user-visible policy symbol that sets some kind of expert level.


The expert flag

A "expert" flag is supported. When this flag is n, the user is presumed to be a novice. When it is y, the user is presumed to be an expert. If the flag is not tied to a symbol, its value is n.

Rationale: This flag is intended to be used by configurator front ends to set UI policy. In the normal case, it will be tied to some policy symbol in the rulebase.


Warndepend declaration

The warndepend declaration takes a list of symbol names. All dependents of each symbol have their prompts suffixed with the name of the symbol in parentheses to indicate that they are dependent on it.

Rationale: Added to support the EXPERIMENTAL symbol in the Linux kernel configuration. This declaration is better than tracking experimental status by hand because it guarantees that subsidiary symbols dependent on an experimental feature will always be flagged for the user.


Icon declaration

An icon declaration associates graphic data (encoded in RFC2045 base64) with the rulebase. Front ends may use this data as an identification icon.

The reference front-end implementation uses the image to iconify the configurator when it is minimized while running in X mode.

The reference front-end accepts the image in GIF format. In the future (when underlying library support permits) PNG support will be added and GIF removed.


Debug

This declaration enables debugging output from the compiler (it has no effect on front-end behavior). It takes an integer value and uses it to set the current debug level. It may change or be removed in future releases.


Expressions

All arithmetic is integer. The compiler permits some kinds of type promotion, described below.

For purposes of the relational operators, trit values are strictly ordered with y > m > n.

Arithmetic operations + - * / have the expected semantics on decimal and hexadecimal value.

Boolean logical expressions may be used as parts of integer-valued formulas (e,g in derivations and constraints). The value of true is 1, and of false is 0.

It is a compile-time error to apply the logical operators or/and/implies to trit or numeric values. Also, expressions occurring in guards (in unless/suppress, or require/prohibit declarations) must yield a value of boolean type. The compiler does type propagation in expressions to check these constraints.

The purpose of these restriction is to enable compile-time detection of situations where confusion of trit or numeric with boolean values might induce subtle errors. For the same reason, if the symbol FOO is trit-valued it is a compile-time error to say just "FOO" in an expression, as opposed to "FOO!=n" or some other more explicit relational.

Thus, because the symbol SCSI is trit-valued:

    unless SCSI suppress A2091_SCSI

is illegal and will raise an error. Write an unambiguous test instead:

    unless SCSI>=m suppress A2091_SCSI

The obvious booleans operations (and, or) are supported; they are commutative and associative. An 'implies' operation is also supported:

    FOO implies BAR  <=>  not (FOO and (not BAR))

The implies operation is neither commutative nor associative.

The usual relational tests (==, !=, >=, <=, >, <) are supported. Relationals bind more tightly than boolean operators, so FOO!=n and BAR==m behaves as expected. Additionally, and binds more tightly than or, so that FOO or BAR and BAZ is FOO or (BAR and BAZ).

Ternary-select is available as in C. The value of a ? b : c is b if a is true, c otherwise.

The following additional ternary-logic operations are available. It is an error to apply these to operands with types other than bool or trit.

Max or union; notation |. Here is a truth table:

Table 2. Union

|ymn
yyyy
mymm
nymn

Min or intersection; notation &. Here is a truth table:

Table 3. Intersection

&ymn
yymn
mmmn
nnnn

Similarity; notation $. Here is a truth table:

Table 4. Similarity

$ymn
yynn
mnmn
nnnn

The operator precedence implied by the BNF above is implemented in the parser.


Symbol Assignment and Side Effects

Setting a symbol's value may have side-effects on other symbols in two ways.

First, it may trigger a change in other variables through explicit requirements. See the section called Using requirements to force variables for discussion.

Second, each symbol has two implicit lists associated with it: of symbols it depends on (ancestors) and symbols that depend on it (dependents). Whenever a symbol is changed, any side-effects are propagated through those lists. Changing the value of the symbol upward (n to m, or m to y) may change the value of ancestors; changing it downward (y to m or m to n) may affect the value of dependents.

See also the section called Dependence for discussion of the two syntactically different ways dependencies can be created.

CML2 interpreters are required to implement all-or-nothing side effects; that is, after an assignment, either the assignment and all its side-effects have been performed, or (in the event the new values would violate a requirement) none of them are.

The reference implementation achieves this by implementing two-phase commit; the assignment and its side-effects can be made tentatively, constraints checked, and then either committed or rolled back.

Side-effect bindings remain linked to the symbol whose value change triggered them, and are backed out whenever that symbol is changed again. Backing out a side-effect may expose previous side-effects on a symbol from other, earlier bindings.

To see how this works, consider the following sequence of actions given the constraints A: (FOO==y implies BAR==y) and B: (BAZ==y implies BAR==n):

  1. User sets FOO=y.

    1. As a side-effect, this sets BAR=y through constraint A

  2. User sets BAZ=y.

    1. As a side-effect, this sets BAR=n constraint B

    2. BAR==n implies FOO=n through constraint A

  3. User sets an unrelated symbol QUUX=y.

  4. User sets BAZ=n.

    This does not have a direct side-effect on BAR. However, since the value BAZ has changed, the side-effects FOO=n and BAR=n of the last BAZ binding is backed out. The visible value of BAR is again y.

The easiest way to understand this is by visualizing the variable-binding transactions as a stack. After the first step, the stack looks like this:

1: FOO=y:         FOO=y BAR=y

After the second step:

2: BAZ=y:         FOO=n BAR=n BAZ=y
1: FOO=y:         FOO=y BAR=y

The third step adds another unrelated binding:

3: QUUX=y:                          QUUX=y
2: BAZ=y:         FOO=n BAR=n BAZ=y
1: FOO=y:         FOO=y BAR=y

The fourth step both adds a binding and backs out the old one:

4: BAZ=n:                     BAZ=n               
3: QUUX=y:                          QUUX=y
1: FOO=y:         FOO=y BAR=y

The reference implementation journals all side-effects and always looks for the most recent binding of a symbol (highest in the stack) when evaluating it.


Order Dependencies

In general, the relative order of CML2 declarations does not change their effect. The prefix declaration, however, is used in interpreting symbol names, so it must precede symbol declarations.

There is a subtler kind of order dependency possible between constraints. Consider the following set of constraints:

1: require FOO==y implies DEP1==y
2: require DEP1 implies BAR==n
3: require FOO==y and BAR==y implies DEP2==n

Now suppose we set FOO to y. Then the values that variables get forced to will be different depending on the order in which the theorem-prover finds the constraints:

1, 2, 3: DEP1==y, BAR==n, DEP2 unchanged.
1, 3, 2: DEP1==y, BAR==n, DEP2==n

In practice this should seldom be a difficulty, but it is well to bear such possibilities in mind when writing complex constraints.


CML2 configuration file format


Output format

The output file consists of a series of lines in the format of either Unix shell variable assignments or directives.

Each ordinary (non-directive) line is led with a symbol name (prefixed if there is a prefix declaration in the rulebase), continues with a =, and finishes with a value. The value may be y, n, or m for boolean or tristate symbols. It may be a quoted string for string literals, or an (unquoted) numeric literal for decimal or hexadecimal symbols.

The value of a symbol will be written if it has either been set by user action or is visible at configuration-save time.

In the reference implementation, symbols are written in depth-first traversal order. Derived symbols are written after the query symbols; each derived symbol is written out if any of the symbols in its formula has been set.

Directives begin with $$. There are currently two directives defined: __freeze and __commit. These cause a commit-with-freeze and a commit-without-freeze, respectively, of all bindings read since the last directive (or the start of file if there were no previous directives).

Lines beginning with # are comments. Postprocessing tools should not attempt to interpret them.


Change history

0.1 -- 24 May 2000 Original CML2 specification.
0.2.0 -- 31 May 2000 Removed whenever/sets from the language. Everything is now done with deduction.
0.2.1 -- 4 June 2000 Added warndepend.
0.3.0 -- 9 June 2000 Deduction algorithm rewritten and documented in section V.
0.4.0 -- 20 June 2000: Value stacking is implemented.
0.5.0 -- 26 June 2000: Fuller support for ranges. Spec format converted to DocBook.
0.6.0 -- 30 June 2000: Eliminated a lexical class.
0.7.0 -- 6 July 2000: The "options" directive was removed.
0.7.0 -- 12 Aug 2000: Added the `explanation' declaration.
0.9.2 -- 15 Jan 2001: Reference manual split out of the paper.
0.9.8 -- 29 Mar 2001: Module-suppression feature added.
1.0.0 -- 9 April 2001: Ready for production release.
1.2.3 -- 23 April 2001: Added -B option.
1.2.5 -- 25 April 2001: Revisions following comments by Greg Banks.
1.3.3 -- 28 April 2001: Help text sections introduced in menus and symbols declarations. The `helpfile' declaration is gone.
1.6.1 -- 16 June 2001: New section on declaration order.
1.6.3 -- 21 June 2001: Menus may be concatenated from multiple declarations.
1.8.5 -- 14 Nov 2001: It's possible to condition a flag on a constant.
1.9.1 -- 25 Nov 2001: Derived symbols can be suppressed.
1.9.4 -- 1 Dec 2001: Default of a choices menu becomes the specified default if it is visible, the first visible symbol after it otherwise.
1.9.10 -- 16 Dec 2001: Compiler now handles suppress-depend guards that are not pure conjunctions.
1.9.11 -- 19 Dec 2001: Added 'like' keyword conjunctions.
2.0.0 -- 2 Jan 2002: Replaced `private' with `label/with'. Added $$freeze and $$commit directives. Added 'choicegroup'. Removed most ordering constraints.
2.2.0 -- 14 Jan 2002: Added `save' declaration. Removed vitality flag.
2.3.0 -- 3 Feb 2002: The `menus' and `explanations' declarations are subsumed in the `symbols' declaration.