Difference between revisions of "Maude download and installation"

From The Maude System
Jump to: navigation, search
(Created the download page)
 
m (Change list from Maude 3.0 to 3.1: Fix link to Emacs' maude-mode)
 
(26 intermediate revisions by 3 users not shown)
Line 1: Line 1:
The new Maude runs on many Unix variants, including Linux. If you are attempting to install it on Microsoft Windows,
+
Maude 3.1 runs on many Unix variants, including Linux.  
please read the separate [[Maude on Microsoft Windows|section]].
+
 
 
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 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 Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make important announcements about the system.
+
In any case, please consider subscribing to the [[Maude Mailing Lists|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.
+
The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.
  
<small>(If you use [http://www.xemacs.org/ XEmacs], then you might find the [[Media:Maude-mode.tar.gz|Maude mode]] for XEmacs
+
==  Core Maude 3.1 ==
written by [http://www.iam.unibe.ch/~kai/ Kai Br&uuml;nnler] or
+
the [[Media:Maude-mode2.el.zip|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. Please see the README for details.
+
If you are interested in more development environments please take a look at the [http://moment.dsic.upv.es/ MOMENT] project web site.)</small>
+
  
==  Core Maude 2.6 ==
+
Maude 3.1 comes with the SMT solver Yices2. Click on the appropriate link below to download the collection of binaries, or click the source link to download and compile the sources yourself. If you wish to compile Maude with CVC4, please, read the instructions in the compressed file with the sources.  
  
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-3.1-linux.zip|Maude 3.1 for Linux64]]
 +
* [[Media:Maude-3.1-macos.zip|Maude 3.1 macOS]]
 +
* [[Media:Maude-3.1.tar.gz|Maude 3.1 source files]]
  
* [[Media:Maude-2.6.tar.gz|Linux on Intel x86, x86-64 and MacOSX on Intel]] (Note: This has been tested only on Leopard and Tiger. Panther and Jaguar users should compile a binary from source.)
+
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:
* [[Compiling Maude from source|Sources]]
+
   file.maude
 
+
   linear.maude
To install from one of the above binaries, you need GNU gzip and tar. Simply extract the binary as follows: In a Unix shell, type
+
  gunzip maude.tar.gz
+
  tar -xvf maude.tar
+
This generates the directory maude/ with the following files in it:
+
   socket.maude
+
   maude.intelDarwin
+
 
   machine-int.maude
 
   machine-int.maude
 +
  maude.[linux64|darwin64]
 
   metaInterpreter.maude
 
   metaInterpreter.maude
  linear.maude
 
 
   model-checker.maude
 
   model-checker.maude
  maude.linux
 
 
   prelude.maude
 
   prelude.maude
 +
  process.maude
 +
  socket.maude
 +
  smt.maude
 
   term-order.maude
 
   term-order.maude
  maude.linux64
+
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.
Depending on your system you can now run maude by starting the appropriate executable file: <tt>maude.linux</tt>, <tt>maude.linux64</tt> or <tt>maude.intelDarwin</tt>.
+
  
== Full Maude 2.6 ==
+
== Full Maude 3.1 ==
  
Full Maude is written in Maude, and is thus platform-independent. Download the new [[Media:full-maude.zip|Full Maude]] and move it into the Core Maude directory (<tt>/usr/local/maude-linux/</tt> in the example above).
+
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-3.1.zip|Full Maude 3.1]] and save it into the Core Maude directory.
  
 
== Maude manual and primer ==
 
== Maude manual and primer ==
  
The Maude manual (in PDF format) and the examples in the manual are available [[Maude 2.6 Manual and Examples|here]].  
+
The manual for Maude 3.1 is available in [[Media:Maude-3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude31-manual-html/maude-manual.html HTML].
 +
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.1-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 3.0 to 3.1 ==
  
== Change list from Maude 2.5 to 2.6 ==
+
* Support for unification modulo associativity-identity,
 +
* Support for the generation of irredundant unifiers,
 +
* Support for the filtering of variant unifiers using variant subsumption,
 +
* Support for the generation of variant matchers,
 +
* An implementation of Unix processes as Maude external objects,
 +
* Several improvements in the presentation of results,
 +
* Several improvements in the handling of control-c,
 +
* Some bugs fixed, and
 +
* Some improvements in syntax error detection and recovering.
  
A list of the [[List of the changes from 2.5 to 2.6|changes]] from 2.5 to 2.6 is available.
+
<small>(If you use [http://www.xemacs.org/ XEmacs], then you might find the [[Media:Maude-mode.tar.gz|Maude mode]] for XEmacs
 +
written by [http://www.iam.unibe.ch/~kai/ Kai Br&uuml;nnler] or
 +
the [[Media:Maude-mode2.el.zip|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 [https://github.com/ssaavedra/maude-mode maude-mode] written by Santiago Saavedra. Please see the README for details.
 +
If you are interested in the Eclipse development environment, please, take a look at the [http://moment.dsic.upv.es/ MOMENT] project web site.)
 +
There are also language packages for Atom and other editors.</small>

Latest revision as of 14:25, 12 March 2021

Maude 3.1 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.1

Maude 3.1 comes with the SMT solver Yices2. Click on the appropriate link below to download the collection of binaries, or click the source link to download and compile the sources yourself. If you wish to compile Maude with CVC4, please, read the instructions in the compressed file with the sources.

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

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

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

Full Maude 3.1

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

Maude manual and primer

The manual for Maude 3.1 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 3.0 to 3.1

  • Support for unification modulo associativity-identity,
  • Support for the generation of irredundant unifiers,
  • Support for the filtering of variant unifiers using variant subsumption,
  • Support for the generation of variant matchers,
  • An implementation of Unix processes as Maude external objects,
  • Several improvements in the presentation of results,
  • Several improvements in the handling of control-c,
  • 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. 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.) There are also language packages for Atom and other editors.