Changes in Core Maude:

• Optimizations
• Metalevel caching is more sophisticated.
• Bug fixes
• A bug which caused problems with comments at the end of reduce commands.

  red start . *** start thing running

• A bug that cause segmentation faults with certain bad meta-modules.
• A problem with the A/AC/AU/ACU matching algorithms that could cause them to consume exponential space (rather than merely exponential time) on hard examples.
• A serious bug that cause incorrect matches for nonlinear AC/ACU patterns (bug existed from 1.0 onwards).
• Auto line wrapping is less buggy though still not perfect.
• Abort from debugger no longer spews garbage on the screen when backing out of nested conditional equations.
• Union sorts are converted to an appropriate normal sort if a suitable one exists rather than the error sort when moving sorts up to the metalevel.
• A bug which caused a segmentation fault if the first op declaration in a module was bad:

  op (rl_=>_.) Bool Bool -> Bool .

• Various structures were accidentally passed by value rather than by reference wasting a small amount of memory.
• All detected memory leaks fixed.
• Object level bubbles now work and will be imported correctly though their use is not recommended.
• Much bullet proofing; no more "FATAL ERROR"s, identities more rigorously checked, specials slightly less fragile (but this is still the best way to generate an "Maude internal error").
• Imports where there was an attribute clash for an operator could cause and internal error. This is now handled by marking the importing module as bad and not allowing further use of it.
• Results printed in graph mode (set print graph on .) could corrupt memory.
• Segmentation fault bug in matching for patterns that could collapse at top due to idem.
• Segmentation fault bug in matching with operators that had either a complex identity or an identity together with idem.
• New features
• The single biggest change in 1.0.5 is that the module system has been completely rewritten in order to support lazy flattening and lazy reparsing.

  lazy flattening: when you enter a heavily structured maude program, the signatures are flattened eagerly as usual but the eqs/rls/mbs are only flattened in the current module when a rewriting command is entered. This saves a lot of memory and speeds up module entry, but: (a) certain errors in eqs/rls/mbs aren't caught until the flattening takes place. (b) there is a short pause before the first execution of a rewriting command in a module takes place, while flattening is done. (c) the order of eqs and rls occuring in different modules has changed. A modules own eqs and rls are now before rather than after imported eqs and rls. Of course you should not be relying on this!

  lazy reparsing: when module with the same name as an existing module is entered, it replaces the old module, an all modules that depended on the old module are marked as outdated, and will be reparsed if an attempt is made to use them. The old modules memory is freed up.

• Memoization added; give memo attribute to an operator declaration to use it for equational rewrites with that operator on top. Memoization tables can be cleared explicitly by the command:

  do clear memo .

  Automatic clearing before each top level rewriting command can be turned on and off with:

  set clear memo on .

  set clear memo off .

• Advisories can be turned off and on:

  set show advise off .

  set show advise on .

• You can exclude rewrites in given module from a trace. This is used in FullMaude to exclude FullMaude's own rewrites:

  trace exclude FULL-MAUDE .

  You can re-enable such rewrites with:

  trace include FULL-MAUDE .

• Segmentation faults and bus errors are now trapped and are reported as "internal errors". If you actually see a segmentation fault now it is actually a stack overflow - usually caused by infinite recursion or very deep terms.
• It is now possible to see the number of rewrites and timing for loop module execution:

  set show loop stats on .

  set show loop timing on .

  set show loop stats off .

  set show loop timing off .

• Rules may have variables in condition that don't occur in lhs; such rules can only be used via meta-apply.
• MAUDE_LIB environment variable added: When looking for "prelude.maude", any directories specified in MAUDE_LIB are searched before that containing the executable. When looking for a file, the current directory is checked, followed by those specified in MAUDE_LIB. E.g. setenv MAUDE_LIB ~/MaudeLib:/usr/lib/MaudeLib:~/CurrentProject
• Automatic file extensions: if a file named foo is not found in a given directory, and foo does not have an extension ending in .maude or .obj then foo.maude, foo.fm, and foo.obj are tried before moving to the next directory.
• load command; works just like "in" but prints fewer messages (usually none):

  load full-maude

  Also files specified on the command line are now loaded in this "quiet" mode.
• When loop mode breaks, Maude tries to reinitialize things with the last entered loop command.
• match/xmatch now print timing information.
• It is possible to hide the arguments of one or more operators when printing results by:

  set print conceal on .

  Operators foo bar and baz are chosen for this treatment by:

  print conceal foo bar baz .

  Operators foo and baz are returned to normal by:

  print reveal foo baz .

  This result printing mode can be switch off by:

  set print conceal off .

• Miscellaneous changes
• Linux version is now statically linked to avoid libc version incompatibilities.
• Compaq Alpha/OSF platform supported.
• MachineInts are now 64-bit regardless of architecture.
• q is now a synonym for quit (OBJ3 backward compatibility).
• Debugging code ifdef'd out for smaller binaries.
• New (2.95.1) gcc used. This produces much better code on some platforms and slightly worse code on others.
• Warnings/Advisories now have a standard style.
• It is now an error to declare prec or gather for an operator which does not have mixfix syntax.
• Timing on Linux should be slightly more accurate; times no longer always end in "9" although -ve times are still possible.

Changes in Full Maude:

• Thanks to the new module system available in the new Maude 1.0.5, it is no longer necessary to flatten the Full Maude specification. This makes much simpler understanding and modifying it, and of course there is no extra amount of work for releasing new versions, which is great. Thanks, Steven. The amount of memory required by the structured version is slightly bigger than the required with the flattened one, but I believe it's a reasonable price (~12 vs. ~20).
• Attributes memo and ctor are handled. Full Maude doesn't do anything with them, just passes them to Core Maude. ctor can be used in those examples in which it is necessary to distinguish the constructors. For example, the test sets example in the tutorial uses it.
• Bugs fixed:
• bug in the handling of parameterized sorts in subsort relations;
• functional theories are now printed correctly;
• multiple message declarations in the same line are now allowed;
• there was a bug in the transformation of object-oriented modules to system modules (thanks, Peter);
• bug in the handling of modules importing the module META-LEVEL instantiated by some module fixed.
• The syntax for the rew commands when a number of rewrites is given has been changed in order to avoid ambiguities. Thus,

  rew`[_`]., rewrite`[_`]., rew-in`[_`]., rewrite-in`[_`].

  have been replaced, respectively, by

  rew-`[_`]., rewrite-`[_`]., rew-in-`[_`]., rewrite-in-`[_`].

• Some minor changes have also been done to get messages closer to what Maude produces (e.g.,

  errorSort -> Error, Result -> result,

  etc.).
• The following commands have been included at the end of the full-maude.maude file:

  loop init . *** so you don't have to start starting Full Maude

  trace exclude FULL-MAUDE . *** so you see just what you want to see in the trace

  set show loop stats on . *** so you see number of rewrites

  set show loop timing on . *** ... and times

• A banner is printed when Full Maude start ups, that is, every time the loop init is entered. Since Maude 1.0.5 tries to reinitialize the loop when it breaks, Full Maude is now a bit more robust. Not much more. I've noticed that it recovers correctly when FULL-MAUDE is the module by default, but if one enters a module not enclosed in parentheses then it complains. Make sense, in that case one has to select FULL-MAUDE.
• Some error handling has been added, for example, now it checks that the attributes used in objects are ok. It recovers from some error terms and error modules in more cases.
• Deprecated synonyms obj (fmod), endo and jbo (endfm), and cq (ceq) are now handled.