README

K tool, version 3.0

K is a framework for programming language design and executable semantics.
This distribution contains a tool prototype which implements many of K's
features.  For more on the K framework and how to use the current tool,
go to k/tutorial (start with the README file there).

NOTE: This README file contains information regarding the stable release of
the K tool indicated in the title above, regardless of whether it came with
the release itself or with subsequent nightly/latest builds.  This file is
updated only when new stable versions are officially released.

WARNING: The command line options for kompile, krun, kast and ktest have
recently (starting with version 'jenkins-k-framework-git-359') changed!
Type --help with any of these to see the new options.  A list of changes is
here: https://github.com/kframework/k/wiki/Command-Line-Option-Changes.

What is new (from v2.7)
-----------------------

* The front-end is now implemented completely in Java (previously it was
implemented in a combination of Perl and Maude), making use of SDF (as
distributed with the Spoofax system).

Because the parser has changed, the syntax of K definitions has changed, too:

1. Modules and files:

require "filename.k" // require the contents of another file found in the
                     // current directory, or the 'include' directory.

module MODULE-NAME
  imports INCLUDED-MODULE

endmodule // in one word

2. Use priorities instead of precedence:
               | Exp "*" Exp
               > Exp "+" Exp

3. Binary mixfix operators can be disambiguated with associativity attributes:
  syntax Exp ::= Exp "*" Exp [left]
               > left:
               	 Exp "+" Exp [left]
               | Exp "-" Exp [left]
               > non-assoc:
               	 Exp "=" Exp [right]

4. You can use bracket productions to override priorities:
               | "(" Exp ")"            [bracket]

5. The scope of a variable in k3 is restricted to each rule.  In k2 it was the
module.  As a result, the sort of each variable should be specified in each
rule in which it is used.  If not specified, it is automatically assumed K.

6. The only accepted comments are // ... for one line comments and /* ... */
for multiline ones. Latex comments remain the same:
               //@ ...
               /*@ ... */
               //! ...
               /*! ... */

Developers
----------

See src/README