update documentation for K 3.4 release

INSTALL → INSTALL.md

@@ -1,27 +1,29 @@
 Here are instructions for installing K from the release zip/tgz archive.
 Users who checked out the sources should follow the instructions in src/README.
 
-1. Prerequisites
-Java Runtime Edition (requires JRE7 or higher)
-  http://java.com/en/download/index.jsp
-To make sure java is installed properly, call "java" in a terminal.
-
-2. Install
-Unzip this directory in your preferred location.  For convenient usage,
-update your $PATH with <preferred-location>/k/bin.
-
-3. Test
-Go to one of the examples (say k/tutorial/2_languages/1_simple/1_untyped/).
-Assuming k/bin is in your $PATH, you can compile definitions using 
-the 'kompile simple-untyped.k' command.
-To execute a program you can use 'krun tests/diverse/factorial.simple'.
-
-4. (Optional) To use the pdf backend, a relatively recent installation 
-of Latex is required.  Besides basic packages, the following (texlive)
-packages are needed: 
-  bera, bezos, bookmark, datetime, ec, etoolbox, fancybox, fancyvrb, import, 
-  listings, marginnote, microtype, ms, pdfcomment, pgf (up-to-date), preview, 
-  soul, stmaryrd, times, titlesec, ucs, url, xcolor, and xkeyval.
+1. Prerequisites:
+  * Java Runtime Edition version 7 or higher (http://java.com/en/download/index.jsp)
+  * To make sure java is installed properly, call `java` in a terminal.
+
+2. Install:
+  * Unzip this directory in your preferred location.  For convenient usage,
+    update your $PATH with <preferred-location>/k/bin.
+
+3. Test:
+  * Go to one of the examples (say k/tutorial/2_languages/1_simple/1_untyped/).
+    Assuming k/bin is in your $PATH, you can compile definitions using 
+    the `kompile simple-untyped.k` command.
+    To execute a program you can use `krun tests/diverse/factorial.simple`.
+
+4. (Optional) Latex:
+  * To use the pdf backend, a relatively recent installation 
+    of Latex is required.  Besides basic packages, the following (texlive)
+    packages are needed: 
+  * bera, bezos, bookmark, datetime, ec, etoolbox, fancybox, fancyvrb, import, 
+    listings, marginnote, microtype, ms, pdfcomment, pgf (up-to-date), preview, 
+    soul, stmaryrd, times, titlesec, ucs, url, xcolor, and xkeyval.
+
+--------------------------------------------------------------------------
 
 We present some instructions for installing TeX Live on Unix-like machines.
 
@@ -41,12 +43,12 @@ in the prerequisites. Note however that our LaTeX macros rely on a quite
 recent version of the pgf package. To make sure you have the latest version
 of this package you can upgrade it using the TeX Live package manager.
 
-    # tlmgr update pgf 
+    $ tlmgr update pgf 
 
 If using a partial TeX Live installation which does not provide all the 
 TeX Live packages specified above, these can be installed with the command:
 
-    # tlmgr install  bera bezos bookmark datetime ec etoolbox fancybox \
+    $ tlmgr install  bera bezos bookmark datetime ec etoolbox fancybox \
                      fancyvrb import listings marginnote microtype ms \
                      pdfcomment pgf preview soul stmaryrd times titlesec ucs \
                      url xcolor xkeyval 

LICENSE → LICENSE.md

@@ -24,17 +24,17 @@ use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 of the Software, and to permit persons to whom the Software is furnished to do
 so, subject to the following conditions:
 
-    * Redistributions of source code must retain the above copyright notice,
-      this list of conditions and the following disclaimers.
+* Redistributions of source code must retain the above copyright notice,
+  this list of conditions and the following disclaimers.
 
-    * Redistributions in binary form must reproduce the above copyright notice,
-      this list of conditions and the following disclaimers in the
-      documentation and/or other materials provided with the distribution.
+* Redistributions in binary form must reproduce the above copyright notice,
+  this list of conditions and the following disclaimers in the
+  documentation and/or other materials provided with the distribution.
 
-    * Neither the names of the K Team, the University of Illinois at
-      Urbana-Champaign, the University Alexandru-Ioan Cuza, nor the names of
-      its contributors may be used to endorse or promote products derived from
-      this Software without specific prior written permission.
+* Neither the names of the K Team, the University of Illinois at
+  Urbana-Champaign, the University Alexandru-Ioan Cuza, nor the names of
+  its contributors may be used to endorse or promote products derived from
+  this Software without specific prior written permission.
 
 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
@@ -63,10 +63,16 @@ licenses, and/or restrictions:
 
 ---------------------------------------
 Maude (http://maude.cs.uiuc.edu) is licensed under the GPL license.
+
 Stratego (http://strategoxt.org) is licensed under the LGPL license.
+
 Xstream (http://xstream.codehaus.org/) is licensed under the BSD license.
+
 XML Pull (http://www.xmlpull.org) API is free.
-Xpp3 (http://www.extreme.indiana.edu/xgws/xsoap/xpp) is licensed under Indiana
+
+Xpp3 (http://www.extreme.indiana.edu/xgws/xsoap/xpp) is licensed under Indiana 
 University Extreme! Lab Software License.
+
 KXML2 (http://kxml.sourceforge.net/kxml2/) is licensed under the BSD license.
+
 SSCTarjan (https://github.com/indy256/codelibrary) is licensed under the Unlicense.

README.md

@@ -0,0 +1,43 @@
+K tool, version 3.4
+-------------------
+
+K is a rewrite-based executable semantic framework in which programming 
+languages, type systems, and formal analysis tools can be defined using
+_configurations_, _computations_, and _rules_. Configurations organize
+the state in units called _cells_, which are labeled and can be nested.
+Computations carry _computational meaning_ as special nested list
+structures sequentializing computational tasks, such as fragments of
+program. Computations extend the original language abstract syntax. K
+(rewrite) rules make it explicit which parts of the term they read-only,
+write-only, read-write, or do not care about. This makes K suitable for
+defining truly concurrent languages even in the presence of sharing.
+Computations are like any other term in a rewriting environment:
+they can be matched, moved from one place to another, modified, or deleted.
+This makes K suitable for defining control-intensive features such as 
+abrupt termination, exceptions, or call/cc.
+
+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), or refer to the
+website, which contains video tutorials, at http://www.kframework.org/.
+
+**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 changed!
+Type `--help` with any of these to see the new options, or see the changelog
+for more details.
+
+New features
+------------
+
+For a list of high-level changes since the previous release, please refer to
+the file CHANGELOG in the current directory.
+
+Developers
+----------
+
+See src/README

src/README → src/README.md

@@ -1,73 +1,72 @@
- 
-1. This is a readme file for the developers.
+This is a readme file for the developers.
 
-2. Prerequisites
+# Prerequisites
 
-2.1 Java Development Kit (required JDK7 or higher)
+## Java Development Kit (required JDK7 or higher)
 You can follow the instructions here: 
 http://docs.oracle.com/javase/7/docs/webnotes/install/index.html depending on 
 the type of your machine.
 
-To make sure that everything works you should be able to call 'java' and
-'javac' from a Terminal.
+To make sure that everything works you should be able to call `java` and
+`javac` from a Terminal.
 
-2.2 Apache ANT
+## Apache ANT
 Linux and Mac:
-    Most likely you will already have it.
+* Most likely you will already have it.
 Windows:
-    Go to http://ant.apache.org/bindownload.cgi and download the zip with the 
+*   Go to http://ant.apache.org/bindownload.cgi and download the zip with the 
     binary distribution. Unzip it in your desired location and follow the 
-    installation instructions from the 'INSTALL' file.
+    installation instructions from the INSTALL file.
 
-Ant usually requires setting an environment variable 'JAVA_HOME' pointing
+Ant usually requires setting an environment variable `JAVA_HOME` pointing
 to the installation directory of the JDK (not to be mistaken with JRE).
 
-2.3 Git - command line
+## Git - command line
 Having a GUI client is not enough. Most distributions have an installation
 option to make git accessible in the command line too.
 
-You can test if it works by calling 'ant' in a Terminal.
+You can test if it works by calling `ant` in a Terminal.
 
-3. Install
-Checkout this directory in your desired location and call 'ant' from the main
+# Install
+Checkout this directory in your desired location and call `ant` from the main
 directory to build the .jar binaries. For convenient usage, you can update
 your $PATH with <checkout-dir>/bin (strongly recommended, but optional).
 
-4. Work on Java code
+# Work on Java code
 We here only give instructions for Eclipse, but similar instructions apply
 for other IDEs.  Open Eclipse and set your workspace to src/javasources.  Go to
 File->Import->General->Existing projects into workspace, and select
 the project src/javasources/KTool.  If you need to edit SDF-related code,
 you should install the Spoofax plugin and then also import
 src/javasources/parsers/Concrete.
 
-5. Work on Maude code
+# Work on Maude code
 Modify the Maude files found in lib/maude/lib. No need for recompilation.
 
-6. Build the final release directory/archives
-Call 'ant release' in the base directory.  This will create a k directory in
+# Build the final release directory/archives
+Call `ant release` in the base directory.  This will create a k directory in
 trunk containing the release distribution and two archives k-latest.(zip|tgz)
 
-You can use 'ant release -Dversion="3.0"' to create a tagged release.
+You can use `ant release -Dversion="3.4"` to create a tagged release.
 
-7. Compiling definitions and running programs
+# Compiling definitions and running programs
 Assuming k/bin is in your path, you can compile definitions using
-the 'kompile' command.  To execute a program you can use 'krun'.
+the `kompile` command.  To execute a program you can use `krun`.
 
-8. Troubleshooting
+# Troubleshooting
 Common error messages:
 
-- Unable to find a javac compiler;
+- `Unable to find a javac compiler;
   com.sun.tools.javac.Main is not on the classpath.
-  Perhaps JAVA_HOME does not point to the JDK.
-+ Make sure JAVA_HOME points to the JDK and not the JRE directory.
+  Perhaps JAVA_HOME does not point to the JDK.`
+  + Make sure `JAVA_HOME` points to the JDK and not the JRE directory.
 
--  Execute failed: java.io.IOException: Cannot run program "git":
-   CreateProcess error=2, The system cannot find the file specified
-+  Git is not accessible in the command line. Please reinstall git and make
-   make sure to check to option to make it available in the command line.
+-  `Execute failed: java.io.IOException: Cannot run program "git":
+   CreateProcess error=2, The system cannot find the file specified`
+   +  Git is not accessible in the command line. Please reinstall git and make
+      make sure to check to option to make it available in the command line.
 
 Sometimes javac dependency resolution fails to recognize changed files and
-would fail to build. Try 'ant clean' and rebuild the entire project.
+would fail to build. Try `ant clean` and rebuild the entire project.
 
 If that still doesn't work, please contact a K developer.