Alfa

History of Changes

• Changes made in 1996
• Changes made in 1997
• Changes made in 1998
• Changes made in 1999

Changes in 2000-2004

000116

• Experimental: Aarne Ranta's Grammatical Framework has been plugged in, allowing you view and, to a limited extent, edit English and Swedish translations of definitions and expressions. New commands that appear in the menu include GF: Show in English, GF: Change English translation of ..., GF: Give in English, and analogously for Swedish.

000326

• Added the option Auto Abstract to the Options menu. Initial setting can be changed with the -autoabstract flag.
• Added the option Only refinements from context to the Options menu. Initial setting can be changed with the -onlyrefine flag.

000826

• Experimental: Added the command Print To File... to the File menu. It saves text much as Save, but it uses plugin supplied print functions when selected in the View menu and locally in declarations and expressions. The intended usage is to save natural language text produced with the GF plugin.
• The GF plugin is still in a rather experimental state, but it now supports French in addition to Swedish and English. There is also work in progress on generating LaTeX code.

000914

• Added Fraction to the layout options available in the Layout Editor...
• Made various small updates to the user's guide and related documents on the web.

000929

• Added Proof style rule to the layout options available in the Layout Editor. This allows you to produce proofs that looks nice in natural deduction style at the same time as you can influence how natural language text is generating by using different proof rule functions.
• The menu command Print To File... now generates LaTeX output. The LaTeX result looks nice, but easily becomes too wide to fit on the page...
• The suggested filename for LaTex output is now the name of the file to being edited with .tex added as a suffix.
• The new command line option -print causes Alfa to print files in batch mode. As an example, the command line

  alfa nat.alfa bool.alfa -print

  will produce the files nat.alfa.tex and bool.alfa.tex.

001022

• Added the command . Projections... to the menu window. It creates a submenu with projections from variables that could be used to fill in the current meta variable. Caveats to be fixed:
  • An empty submenu might be shown if no projections are possible.
  • The menu window doesn't automatically return to the main menu after a failed attempt to make a projection, but you can use any action that normally changes the menu, e.g., moving the cursor, to get the main menu back.

001029

• A web page on the recently added support for Printing Alfa documents was created.

001102

• The web page on Printing Alfa documents was improved and moved.
• Constructor names are now printed in boldface.
• A bug caused by packages occurring in the Projections menu was fixed.

001118

• Experimental: added a command Wrap to simplify bottom-up construction of expressions.
• The arguments in open expressions/declarations can now be selected and deleted. (Expect to add more commands to manipulate them later.) Note that selecting the name and the whole argument is not the same.

001128

• Changed how variable names are printed, to make them look nicer and to avoid problems with accented characters.
• Updated the web page on Printing Alfa documents with information on how comments are printed, and what LaTeX macros that can be used to influence how things printed.

001204

• Changed how definitions, packages in particular, are printed, to make them more likely to fit on the page. (Before, complete defintions were printed in LaTeX's math mode, now they are printed in paragraph mode, allowing line breaks and page breaks to be inserted.). This makes them look less similar to what you see on the screen, however.

010216

• Bug fix: the command to insert a new postulate was not added to the menu.
• Added feature: lambda bound variables can be renamed. (If you select a lambda bound variable, you actually select a typing, where the type is hidden, if brief notation is turned on.)
• Infix operators applied to too many arguments are still shown as infix applications, unless hiding is turned off. E.g., the term o A B C f g x, where o has 3 hidden arguments, is displayed as (f o g) x rather than o f g x, when hiding is on, and o A B C f g x, rather than (A o B) C f g x, when hiding is turned off.

010221

• Added a horizontal scroll bar to the menu window. (Suggested by Jan Smith)

010311

• The proof style Top-Down Proof Tree has been improved and, after being "work in progress" for a long while, now seems to to be a useful alternative to Natural Deduction style proofs, which can easily become rather wide. An example is shown in the natural deduction tutorial.

010319

• Improved the way assumptions (i.e., lambda abstractions) are displayed in proofs. Instead of lambdas, they are now shown with their names and types in square brackets.

010322

• Fixed a bug introduced on 010319 that could cause Alfa to crash with "No match in _needParen".

010415

• Instead of always jumping to the next meta variables after an editing operation, the cursor now only jumps if was on a meta variable before the editing operation.
• Added Auto Goto Next Goal to the Options menu, which allow you to completely turn off cursor jumping after editing operations. The initial setting can be changed with the -autonextgoal flag.

010418

• Improved LaTeX printing: added conversion of most characters in the symbol font (e.g. greek letters) to the appropriate LaTeX commands. Also fixed a bug in the printing of data definitions.

010503

• Added a flag -uglymembershipsymbol to make Alfa use ::, instead of the usual set membership symbol, in type signatures.
• Created a version of Alfa with preliminary support for inductive families, using Makoto's version of Agda. For the time being, it is separate from the ordinary version of Alfa, and is started with the command ialfa and it is available only on dogbert (our main development machine).

010515

• Just a small change: When brief notation is off, Alfa now chooses between horizontal and vertical layout when displaying (dependent) function types and lambda abstractions.

010530

• Bug fix: Alfa failed to avoid importing the same file twice, if it was imported via several paths, some of which contained ../../.

010531

• Instead of always appearing with a light, constructors are now filtered and marked or like other entries in the menu. This will probably not make any difference most of the time, except for constructors in inductive families (in ialfa).

010603

• For improved color usage consistency, parentheses, brackets and braces are now displayed in the keyword/delimiter color. (See command line options.)
• The line width used for drawing large brackets etc is now adjusted according to the font size.
• Removed parentheses around some mixfix operator applications that don't need them.
• Updated the section about layout options in the user's guide.
• Fixed a font size bug: font sizes were internally numbered 0-6, but externally 1-7. They are now numbered 1-7 everywhere, and the default size is 4 instead of 3.

010614

• Add support for associative operators. For example, if + is declared associative, both (a+b)+c and a+(b+c) will be displayed as a+b+c.

010615

• Experimental feature: when specifying mixfix operators, you can now use digits in addition to _ to specify not only where to put an argument, but also which argument to put there. For example, if _ then _ else _ is equivalent to if 1 then 2 else 3, and with today's feature, you could also use 2 if 1, 3 otherwise as an alternative view of the same operator.

010616

• Support for properties (abstract/private etc) and type signatures in open arguments. Note: the Agda type checker is likely to fail when adding a type signature...
• Postfix operator now have a precedence setting, like infix/distfix/mixfix operators (but no associativity).

010618

• Support for the new mixfix functionality (from 010615) and the new way of displaying assumptions in proofs (from 010319) in the LaTeX printer.
• More consistent terminology for commands that add and remove type annotations in expressions.

010625

• Small updates of the user's guide.

020725

• Alfa now uses IAgda (with support for idata) by default.

020801

• Alfa distributions now contain Michael Hedberg's New library. (Documentation is under preparation.)

021120

• Alfa now saves all View menu options except the Font Size. (Before, only the Argument Hiding option was saved.)

030407

• Added the flag -termcounter to change Agda's termination counter (the built-in default value is 1000.)
• The Compute command now appears in the menu with a red light , instead of being absent from the menu, if computation fails. By selecting the (red) Compute command, you can get the error message containing the reason why the computation failed (problably that the termination counter reached the limit).

041014

• Added the option Simple Refine to the Options menu. Previously, this option could be set only with the command line flag -simplerefine. That flag now sets the default for the menu option.