Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha76/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha76/

My Maude alpha release site now requires authentication:

User Name: maudeabuser
Password: bughunter

The linux version is statically linked, while the solaris version
only depends are standard solaris dynamic libraries - you should not
have to install any shared objects to run these versions.

This and future alpha releases include the source tree
(alpha76.src.tar.gz). This is done for several reasons:

(1)	To allow static binaries while preserving your right to link
	against newer versions of GNU LGPL'd libraries it uses.

(2)	My hard drive died during the level 0 backup while I was at
	WRLA 2002 and this has left me paranoid about having the only
	Maude source tree on my local disk.

(3)	To allow white box testing.

(4)	Several people have expressed an interest in porting it to
	their favorite platform - although this may be premature as
	the source tree is rather messy and I'm planning a big
	reorganization before the end of the year.

Note that the source code is not yet under the GNU GPL, and like the
binaries should not be redistributed. Currently it only compiles with
g++ 2.95.3. I will be moving it to a newer C++ compiler/stdc++ library
in the near future. Other requirements are recent versions of bison
and flex and the following 3rd party libraries:

Doug Lea's malloc (ftp://g.oswego.edu/pub/misc/malloc.c)
BuDDy (http://www.itu.dk/research/buddy/)
Tecla (http://www.astro.caltech.edu/~mcs/tecla/)
GNU GMP (http://www.swox.com/gmp/)

I have mirrored them in:

http://www.csl.sri.com/~eker/Maude/Lib/Src


Bug fixes:
(1)	We used to allow iter operators with more or less than one
	argument which could provoke internal errors:

	fmod SUCC-BUG is
	  sort Foo .
	  op crash : -> Foo [iter] .
	endfm

(2)	The following example used to take O(n^3) time to abort due to
	a cascade of eager big num computations that are redone and
	thrown away during the stack unwinding (n = # of stack
	frames).

	fmod FACT is pr NAT .
	  op _! : Nat -> NzNat .
	vars N M : Nat .
	  eq 0 ! = s 0 .
	  eq (s N) ! = s N * N ! .
	endfm

	red 10000 ! .
	^C
	abort .

	The bug is now partly fixed by an extra test for abort in
	ACU_NumberOpSymbol; however the cascade of AC normalization is
	still O(n^2) (but far less noticable). A better ACU
	representation will eventually get this down to O(n log n)
	which will be unnoticable to the interactive user.

(3)	The performance bug noted in the Alpha71a release notes wrt
	associativity checking for kinds with many user sorts (Dilia's
	example) is mostly resolved by replacing the O(n^3) algorithm
	with a O(k.n^2) algorithm where k is the width of the sort
	diagram generated for the associative operator. k is bounded
	by the number of user sorts, n, and when n is large, k is
	typically much smaller.

(4)	We now check that terms kinds agree in eq/ceq/rl/crl
	meta-statements and =/:=/=> meta-condition fragments and
	metaMatch/metaXmatch/metaSearch descent functions.
	We also that term and sort kinds agree in mb/cmb
	meta-statements and : meta-condition fragments. The first of
	this large family of related bugs was reported by Peter.

(5)	The check for collapsing to a larger or incomparable sort via
	idempotence was the wrong way around.

(6)	Some missing operator sort declarations added to the prelude.

Other changes:
(1) Command line editing is supported using Tecla. There are a large
number of commands and options - see

http://www.astro.caltech.edu/~mcs/tecla/

for details. Basics: left/right arrow keys to move within line,
up/down arrow keys for history and tab for file name completion.
Also you get a continuation prompt rather than a blank line when Maude
is expecting more input.

(2) The line wrapper now notices changes in the terminal width
(courtesy of Tecla).

(3) The line wrapper uses a new algorithm that avoids inserting a
newline when the next token (say a Nat or a String) is so long that
it will hardwrap anyhow.

(4) You can now use \ <newline> in String constants (just like in
C++):

red in STRING :
"'The time has come,' the Walrus said, \
'To talk of many things: \
Of shoes and ships and sealing wax, \
Of cabbages and kings; \
Of why the sea is boiling hot, \
And whether pigs have wings.'" .

(5) The frozen attribute takes a list of numbers to freeze individual
arguments; e.g.:

  op i : Foo Foo Foo -> Foo [frozen (1 3)] .

Frozen on it's own freezes all arguments as before. The metalevel now
only supports the list of numbers version:

  op frozen : NatList -> Attr [ctor] .

though there is a nasty but temporary hack to allow the current
version of Full Maude to run. This change necessitated replacing the
frewrite algorithm - this is a good place to look for bugs.

(6) There is a new attribute owise (or otherwise) that is only
permitted for equations. An owise equation will only be applied
at a redex if no regular equations apply at that redex.
This feature should be used with care as it can make your
specifications harder to analyze. In some ways it a bit like cut in
Prolog or goto in C++. The reflection is
  op owise : -> Attr [ctor] .

(7) The remaining ANSI escape sequences are now available in the
format attribute as follows:

p      black (for pitch black... b is already used.)
w      white
P      Background black
R      Background red
G      Background green
Y      Background yellow
B      Background blue
M      Background magenta
C      Background cyan
W      Background white
?      Dim
f      Blink (for flash... b is already used.)
x      Reverse video
h      Hidden

I've included a modified version of interfere.maude from the WRLA 2002
demo to show what tricks are possible.

(8) Warnings and advisories now have a more standardized form. Quoting
of user identifiers used be very inconsistent, as well as confusing
since ' and " can legally appear in identifiers. Instead color is
used:

Warning: red
Advisory: green
User identifiers: magenta

However quoting of whole statments on lines of their own are not
colored.

(9) Compilation of operator declarations is now done lazily just as
compilation of eqs/rls/mbs has been done for some time. This now means
that some warnings and advisories will only show up when you actually
do a reduction in a module. The benefit is a saving of cpu cycles and
memory for loading large programs (such as Full Maude) where execution
occurs in the last module.

(10) There are a slew of under-the-hood changes such as an
optimization in the main AC/ACU matcher, a new memory allocation
mechanism for dag nodes and linking against newer 3rd party libraries.
Hopefully these shouldn't have introduced any new bugs...

Steven