Difference between revisions of "Maude download and installation"

From The Maude System
Jump to: navigation, search
Line 8: Line 8:
 
==  Core Maude 3.0 ==
 
==  Core Maude 3.0 ==
  
Click on the appropriate link below to download the collection of binaries, or click the source link to download and compile the sources yourself.
+
Maude 3.0 comes with one of the SMT solvers Yices or CVC. Click on the appropriate link below to download the collection of binaries, or click the source link to download and compile the sources yourself.
  
* [[Media:Maude-2.7.1-linux.zip|Maude 2.7.1 for Linux64]]
+
* [[Media:Maude-3.0+yices2-linux.zip|Maude 3.0 (with Yices 2) for Linux64]]
* [[Media:Maude-2.7.1-osx.zip|Maude 2.7.1 for Mac OS X]]
+
* [[Media:Maude-3.0+yices2-osx.zip|Maude 3.0 (with Yices 2) for Mac OS X]]
* [[Media:Maude-2.7.1.tar.gz|Maude 2.7.1 source files]]
+
* [[Media:Maude-3.0+cvc4-linux.zip|Maude 3.0 (with CVC 4) for Linux64]]
 +
* [[Media:Maude-3.0+cvc4-osx.zip|Maude 3.0 (with CVC 4) for Mac OS X]]
 +
* [[Media:Maude-3.0.tar.gz|Maude 3.0 source files]]
  
To install from one of the above binaries, simply extract the downloaded zip file.This generates the directory maude/ with the following files in it:
+
To install from one of the above binaries, simply extract the downloaded zip file.This generates the folder with the following files in it:
 
   linear.maude
 
   linear.maude
 
   machine-int.maude
 
   machine-int.maude
   maude.[linux64|darwin64]
+
   maude-[CVC4|Yices2].[linux64|darwin64]
 
   metaInterpreter.maude
 
   metaInterpreter.maude
 
   model-checker.maude
 
   model-checker.maude
Line 23: Line 25:
 
   socket.maude
 
   socket.maude
 
   term-order.maude
 
   term-order.maude
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.
+
  smt.maude
 +
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude-CVC4.linux64</tt>, <tt>maude-CVC4.darwin64</tt>, <tt>maude-Yices2.linux64</tt> or <tt>maude-Yices2.darwin64</tt>.
  
== Full Maude 2.7.1 ==
+
== Full Maude 3.0 ==
  
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-2.7.1.zip|Full Maude 2.7.1]] and save it into the Core Maude directory.
+
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-3.0.zip|Full Maude 3.0]] and save it into the Core Maude directory.
  
 
== Maude manual and primer ==
 
== Maude manual and primer ==
  
The manual for Maude 2.7.1 is available in [[Media:Maude-2.7.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/manual271/maude-manual.html HTML].  
+
The manual for Maude 3.0 is available in [[Media:Maude-3.0-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/manual30/maude-manual.html HTML].  
The examples in the manual and in the book All About Maude is also available [[Media:Maude-2.7.1-manual-book-examples.zip|here]].
+
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.0-manual-book-examples.zip|here]].
  
The primer for Maude 2.0.1 (but mostly applicable for later versions too) is available [[Maude 2 Primer and Examples|here]].
+
== Change list from Maude 2.7.1 to 3.0 ==
  
== Change list from Maude 2.7 to 2.7.1 ==
+
* Symbolic reachability analysis of concurrent systems using narrowing,
 
+
* A strategy language for controlling rewriting,
* Unification modulo Associativity is now partially supported.
+
* External objects that allow flexible interaction of Maude object-based concurrent systems with the external world (including sockets, files, standard streams and meta-interpreters),
* Some bugs fixed.
+
* Parameterized views,
 +
* A connection to SMT solvers CVC 4 and Yices 2,
 +
* Some bugs fixed, and
 
* Some improvements in syntax error detection and recovering.
 
* Some improvements in syntax error detection and recovering.
  

Revision as of 23:44, 20 December 2019

Maude 3.0 runs on many Unix variants, including Linux.

In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. In any case, please consider subscribing to the Maude users mailing list, as this is also the mechanism by which we will make announcements about the system.

The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.

Core Maude 3.0

Maude 3.0 comes with one of the SMT solvers Yices or CVC. Click on the appropriate link below to download the collection of binaries, or click the source link to download and compile the sources yourself.

To install from one of the above binaries, simply extract the downloaded zip file.This generates the folder with the following files in it:

  linear.maude
  machine-int.maude
  maude-[CVC4|Yices2].[linux64|darwin64]
  metaInterpreter.maude
  model-checker.maude
  prelude.maude
  socket.maude
  term-order.maude
  smt.maude

Depending on your system you can now run Maude by starting the appropriate executable file: maude-CVC4.linux64, maude-CVC4.darwin64, maude-Yices2.linux64 or maude-Yices2.darwin64.

Full Maude 3.0

Full Maude is written in Maude, and is thus platform-independent. Download Full Maude 3.0 and save it into the Core Maude directory.

Maude manual and primer

The manual for Maude 3.0 is available in PDF format and in HTML. The examples in the manual and in the book All About Maude is also available here.

Change list from Maude 2.7.1 to 3.0

  • Symbolic reachability analysis of concurrent systems using narrowing,
  • A strategy language for controlling rewriting,
  • External objects that allow flexible interaction of Maude object-based concurrent systems with the external world (including sockets, files, standard streams and meta-interpreters),
  • Parameterized views,
  • A connection to SMT solvers CVC 4 and Yices 2,
  • Some bugs fixed, and
  • Some improvements in syntax error detection and recovering.

(If you use XEmacs, then you might find the Maude mode for XEmacs written by Kai Brünnler or the Maude mode written by Ellef Gjelstad useful. Extract the mode using the command "gunzip -c maude-mode.tar.gz | tar -xvf -" and follow instructions in maude-mode/README. Note that the Maude mode does not run under GNU Emacs. If you are using Emacs 24 please consider to use the maude-mode written by Santiago Saavedra [1]. Please see the README for details. If you are interested in the Eclipse development environment, please, take a look at the MOMENT project web site.)