Difference between revisions of "Maude download and installation"

From The Maude System
Jump to: navigation, search
(Created the download page)
 
(Fix in PDF link, Linux distributions)
 
(53 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.4 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].
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 the Maude binaries, 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
+
The Linux64 and macOS versions of Maude 3.4 are available at [https://github.com/SRI-CSL/Maude/releases/tag/Maude3.4 its GitHub site].
written by [http://www.iam.unibe.ch/~kai/ Kai Br&uuml;nnler] or
+
Its sources are available from the same place. You can find instructions together with the sources. Some Linux distributions also offer Maude in their official repositories ([https://packages.debian.org/stable/maude Debian], [https://packages.ubuntu.com/maude Ubuntu], [https://archlinux.org/packages/extra/x86_64/maude/ ArchLinux], etc.), although their packages might not be up to date.
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 ==
+
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
Click on the appropriate link below to download the collection of binaries, or click the source link to download and compile the sources yourself.
+
   linear.maude
 
+
* [[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.)
+
* [[Compiling Maude from source|Sources]]
+
 
+
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|arm64]
 
   metaInterpreter.maude
 
   metaInterpreter.maude
  linear.maude
 
 
   model-checker.maude
 
   model-checker.maude
  maude.linux
 
 
   prelude.maude
 
   prelude.maude
 +
  process.maude
 +
  smt.maude
 +
  socket.maude
 
   term-order.maude
 
   term-order.maude
   maude.linux64
+
   time.maude
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>.
+
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt>, <tt>maude.arm64</tt> or <tt>maude.darwin64</tt>.
  
== Full Maude 2.6 ==
+
== Maude manual and primer ==
  
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).
+
The manual for Maude 3.4 is available in [[Media:Maude34manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML].
 +
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.4-manual-book-examples.zip|here]].
  
== Maude manual and primer ==
+
== Main changes from Maude 3.3.1 to Maude 3.4 ==
 +
 
 +
* Pseudo-random number generator objects
 +
* Initial equality operator
 +
* Meta-print to string operator and message pair
 +
* LaTeX support
 +
* =># search type
 +
* Various optimizations
 +
* Many bug fixes
 +
 
 +
== Main changes from Maude 3.3 to 3.3.1 ==
 +
 
 +
* Some overparsing has been added to provide more informative hints on user input.
 +
* Some bugs fixed.
 +
 
 +
== Main changes from Maude 3.2.2 to 3.3 ==
 +
 
 +
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories.
 +
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended.
 +
* Modules can now be imported in a new generated-by mode.
 +
* Some new commands and flags have been added.
 +
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. 
 +
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site].
 +
* Some over parsing has been added to better recover and to provide more informative hints on user input.
 +
* Some bugs fixed.
 +
 
 +
== Main changes from Maude 3.2 to 3.2.2 ==
 +
 
 +
* Improvement on the vu-narrow command
  
The Maude manual (in PDF format) and the examples in the manual are available [[Maude 2.6 Manual and Examples|here]].  
+
== Main changes from Maude 3.1 to 3.2 ==
  
The primer for Maude 2.0.1 (but mostly applicable for later versions too) is available [[Maude 2 Primer and Examples|here]].
+
* Support for filtered variant unification in vu-narrow command,
 +
* Several improvements in unification modulo several axioms,
 +
* Several improvements of the external Maude I/O objects,
 +
* A command flag for the depth of searching for A/AU unifiers, and
 +
* Some bugs fixed.
  
== Change list from Maude 2.5 to 2.6 ==
+
== Change list from Maude 3.0 to 3.1 ==
  
A list of the [[List of the changes from 2.5 to 2.6|changes]] from 2.5 to 2.6 is available.
+
* 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.

Latest revision as of 20:20, 21 March 2024

Maude 3.4 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found here.

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 the Maude binaries, and documentation and examples.

The Linux64 and macOS versions of Maude 3.4 are available at its GitHub site. Its sources are available from the same place. You can find instructions together with the sources. Some Linux distributions also offer Maude in their official repositories (Debian, Ubuntu, ArchLinux, etc.), although their packages might not be up to date.

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|arm64]
  metaInterpreter.maude
  model-checker.maude
  prelude.maude
  process.maude
  smt.maude
  socket.maude
  term-order.maude
  time.maude

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

Maude manual and primer

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

Main changes from Maude 3.3.1 to Maude 3.4

  • Pseudo-random number generator objects
  • Initial equality operator
  • Meta-print to string operator and message pair
  • LaTeX support
  • =># search type
  • Various optimizations
  • Many bug fixes

Main changes from Maude 3.3 to 3.3.1

  • Some overparsing has been added to provide more informative hints on user input.
  • Some bugs fixed.

Main changes from Maude 3.2.2 to 3.3

  • Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories.
  • The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended.
  • Modules can now be imported in a new generated-by mode.
  • Some new commands and flags have been added.
  • Constants can be declared as parameters in theories, and be parameterized in parameterized modules.
  • Full Maude is no longer distributed as part of Maude. It is still available from the Full Maude's github site.
  • Some over parsing has been added to better recover and to provide more informative hints on user input.
  • Some bugs fixed.

Main changes from Maude 3.2 to 3.2.2

  • Improvement on the vu-narrow command

Main changes from Maude 3.1 to 3.2

  • Support for filtered variant unification in vu-narrow command,
  • Several improvements in unification modulo several axioms,
  • Several improvements of the external Maude I/O objects,
  • A command flag for the depth of searching for A/AU unifiers, and
  • Some bugs fixed.

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.