Maude download and installation

From The Maude System
Revision as of 17:24, 25 September 2024 by Malaga (Talk | contribs)

Jump to: navigation, search

Maude 3.5 runs on many Unix variants, including MacOS and 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 (both darwin64 and ARM boxes) versions of Maude 3.5 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.5 is available in PDF format. The examples in the manual and in the book All About Maude is also available here.

Main changes from Maude 3.4 to Maude 3.5

  • Several changes related to the vu-narrow command:
    • vfold option,
    • path option,
    • a state may now subsume its ancestors,
    • allow term disjunctions at the object level,
    • show most general states command, and
    • show frontier states command
  • Reading from the stdin stream now supports continuation lines
  • Improvement of the initial equality operator
  • Extra built-in operators on characters and strings
  • Various optimizations
  • Many bug fixes

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.