Starting with tag: [TAG 2.0.1 ulfn@cs.chalmers.se**20070706121249] [bumped version to 2.0.2 ulfn@cs.chalmers.se**20070706121351] [made literate agda files work properly ulfn@cs.chalmers.se**20070712123859] [white space ulfn@cs.chalmers.se**20070712123938] [prepared for magic with ulfn@cs.chalmers.se**20070713180158] [magic with ulfn@cs.chalmers.se**20070713201656] [test cases for magic with ulfn@cs.chalmers.se**20070713223321] [bumped version to 2.1.0 ulfn@cs.chalmers.se**20070713223425] [TAG 2.1.0 ulfn@cs.chalmers.se**20070713223506] [bumped version to 2.1.1 ulfn@cs.chalmers.se**20070713223950] [... syntax for non-dependent with ulfn@cs.chalmers.se**20070714195514] [On windows, avoid file io using Data.ByteString.Lazy makoto.takeyama@aist.go.jp**20070715171034] [view from the left type checker ulfn@cs.chalmers.se**20070716150852] [fixed some problems with ... syntax ulfn@cs.chalmers.se**20070725155511] [made termination checker accept things like y :: ys < x :: y :: ys ulfn@cs.chalmers.se**20070726151608] [postpone typechecking of records against meta types ulfn@cs.chalmers.se**20070726195535] [effect example ulfn@cs.chalmers.se**20070726211838] [binary number example ulfn@cs.chalmers.se**20070727133340] [forgot to add boot file ulfn@cs.chalmers.se**20070727133355] [show implicit arguments when generating with function type ulfn@cs.chalmers.se**20070727190819] [minor changes to path example ulfn@cs.chalmers.se**20070727201010] [updated failing test case ulfn@cs.chalmers.se**20070727201022] [some examples ulfn@cs.chalmers.se**20070728113743] [sinatra example ulfn@cs.chalmers.se**20070730114335] [fixed bug with wrong hiding of module params in record field types ulfn@cs.chalmers.se**20070730114349] [Added nubFiles. Nils Anders Danielsson **20070704231746] [Unidentical references to the same file should not trigger an error anymore. Nils Anders Danielsson **20070704232155 + I want this feature since my default search path contains both the current directory and the path to a general library, and the previous behaviour made it awkward to work on the library itself. + The machinery for comparing file names is a bit shaky, but I hope that this will work well in practice. ] [Made the Emacs mode better aligned with Emacs 22. Nils Anders Danielsson **20070809203823 + Without breaking backwards compatibility (for most installations, I hope, etc., etc.). ] [put proofs back into the cwf model example ulfn@cs.chalmers.se**20070810090420] [failing tests message update ulfn@cs.chalmers.se**20070810090501] [fixed constructors in parameterised modules bug ulfn@cs.chalmers.se**20070815125950] [bumped version to 2.1.2 ulfn@cs.chalmers.se**20070816145040] [TAG 2.1.2 ulfn@cs.chalmers.se**20070816145125] [bumped version to 2.1.3 ulfn@cs.chalmers.se**20070816145248] [Added notes from a discussion about how a class system might be defined. Nils Anders Danielsson **20070817165913] [summer school lecture ulfn@cs.chalmers.se**20070818193813] [summer school lecture ulfn@cs.chalmers.se**20070820092217] [tidying up of summer school lecture ulfn@cs.chalmers.se**20070820114806] [summer school lecture changes ulfn@cs.chalmers.se**20070821072811] [alonzo runtime system cabal package ulfn@cs.chalmers.se**20070821072851] [font info in README ulfn@cs.chalmers.se**20070821090328] [added builtin pragmas to RTP.hs ulfn@cs.chalmers.se**20070821094151] [naive boolean solver example ulfn@cs.chalmers.se**20070821110039] [normalisation for simply typed lambda calculus example ulfn@cs.chalmers.se**20070822120221] [size change mehltret@cip.ifi.lmu.de**20070903054120] [moved-isLeft-isRight-to-Utils/Either andreas.abel@ifi.lmu.de**20070903151409] [size-change termination andreas.abel@ifi.lmu.de**20070903151454 The old foetus termination checker has been moved to FoetusTermination.hs. The new checker uses the foetus infrastructure of call graphs, call matrices, and call graph completion and just replaces the termination criterion of foetus (lexicographic termination order exists) by the one of size-change termination (each idempotent call matrix from a function to itself has a decreasing argument). Also call matrices can now be nested: instead of a single entry of type order (<, =, or ?) they can have matrices as entries. These are used when extracting call matrices from a tupled function (e.g., add, ack : Nat * Nat -> Nat) or in cases like f (x :: y :: ys) = f (x :: ys) The resulting call matrix will be x y::ys x = ? ys ? < Some examples now termination check which would have required reformulation otherwise (see examples/Termination/Examples.hs). Subpattern analysis should now be superfluous (at least it has been commented out for now). ] [solutions to summer school exercises ulfn@cs.chalmers.se**20070821105936] [fix-order-multiplication andreas.abel@ifi.lmu.de**20070903161548] [tests-for-strict-positivity andreas.abel@ifi.lmu.de**20070910153510 Extended regression test suite by a few examples of strictly positive and not strictly positive data types. ] [fix to positivity test ulfn@cs.chalmers.se**20070911110015] [failing tests error messages ulfn@cs.chalmers.se**20070911110409] [tait example ulfn@cs.chalmers.se**20070911110427] [LINE pragmas ulfn@cs.chalmers.se**20070917120035] [allow LINE pragma at the beginning of a file ulfn@cs.chalmers.se**20070917143607] [very nested datatype example ulfn@cs.chalmers.se**20070917144113] [nested-data-example andreas.abel@ifi.lmu.de**20070913123615] [simplified Bush test case ulfn@cs.chalmers.se**20070920094438] [start on a very simple library ulfn@cs.chalmers.se**20070920094501] [a simple stack language example ulfn@cs.chalmers.se**20070920094548] [bool and logic in simple-lib ulfn@cs.chalmers.se**20070928112000] [fixed impossible bug for definitions like id id = id ulfn@cs.chalmers.se**20070928124048] [added Windows readme file ulfn@cs.chalmers.se**20070928135609] [cbs example ulfn@cs.chalmers.se**20070929103212] [cbs example: made interpreter sound by construction ulfn@cs.chalmers.se**20070930140944] [changed to ctags ulfn@cs.chalmers.se**20071001161534] [fixed bug with abstract in local defs ulfn@cs.chalmers.se**20071001161551] [minor cosmetics in cbs example ulfn@cs.chalmers.se**20071001161617] [fixed bug with module imports ulfn@cs.chalmers.se**20071002105427] [fixed error message for abstract constructor out of scope ulfn@cs.chalmers.se**20071002115024] [Made note about Unicode fonts for Emacs more precise. Nils Anders Danielsson **20070827094042] [Added note which should ensure that Agda files use UTF-8 encoding. Nils Anders Danielsson **20071004172525 + If the users follow the note... ] [Added annotation-preserve-mod-p-and-undo. Nils Anders Danielsson **20071004184256] [Highlighting is now rear-sticky. Nils Anders Danielsson **20071004203445 + So, for instance, if you append text to a comment (by writing one character at a time, not by copying), the new text will be highlighted using the comment face. ] [Made it possible to use a dedicated font for Agda buffers. Nils Anders Danielsson **20071004210654 + The default settings should now provide a font with many Unicode symbols, provided that the font that I have in mind is installed on the system, and the X Window System is used. ] [Included the agda2 customisation group in the languages group. Nils Anders Danielsson **20071004210740] [Updated the outdated documentation for font selection. Nils Anders Danielsson **20071005112702] [removed preprocessor stuff from parser ulfn@cs.chalmers.se**20071008135857] [deunicoded cbs example and added path finding program ulfn@cs.chalmers.se**20071009152600] [popup-menu at a goal is shift-mouse-2 makoto.takeyama@aist.go.jp**20071003084001] [unicode_on_windows makoto.takeyama@aist.go.jp**20071010064640] [Stopped using special Agda2 face, the default font is changed instead. Nils Anders Danielsson **20071010145116 + This only applies to the current frame, and the behaviour can be turned off. ] [Fixed typo. Nils Anders Danielsson **20071010145202] [Fixed comment. Nils Anders Danielsson **20071013104604] [Added flag (pragma) for turning off the completeness checker. Nils Anders Danielsson **20071013105744 + This flag is currently unused, since there is no completeness checker yet. ] [Improved the command-line usage information. Nils Anders Danielsson **20071013110135] [Added infrastructure for highlighting incomplete patterns. Nils Anders Danielsson **20071013110947] [Added "show normalised context" functionality to GUI. Nils Anders Danielsson **20071013122730] [Removed incorrect documentation. Nils Anders Danielsson **20071013124906] [Got rid of warning. Nils Anders Danielsson **20071013131154] [Fixed documentation. Nils Anders Danielsson **20071013132500] [Fixed bug caused by read-only text. Nils Anders Danielsson **20071013141628] [Fixed bug: Text properties were not removed properly. Nils Anders Danielsson **20071013142107] [Made some macros more hygienic. Nils Anders Danielsson **20071014100853] [allow newline in pragmas ulfn@cs.chalmers.se**20071016124400] [removed note about windows from README ulfn@cs.chalmers.se**20071016124449 windows users should read README_WINDOWS ] [added more stuff to simple-lib ulfn@cs.chalmers.se**20071016124550] [added missing BUILTIN STRING to alonzo run-time ulfn@cs.chalmers.se**20071016124600] [fixed bug with missing parentheses when refining ulfn@cs.chalmers.se**20071016140100] [The Emacs mode can now control the display of implicit arguments. Nils Anders Danielsson **20071016142403] [fixed silly bug with evaluating primitives ulfn@cs.chalmers.se**20071016145217] [fixed bug when using give on an instantiated meta ulfn@cs.chalmers.se**20071016153336] [changed generated name for non-dependent args to .x (from _) ulfn@cs.chalmers.se**20071016153417] [fixed bug with displaying contexts ulfn@cs.chalmers.se**20071017152745] [fixed bug with let bindings under lambdas ulfn@cs.chalmers.se**20071018131429] [fixed bug with some primitive functions ulfn@cs.chalmers.se**20071018131655] [don't allow positivity checker to see through abstract ulfn@cs.chalmers.se**20071018132133] [added failing test cases for declaration exceptions ulfn@cs.chalmers.se**20071018142650] [disallowed records in mutual blocks ulfn@cs.chalmers.se**20071018142742] [added pretty printing for declaration exceptions ulfn@cs.chalmers.se**20071018142805] [fixed printing of declaration exceptions ulfn@cs.chalmers.se**20071018161859] [report error on non-existing names in fixity declarations ulfn@cs.chalmers.se**20071019114236] [The Emacs mode now respects the optTerminationCheck flag. Nils Anders Danielsson **20071019070918] [Made infoFileName more robust for non-absolute paths. Nils Anders Danielsson **20071019073636] [Added key binding for reloading or clearing syntax highlighting. Nils Anders Danielsson **20071019083107] [Syntax highlighting for Emacs is now generated more often. Nils Anders Danielsson **20071019083823 + It is generated when imported modules are type checked. (And as a consequence imported files are now termination checked. When the Emacs mode is used this information is not visible unless the file in question is inspected, though.) + If the --emacs flag is given the batch interface also generates Emacs highlighting files. ] [Termination problems are now displayed for imported modules (in batch mode). Nils Anders Danielsson **20071019102436 + When term.warn.no is ≥ 1. + And only if the module is actually type checked. ] [Removed the non-existing agda2-submit-bug-report from the Agda2 menu. Nils Anders Danielsson **20071019112131] [implemented check for repeated variables in left hand sides ulfn@cs.chalmers.se**20071022120942] [Made the use of top-level unsafePerformIO a bit more safe. Nils Anders Danielsson **20071019113038] [Fixed typo in comment. Nils Anders Danielsson **20071019140254] [Merged the three IORefs into a single one. Nils Anders Danielsson **20071019160929 + Removed the environment from the state (it was never updated). ] [Made it possible to infer types and normalise things at the top-level. Nils Anders Danielsson **20071019162051 + Without first creating a dummy goal... ] [Changed a bunch of key bindings. Nils Anders Danielsson **20071020150206 + C-c C-g for give is annoying, since C-g is typically used to abort things in Emacs. I changed it to C-c C-h (fill Hole), and moved agda2-highlight-reload-or-clear to C-c C-s. + Some other key bindings clashed with recommendations for how Emacs modes should be written, so I changed them: agda2-show-context -> C-c ; agda2-text-state -> C-c C-x C-t (analogously to C-c C-x C-b) agda2-solveAll -> C-c C-= ] [Decided to change to more consistent key bindings. Nils Anders Danielsson **20071020154405 + These are of course up for discussion. It's a good idea to change them before we get too many users, though. ] [Removed the key binding explanations. Nils Anders Danielsson **20071020155310] [Changed the key binding for give to C-c C-SPC. Nils Anders Danielsson **20071020201018] [fixed bug with metavariables being solved with wrong implicitness ulfn@cs.chalmers.se**20071022125154] [fixed bug where substitution was not applied properly when unifying ulfn@cs.chalmers.se**20071024120514] [fixed bug with unification not postponing constraints ulfn@cs.chalmers.se**20071024141443] [disabled normalisation when looking for display forms ulfn@cs.chalmers.se**20071024145431 when printing non-terminating terms (for instance, in the termination checker) display form lookup might otherwise loop ] [removed a quite possible __IMPOSSIBLE__ ulfn@cs.chalmers.se**20071024150510] [the positivity check can no longer see through abstract ulfn@cs.chalmers.se**20071024153503] [minor bug fixes in examples ulfn@cs.chalmers.se**20071024165626] [throw error when termination checking fails on top-level (batch mode only) ulfn@cs.chalmers.se**20071024165655] [The TAB key (indentation) now works in terminals. Nils Anders Danielsson **20071025104828 + At least in my terminal. ] [Changed the key binding for inferring types to C-c C-d ("deduce"). Nils Anders Danielsson **20071025105215 + C-i means the same as TAB in Emacs (by default, anyway), and this is what was displayed in the menus. ] [Added explanations for the C-c C-e and C-c C-d key bindings. Nils Anders Danielsson **20071025105449] [cbs example: start on proof ulfn@cs.chalmers.se**20071029155713] [added license files ulfn@cs.chalmers.se**20071106131112] [ghc-6.8 compatibility ulfn@cs.chalmers.se**20071106131213] [minor makefile changes ulfn@cs.chalmers.se**20071107105726] [updated cabal file for translator to cabal-1.2 ulfn@cs.chalmers.se**20071108183349] [fixed some test cases ulfn@cs.chalmers.se**20071108183433] [moved to quickcheck 2 and implemented some tests ulfn@cs.chalmers.se**20071108205010] [resolved conflicts ulfn@cs.chalmers.se**20071108233633] [Alonzo - better import handling for open import...public marcin.benke@gmail.com**20071107100302] [The Agda Wiki is now listed as the Agda homepage. Nils Anders Danielsson **20071108163244] [In GHC 6.8.1 a Monoid instance for Maybe is already defined. Nils Anders Danielsson **20071108190016] [The API of Data.Map changed in GHC 6.8.1. Nils Anders Danielsson **20071108190033] [Broke recursive cycle in a different way. Nils Anders Danielsson **20071108192254 + With GHC 6.8.1 and Cabal 1.2 the file Lexer.hs-boot was not found; for some reason GHC did not look for it in src/full, but only in dist/build. + Workaround: Created .hs-boot files for modules which are not generated (unlike Lexer.hs) instead. ] [Tabs embedded in string literals now seem to give rise to lexical errors. Nils Anders Danielsson **20071108192418 + Under GHC 6.8.1. ] [Removed "empty" modules from the export list. Nils Anders Danielsson **20071108192858 + A new GHC warning spotted these. ] [Simplified encoding/decoding and got rid of the append workaround. Nils Anders Danielsson **20071108193624 + Note that this code requires a new version of binary (0.4.1) and perhaps also new versions of GHC (6.8.1) and bytestring (0.9.0.1). + I tested a version of this patch a long time ago, and back then it only lead to small differences in (de)serialisation efficiency. ] [Listed a missing module. Nils Anders Danielsson **20071108195003] [Upgraded the Cabal files to Cabal 1.2 and the new base libraries. Nils Anders Danielsson **20071108195500 + Also made library version ranges more precise. Upgrades where the major component of the version changes are rejected by this configuration. + I used the current versions of various libraries as the minimum acceptable. I think this is fine, since Cabal 1.2 only ships with GHC 6.8.1; it is easier (?) to ask people to upgrade GHC than to ask them to upgrade Cabal. Furthermore the current version of zlib is easier to install on Windows, and the current version of binary is required to avoid a serialisation bug. + I also set explicit version ranges on the tools used (Alex and Happy). These could perhaps be tweaked. ] [Added missing --dont-termination-check pragmas to the test suite. Nils Anders Danielsson **20071108203013] [Made some comments less Unix-specific. Nils Anders Danielsson **20071108203733] [Updated README: New Cabal, new libraries. Nils Anders Danielsson **20071108203807] [Improved a comment. Nils Anders Danielsson **20071108203819] [Merged Ulf's and my changes incorporating support for GHC 6.8.1. Nils Anders Danielsson **20071109142747 + Removed support for older versions of GHC and older libraries. ] [Replaced the license with the one used for the old Agda. Nils Anders Danielsson **20071109151537] [Fixed the build-type field. Nils Anders Danielsson **20071109151603] [Added some copyright holders. Nils Anders Danielsson **20071111190344] [fixed conflicts in cabal file ulfn@cs.chalmers.se**20071112104248] [removed unused module ulfn@cs.chalmers.se**20071112104307] [fixed mistake when resolving conflicts ulfn@cs.chalmers.se**20071112105522] [added instructions for downloading QuickCheck 2 to README ulfn@cs.chalmers.se**20071112110907] [fixed LICENSE file for the agda binary ulfn@cs.chalmers.se**20071112111534] [minor bugs in Monad, Data.Fin and Data.Vec scm@iis.sinica.edu.tw**20071113012506 1. Added spaces around colon in Monad.agda. 2. _\/_ and _\equiv_ both have precedence 20, therefore Agda cannot parse them when they appear together. Explicitly bracketed them in Data.Fin and Data.Vec. ] [changed implicit lambda insertion for holes (issue 24) ulfn@cs.chalmers.se**20071119131018] [added readline library to executable cabal (needed on mac) ulfn@cs.chalmers.se**20071119131053] [added literate test case (currently broken: issue 23) ulfn@cs.chalmers.se**20071119131159] [Fixed bug: readline dependency should not be present under Windows. Nils Anders Danielsson **20071112141839] [Simplified the test for Windows. Nils Anders Danielsson **20071112093803] [Improved the documentation of agda2-ghci-options. Nils Anders Danielsson **20071112133113] [Added tested-with field (tested with GHC 6.8.1). Nils Anders Danielsson **20071112142202] [Merged the two README files, and updated some parts of them. Nils Anders Danielsson **20071112142417] [Fixed simple error in example. Nils Anders Danielsson **20071116143625] [Modified the set of primitive operations. Nils Anders Danielsson **20071116145308 + Added primCharEquality. + Renamed the other equality operations for consistency. + Replaced primCharToInteger and primIntegerToChar to primCharToNat and primNatToChar, respectively. ] [improved makefile to check if reconfigure is needed ulfn@cs.chalmers.se**20071120133152] [fixed bug with literate files (issue 23) ulfn@cs.chalmers.se**20071120133236] [fixed bug in Makefile ulfn@cs.chalmers.se**20071126005009] [dot patterns represented in internal syntax (not used yet) ulfn@cs.chalmers.se**20071126005020] [generate dot patterns in the internal syntax ulfn@cs.chalmers.se**20071126064314] [the termination checker now looks at dot patterns ulfn@cs.chalmers.se**20071126064401] [added test case for dot pattern supported termination ulfn@cs.chalmers.se**20071126064818] [fixed bug with dot patterns having the wrong context ulfn@cs.chalmers.se**20071126073431] [test case for the bug fixed in the previous patch ulfn@cs.chalmers.se**20071126073948] [fixed bug with dot patterns being updated incorrectly ulfn@cs.chalmers.se**20071126083115] [fixed bug with dot patterns not being updated when splitting on literal ulfn@cs.chalmers.se**20071126083252] [disabled termination checker for AIM4/bag (strange bug?) ulfn@cs.chalmers.se**20071126140403] [remember telescope and permutation of clauses ulfn@cs.chalmers.se**20071126140437] [started on Coverage.hs ulfn@cs.chalmers.se**20071126140702] [call coverage checker (which doesn't do anything) ulfn@cs.chalmers.se**20071127000530] [changed the interface of clause splitting ulfn@cs.chalmers.se**20071127001542] [Changed the key binding used for solving constraints (C-c C-! → C-c C-s). Nils Anders Danielsson **20071126113919] [Made it possible to evaluate abstract things in the GUI. Nils Anders Danielsson **20071126114044] [exception monad transformer ulfn@cs.chalmers.se**20071127082732] [changed index unification to return yes/no/maybe ulfn@cs.chalmers.se**20071127082752] [index unification in clause splitting (still unfinished) ulfn@cs.chalmers.se**20071127082822] [clause splitting finished (needs testing) ulfn@cs.chalmers.se**20071128012531] [working coverage checker ulfn@cs.chalmers.se**20071128064224] [remove interface file if it creation fails (to avoid truncated interface files) ulfn@cs.chalmers.se**20071128065350] [look at dontCompletenessCheck flag ulfn@cs.chalmers.se**20071128070304] [fixed bug with splitting on wrong variable in coverage checker ulfn@cs.chalmers.se**20071128073209] [nice error message for incomplete matching ulfn@cs.chalmers.se**20071128080725] [changed syntax for record fields in preparaton for fancy projection modules ulfn@cs.chalmers.se**20071128112225 + Fields are now prefixed by the 'field' keyword. This is a layout keyword so you can say: record A : Set where field a : X b : Y ] [infix declarations allowed in record declarations ulfn@cs.chalmers.se**20071128120441] [test case for infix record fields ulfn@cs.chalmers.se**20071128134019] [changed name of checking disabling flags ulfn@cs.chalmers.se**20071128134034] [fixed bug with constructors of private datatypes being visible ulfn@cs.chalmers.se**20071129001243] [added Makoto's solution to the isabelle parenthesis excercise to the examples ulfn@cs.chalmers.se**20071129002713] [how to avoid naming implicit arguments (ParenTac example) ulfn@cs.chalmers.se**20071129004047] [separate make targets for build and register ulfn@cs.chalmers.se**20071129005735] [preparations module instantiations in let ulfn@cs.chalmers.se**20071130014746] [fixed bug with postponed type checking in non-empty contexts ulfn@cs.chalmers.se**20071130015443] [Fixed bug in termination checker. Nils Anders Danielsson **20071129005911 + Made a better job of replacing instantiated meta-variables with the terms they represent; the termination checker does not handle meta-variables. ] [Updated generation of highlighting information to reflect AST changes. Nils Anders Danielsson **20071129012942] [added --emacs and --vim when doing make test ulfn@cs.chalmers.se**20071130022627] [cleaned up some options ulfn@cs.chalmers.se**20071130022654] [.lagda.(vim|el) are boring ulfn@cs.chalmers.se**20071130030001] [fixed bug with with in where ulfn@cs.chalmers.se**20071130043930] [allow splitting on dot patterns in coverage checker ulfn@cs.chalmers.se**20071130045435] [added sugar for open module _ = ... ulfn@cs.chalmers.se**20071130051700 + open M es + is sugar for + open module _ = M es ] [updates to the TODO file ulfn@cs.chalmers.se**20071130052142] [allow module instantiations in let ulfn@cs.chalmers.se**20071130054837] [bound concrete names now comes with a fixity (always defaultFixity) ulfn@cs.chalmers.se**20071130062613] [fancy record declarations ulfn@cs.chalmers.se**20071130103446 + You can now include arbitrary declarations in records. + Declarations appearing before the last field must be valid + let declarations (simple definitions or module manipulation), + but declarations after the last field can be anything. ] [fixed bug with the new open short hand ulfn@cs.chalmers.se**20071130110530] [fixed another bug with new open short hand ulfn@cs.chalmers.se**20071130141734] [export Doc from TypeChecking.Pretty ulfn@cs.chalmers.se**20071207081947] [fixed bug with record fields of meta type ulfn@cs.chalmers.se**20071207082012] [fixed bug with matching on number literals (issue 26) ulfn@cs.chalmers.se**20071207100255] [enforces builtin bindings to zero, suc, cons, nil, true, and false to be constructors ulfn@cs.chalmers.se**20071207101002] [removed deprecated builtin equality ulfn@cs.chalmers.se**20071207101017] [only look at dot patterns when termination checking if really necessary ulfn@cs.chalmers.se**20071207123004] [profiling files are really boring ulfn@cs.chalmers.se**20071207144202] [fixed bug with module application in let (issue 34) ulfn@cs.chalmers.se**20071207144214] [fixed bug with fixity declarations not being scope checked inside records (issue 35) ulfn@cs.chalmers.se**20071207150033] [fixed issue 17 with incorrect scoping of with clauses ulfn@cs.chalmers.se**20071211104032] [fixed more bugs with module applications in let (issue 34) ulfn@cs.chalmers.se**20071211113922] [implemented a simple tool to generate tag files (hTags) ulfn@cs.chalmers.se**20071211182503] [use hTags to generate tags file for source tree ulfn@cs.chalmers.se**20071211183113] [fixed error message for invalid let declarations (issue 41) ulfn@cs.chalmers.se**20071212000825] [benchmarking ulfn@cs.chalmers.se**20071213120959] [logs from benchmark runs ulfn@cs.chalmers.se**20071219100923] [more benchmark runs ulfn@cs.chalmers.se**20071219102354] [Added the Haskell Communities and Activities Report entry for Dec 2007. Nils Anders Danielsson **20071207113629] [Documented discussion with Ulf about fixity declarations and parsing. Nils Anders Danielsson **20071220190221] [Improved formatting of generated command. Nils Anders Danielsson **20080108191458] [fixed bug with caselessness checker ulfn@cs.chalmers.se**20080116143911] [some error message changes ulfn@cs.chalmers.se**20080116143931] [distinguish between different literals when checking for caselessness ulfn@cs.chalmers.se**20080131074215] [translator update to changes in name representation ulfn@cs.chalmers.se**20080131074258] [Added support for the etags file format. Nils Anders Danielsson **20080209204406] [avoid duplicated names in the context ulfn@cs.chalmers.se**20080219142145] [eta contract terms before magic with abstraction ulfn@cs.chalmers.se**20080220000913] [dtp'08 talk ulfn@cs.chalmers.se**20080220000942] [allow overloaded constructors ulfn@cs.chalmers.se**20080220020505] [dtp'08 implementations (Ulf and Conor) ulfn@cs.chalmers.se**20080222105456] [fixed a bug which caused the type checker to loop ulfn@cs.chalmers.se**20080222161330] [added simple-lib to the test suite and made some changes ulfn@cs.chalmers.se**20080222161350] [prepared for enhanced constraint solving for injective functions ulfn@cs.chalmers.se**20080225172958] [removed unnecessary closure in meta judgments ulfn@cs.chalmers.se**20080225205016] [better regexping on error messages ulfn@cs.chalmers.se**20080225221558] [enhanced constraint solving for injective functions ulfn@cs.chalmers.se**20080225221631] [fixed an unsafe use of injectivity ulfn@cs.chalmers.se**20080226130406] [disable profiling of the executable ulfn@cs.chalmers.se**20080226130522] [fixed a problem with under constrained metas when using injectivity ulfn@cs.chalmers.se**20080226185041] [actually fix the problem with underconstrained metas ulfn@cs.chalmers.se**20080226194921] [postpone checking of constructors against blocked types ulfn@cs.chalmers.se**20080226214808] [fixed a bug with the names of implicit arguments being forgotten ulfn@cs.chalmers.se**20080227082536] [added mparens to Utils.Pretty ulfn@cs.chalmers.se**20080229235041] [Fix bug in font handling. Nils Anders Danielsson **20080229223847 + On window systems other than x and w32 the agda2 fontset was never created, but we still tried to make use of it (unless agda2-change-default-font was nil). + The current code may not work out of the box on all systems. However, the resulting error message should be more enlightening. ] [Fixed possible future bug: Pragmas were applied too late. Nils Anders Danielsson **20080301002754] [more compatible regexp for failing tests ulfn@cs.chalmers.se**20080228105317] [give type error when injective instantiation is impossible ulfn@cs.chalmers.se**20080228105339] [extended pattern match unification to handle datatypes and axioms ulfn@cs.chalmers.se**20080303103905] [minor changes to the simple lib ulfn@cs.chalmers.se**20080303103941] [Add a few required files into the sdist tarball Duncan Coutts **20080304023745 Though it's not obvious what the configure is actually used for. None of the results seem to be used. Perhaps build-type: Simple would be sufficient? Using this patch and the latest development version of Cabal, "cabal sdist" now produces a tarball that can be used sucessfully to build agda. Previously the .hs-boot files were omitted from the tarbal, see: http://hackage.haskell.org/trac/hackage/ticket/67 ] [treat postulates as type constructors when checking injectivity ulfn@cs.chalmers.se**20080304175112] [Added some more primitives to RTP.hs. Wouter Swierstra **20080304194713] [structure sharing (de)serialisation makoto.takeyama@aist.go.jp**20080305125725] [added a benchmark and a couple of runs ulfn@cs.chalmers.se**20080306113611] [The Agda syntax table is now used also in the info buffer. Nils Anders Danielsson **20080307021601 + This ensures that parenthesis highlighting works better in the presence of backslashes (consider \{...}, for instance). ] [fixed issue 49 with named implicits in module telescopes ulfn@cs.chalmers.se**20080311161047] [added error messages for coverage checking errors ulfn@cs.chalmers.se**20080311162952] [fixed issue 52 with missing with-clauses ulfn@cs.chalmers.se**20080313144112] [enforce omitted rhs if there are absurd patterns (issue 51) ulfn@cs.chalmers.se**20080313144845] [fixed a problem with translating reexported constructors in termination checking ulfn@cs.chalmers.se**20080317211840] [fixed a bug in let n-kato@aist.go.jp**20080317020231] [added test case for the let bug ulfn@cs.chalmers.se**20080318105942] [made the user interface aware of postponed typechecking constraints ulfn@cs.chalmers.se**20080319125837] [new pragmas for Alonzo ulfn@cs.chalmers.se**20080319222804 {-# COMPILED_DATA D HsC1 .. HsCn #-} Compile the constructors of the datatype D to the Haskell constructors HsC1 .. HsCn. The Haskell datatype should exist already (this isn't checked). {-# COMPILED f HaskellCode #-} Compile postulate f to the given HaskellCode. No checking. Examples: data Unit : Set where unit : Unit {-# COMPILED_DATA Unit () #-} postulate IO : Set -> Set putStrLn : String -> IO Unit {-# COMPILED putStrLn Prelude.putStrLn #-} ] [don't inline definitions for COMPILED functions ulfn@cs.chalmers.se**20080320094702] [new pragma IMPORT to make Alonzo import Haskell modules ulfn@cs.chalmers.se**20080320102410 {-# IMPORT Control.Concurrent (forkIO) #-} ] [Agda is now tested using GHC 6.8.2. Nils Anders Danielsson **20080319164551] [Switched to the simple build type. Nils Anders Danielsson **20080320153855] [made Alonzo ignore abstract mode ulfn@cs.chalmers.se**20080320203047] [generate the correct file for hierarchical modules when compiling ulfn@cs.chalmers.se**20080320212435] [fixed bug with commas not allowed in pragmas ulfn@cs.chalmers.se**20080320214907] [fixed Alonzo to handle local and hierarchical modules ulfn@cs.chalmers.se**20080320224939] [file IO example using the FFI ulfn@cs.chalmers.se**20080320231117] [fixed semantics of hGetContents in fileIO example ulfn@cs.chalmers.se**20080320232921] [improved interaction between pattern match unification and constraint solving ulfn@cs.chalmers.se**20080331145041] [added a pragma option --no-injectivity-check makoto.takeyama@aist.go.jp**20080401085512] [added MAlonzo compiler (this time with MAlonzo/Primitives.hs) makoto.takeyama@aist.go.jp**20080402000743] [some changes to the simple lib and a division example ulfn@cs.chalmers.se**20080403102454] [fixed bug with --no-positivity being used for disabling the injectivity check ulfn@cs.chalmers.se**20080403161202] [added a benchmark with some categories with families stuff ulfn@cs.chalmers.se**20080407121111] [some prototyping for locally nameless variable representation ulfn@cs.chalmers.se**20080407141946] [fixed a bug which could cause the type checker to loop on postponed type checking problems ulfn@cs.chalmers.se**20080421072626] [Extended the expression grammar to general mixfix operators. Nils Anders Danielsson **20080401233732] [Prototyped an implementation of my suggested handling of precedences. Nils Anders Danielsson **20080401233837 + The code seems to work and is reasonably efficient if parser combinators which do left factorisation on the fly are used. ] [Simplified Parser by using Control.Applicative. Nils Anders Danielsson **20080402004036] [Experimented with some continuation transformers. Nils Anders Danielsson **20080402011047] [Added an elegant but slow parser to the test suite. Nils Anders Danielsson **20080402012837] [Switched from lists to Data.Sequence in AmbExTrie2. Nils Anders Danielsson **20080402014022] [Made the grammar a bit more complicated. Nils Anders Danielsson **20080402015707 + This made all the parsers slower, but the trie-based ones are still OK. ] [Improved efficiency by using memoisation. Nils Anders Danielsson **20080403191651] [Added some more demanding test cases. Nils Anders Danielsson **20080403191710] [Added some open questions. Nils Anders Danielsson **20080403191825] [added emacs command to show goal and context (C-c C-,) ulfn@cs.chalmers.se**20080429092114] [fixed bug with overloaded constructors where we gave up rather than postpone ulfn@cs.chalmers.se**20080429144047] [fixed some naming problems in the Alonzo rts ulfn@cs.chalmers.se**20080505085324] [messing around with the simple-lib ulfn@cs.chalmers.se**20080505085436] [Added the May 2008 HCAR contribution. Nils Anders Danielsson **20080504190441] [Added --no-universe-check. Nils Anders Danielsson **20080502141529] [Fixed bug, thus improving performance. Nils Anders Danielsson **20080409001230 + Apparently FGL implements /multi/-graphs. ] [Added the standard backtracking parser. Nils Anders Danielsson **20080410171836] [Added a memoised variant of the standard backtracking parser. Nils Anders Danielsson **20080410210132 + This is currently the fastest parser. ] [Added implementation note. Nils Anders Danielsson **20080410211437] [Added more test cases. Nils Anders Danielsson **20080411003714 + These confirm that the memoising parser is the fastest one. ] [Removed some speculative comments. Nils Anders Danielsson **20080411021518] [Added discussion about ambiguity. Nils Anders Danielsson **20080411021654] [Removed parse from the parser interface. Nils Anders Danielsson **20080417184638] [Changed the syntax table: Now almost all characters are word constituents. Nils Anders Danielsson **20080430153549 + This matches the Agda lexical syntax better. + Unfortunately some functions, for instance forward-word (M-f), do not seem to respect the syntax table for multi-byte characters. I think this is a bug in Emacs. ] [Simplified code (removed unused argument). Nils Anders Danielsson **20080430153737] [Fixed typo in error message ulfn@cs.chalmers.se**20080505085939] [more naming issues in alonzo rts ulfn@cs.chalmers.se**20080505100840] [Made some interfaces more precise by switching from lists to sets. Nils Anders Danielsson **20080507121017 + This makes the memoised parser run maybe 10% slower (on my test cases), but the trie parsers run a bit faster. ] [Replaced quadratic subcomputation with an O(n log n) one. Nils Anders Danielsson **20080507124701 + Note that for my tests this does not make much of a difference, performance-wise, due to the short inputs involved. ] [Simplified the code by switching to an explicit grammar. Nils Anders Danielsson **20080507210733 + The interface is nicer now: no unique keys are necessary. Parser backends instead have the opportunity to memoise all non-terminals. This is done by the memoised backtracking parser (in Memoised). + I could remove all memoisation from PrecedenceGraph, but this made the trie parsers slow. Since Memoised seems to be the best parser anyway I moved the previous setup to a separate directory ("benchmark"), and kept just Memoised here. + This change does not affect performance much (for Memoised). ] [Moved efficientNub to a separate file. Nils Anders Danielsson **20080507210909] [Required all parsers to be monadic. Made symbol primitive instead of sym. Nils Anders Danielsson **20080507223255] [Outlined how sections can be supported. Nils Anders Danielsson **20080507223446] [Added support for sections and "closed" mixfix operators. Nils Anders Danielsson **20080507223537] [fixed support for local modules in Alonzo and improved handling of natural numbers ulfn@cs.chalmers.se**20080508074215] [show unsolved metas in normalised form in the emacs mode ulfn@cs.chalmers.se**20080508074318] [added some stuff to simple-lib ulfn@cs.chalmers.se**20080508074354] [made the positivity checker look inside defined functions ulfn@cs.chalmers.se**20080511205351] [first approximation of a make-case command (doesn't do 'with') ulfn@cs.chalmers.se**20080513154554] [Remove the emacs22-only ?\s; fix a typo Samuel Bronson **20080507181842] [Make highlighting more dark-background friendly Samuel Bronson **20080505205704] [hiding of implicit arguments and handling absurd patterns in make case ulfn@cs.chalmers.se**20080514082137] [Split out the expression parser from the precedence graph code. Nils Anders Danielsson **20080508173507] [Made a comment more correct. Nils Anders Danielsson **20080512175239] [Fixed some typos. Nils Anders Danielsson **20080513192336] [injectivity check doesn't reduce right hand sides ulfn@cs.chalmers.se**20080514113031] [changed --no-universe-check to --type-in-type (and updated the semantics) ulfn@cs.chalmers.se**20080514113125] [removed the flag to disable injectivity checking ulfn@cs.chalmers.se**20080514141912] [handle 'with' in make case + some fixes ulfn@cs.chalmers.se**20080515091519 case on implicit arguments now works properly case in parameterised modules also works ] [make case only replaces the current line ulfn@cs.chalmers.se**20080515094445] [TAG afp08 ulfn@cs.chalmers.se**20080515115143] [fixed a bug with make case and with ulfn@cs.chalmers.se**20080516143208] [fixed a bug with absurd patterns and make case (issue 73) ulfn@cs.chalmers.se**20080516144457] [Made the Emacs UI display internal errors. Nils Anders Danielsson **20080516151415] [Removed unused macro. Nils Anders Danielsson **20080516151726] [Improved formatting of errors without ranges. Nils Anders Danielsson **20080516161852] [Fixed issue 20 (pragmas are too static in the GUI). Nils Anders Danielsson **20080517081540 + To avoid complicating things too much I decided to reset all options, including whether or not to display implicit arguments, on each reload. ] [Moved the text mode/type checked indication forward in the mode line. Nils Anders Danielsson **20080517083141] [Added more status information to the mode line. Nils Anders Danielsson **20080517091454 + Currently just an indication of whether implicit arguments are displayed. ] [Minor simplification. Nils Anders Danielsson **20080517093748] [Added an option to use Conor McBride's colour scheme. Nils Anders Danielsson **20080517120803 + I may not have gotten all the colours right, though. ] [Added support for more matching parentheses. Nils Anders Danielsson **20080517160238] [Simplified the syntax table code. Nils Anders Danielsson **20080517164024] [Improved documentation. Nils Anders Danielsson **20080517164237] [Fixed bug caused by incompatible settings in .ghci. Nils Anders Danielsson **20080518122945] [All non-ASCII whitespace characters are now treated as whitespace. Nils Anders Danielsson **20080518123927 + Do we also want to treat \f and \v as whitespace? ] [Moved away or fixed many broken example files. Nils Anders Danielsson **20080518144152] [make case now preserves variable names of the original clause ulfn@cs.chalmers.se**20080519085742] [TAG AFP08-2 ulfn@cs.chalmers.se**20080520061847] [fixed some bugs ulfn@cs.chalmers.se**20080520062303] [Added the standard library to the test-suite. Nils Anders Danielsson **20080522125025 + This test case is rather slow, so maybe it should not be activated by default. However, test cases that are not activated by default run the risk of not getting run at all... ] [Fixed bug: agda2-highlight-face-groups could not be permanently customised. Nils Anders Danielsson **20080523150348] [Changed some colours in "Conor's" colour scheme. Nils Anders Danielsson **20080523150409 + Made termination and completeness checking errors be highlighted differently from other errors. ] [Noted that agda2-highlight-incomplete-pattern-face is currently unused. Nils Anders Danielsson **20080523150445 + Since the backend treats incomplete patterns as full errors instead of warnings. ] [Removed possibly incomprehensible remark. Nils Anders Danielsson **20080523150542] [Fixed issue 75 (sometimes hidden arguments cannot be referenced by name). Nils Anders Danielsson **20080523150519] [fixed scoping bug with overloaded constructors (issue 62) ulfn@cs.chalmers.se**20080527110953] [make library-test checks out the standard library to std-lib/ ulfn@cs.chalmers.se**20080527111226 and just does darcs pull if std-lib/ exists ] [fixed bug with overloaded constructors in parameterised modules ulfn@cs.chalmers.se**20080527120457] [fixed printing of impossibles in batch mode ulfn@cs.chalmers.se**20080530073815] [fixed bug with modules in let ulfn@cs.chalmers.se**20080530073854] [Documented and tested some invariants. Nils Anders Danielsson **20080527175348] [Removed an unnecessary precondition. Nils Anders Danielsson **20080527185639] [Noted a problem with the suggested approach to operator precedences. Nils Anders Danielsson **20080528200029] [Made make test recheck everything by default. Nils Anders Danielsson **20080529210203 + Change the setting of AGDA_TEST_FLAGS if you don't like this. ] [Suggested dropping the transitivity emulation. Nils Anders Danielsson **20080529211338] [changed a lot of Ints to Integers ulfn@cs.chalmers.se**20080530124136] [Put all modules under the top-level hierachical name Agda. Nils Anders Danielsson **20080530150335 + This ensures that we do not pollute the Haskell module name space too much. ] [made agda1 to agda2 translator compile ulfn@cs.chalmers.se**20080530151358] [codata and corecursion (only syntax) ulfn@cs.chalmers.se**20080530172437] [fixed silly mistake in lexer ulfn@cs.chalmers.se**20080602073708] [safe unfolding of corecursive functions ulfn@cs.chalmers.se**20080602081755] [made the termination checker ignore coconstructors ulfn@cs.chalmers.se**20080602081857] [some utility functions for mutual blocks ulfn@cs.chalmers.se**20080602124410] [productivity checking for corecursive functions ulfn@cs.chalmers.se**20080602151626] [fixed bug with productivity checker messing up some termination problems ulfn@cs.chalmers.se**20080602161850] [Improved the precedence graph interface. Nils Anders Danielsson **20080531194229 + Precedence graph users no longer need to keep track of the mapping between internal graph nodes and operator names. + Unique names, containing the full module name, are now used. + Also fixed a bug in bindsAs (caught by a test case). ] [Dropped the transitivity emulation. Nils Anders Danielsson **20080531195333] [Added more tests. Rearranged files. Nils Anders Danielsson **20080601202028] [Removed associativity from the fixity type. Nils Anders Danielsson **20080601222949] [Added separate and twoAdjacent. Nils Anders Danielsson **20080602211018] [Added a lexer and support for parsing qualified names. Nils Anders Danielsson **20080602211233 + Including qualified operator applications and sections. ] [Improved a property. Nils Anders Danielsson **20080602213743] [Added an example which does not pass the productivity checker. Nils Anders Danielsson **20080603082115] [fixed bug in with functions where dot patterns were needed to evaluate the types ulfn@cs.chalmers.se**20080603132427] [normalise dot patterns when using them for termination (fixes issue 53) ulfn@cs.chalmers.se**20080603142725] [fixed issue 54 (panic in the coverage checker) ulfn@cs.chalmers.se**20080603144441] [removed support for as-patterns ulfn@cs.chalmers.se**20080604083555] [fixed some problems with make case and dot patterns (issue 73) ulfn@cs.chalmers.se**20080604091843] [require binary-0.4.1 ulfn@cs.chalmers.se**20080604095605] [fixed issue 74 with make case in modules with implicit parameters ulfn@cs.chalmers.se**20080604115141] [clear undo history when loading to fix memory leak (issue 67) ulfn@cs.chalmers.se**20080604123721] [more-termination-examples andreas.abel@ifi.lmu.de**20080604124753] [added-3-termination-examples-to-makefile andreas.abel@ifi.lmu.de**20080604130006] [termination-check-ignore-constructor-names andreas.abel@ifi.lmu.de**20080604130641] [added disclaimer to the interactive mode ulfn@cs.chalmers.se**20080604131348] [termination-check-ignore-constructor-names andreas.abel@ifi.lmu.de*-20080604130641] [removed termination examples with constructor names not mattering ulfn@cs.chalmers.se**20080604150504] [disallow shadowing of module names ulfn@cs.chalmers.se**20080604160433] [MAlonzo FFI support makoto.takeyama@aist.go.jp**20080604155931] [README adapted to the top-level hierachical name Agda andres.sicard@gmail.com**20080604160702] [do eta contraction when termination checking ulfn@cs.chalmers.se**20080604163705] [added the stream eating example ulfn@cs.chalmers.se**20080605104633] [fixed bug with metavariables not being expanded in datatype declarations ulfn@cs.chalmers.se**20080611100554] [Removed the Agda-aware undo feature from the Emacs mode. Nils Anders Danielsson **20080604124142] [Made it possible to use forall-style declarations for (co)data parameters. Nils Anders Danielsson **20080610152516] [Made it possible to use forall-style declarations for module parameters. Nils Anders Danielsson **20080611121448] [added test case for forall-style datatype parameters ulfn@cs.chalmers.se**20080611125612] [always pull patches from standard lib ulfn@cs.chalmers.se**20080611125629] [fixed issue 80 with constructor types not being properly unfolded ulfn@cs.chalmers.se**20080611125653] [fixed issue 63 where the scope checker allowed duplicate constructors ulfn@cs.chalmers.se**20080611130919] [error message comparison in make fail ignores whitespace ulfn@cs.chalmers.se**20080611131946] [fixed issue 76 (missing parenthesis around roundfix operators) ulfn@cs.chalmers.se**20080611133309] [Merged two related test cases. Nils Anders Danielsson **20080611144838] [Made it possible to use forall-style declarations for record parameters. Nils Anders Danielsson **20080612154848] [fixed bug in emptyness checker (issue 81) and improved error message ulfn@cs.chalmers.se**20080616105953] [added test case for issue 81 ulfn@cs.chalmers.se**20080616110202] [MAlonzo now checks that main has type IO a (issue 82) ulfn@cs.chalmers.se**20080616145536] [Removed the primitive IO functions, along with the UNIT builtin. Nils Anders Danielsson **20080616145220 + Use the FFI for IO. + Note that this change may break the old Alonzo. ] [Updated the MAlonzo README in response to a recent patch. Nils Anders Danielsson **20080616150610] [removed unused Serialise.hs ulfn@cs.chalmers.se**20080617103139] [renamed SerialiseShare.hs to Serialise.hs ulfn@cs.chalmers.se**20080617105229] [infrastructure for checking the types of foreign functions ulfn@cs.chalmers.se**20080617111441] [COMPILED_TYPE pragma and translation to Haskell types ulfn@cs.chalmers.se**20080617135508] [changed COMPILED_DATA pragma to include Haskell type name ulfn@cs.chalmers.se**20080617151450] [updated simple-lib to the new COMPILED_DATA pragma ulfn@cs.chalmers.se**20080617151603] [MAlonzo now checks the types of foreign functions and constructors ulfn@cs.chalmers.se**20080617160323] [use -fno-warn-overlapping-patterns when compiling generated Haskell ulfn@cs.chalmers.se**20080617161526] [fixed a bug in Haskell code generation for primitive functions ulfn@cs.chalmers.se**20080617173746] [fixed a bug in MAlonzo with foreign constructors being incorrectly qualified ulfn@cs.chalmers.se**20080617173823] [changed simple-lib to be MAlonzo compatible ulfn@cs.chalmers.se**20080617173933] [made malonzo the default compiler ulfn@cs.chalmers.se**20080617190432] [Fixed comment. Nils Anders Danielsson **20080617143949] [Agda has now been tested with GHC 6.8.3. Nils Anders Danielsson **20080618132825] [Agda now compiles with binary-0.4.2 ulfn@cs.chalmers.se**20080619121032] [patched the Agda1 to Agda2 translator to concrete syntax changes ulfn@cs.chalmers.se**20080619121049] [Removed unnecessary code. Nils Anders Danielsson **20080706101550] [Syntax table change: Made _ and ! punctuation characters. Nils Anders Danielsson **20080706102611] [Defined some Agda-specific abbrevs. Nils Anders Danielsson **20080708125437 + For instance, if you type d C-x ' the text "data : Set where\n" is inserted in the buffer, and point is placed between "data" and ":". + I have not worked hard on these abbrevs. Improvements are welcome. ] [Defined an Agda-specific input method. Nils Anders Danielsson **20080717142016 + The input method is highly customisable. One can easily import bindings from other Quail input methods, change the prefix of the bindings, etc. + By default the input method uses most bindings from the TeX input method, plus a number of mode-specific bindings. + The input method has not been tested much yet, so expect changes in the default bindings. ] [Stopped referring to the batch-mode tool as an "interpreter". Nils Anders Danielsson **20080719110756] [Explained how to rebuild the batch-mode tool when upgrading. Nils Anders Danielsson **20080719110936] [Replaced text about the TeX input method with text about the Agda one. Nils Anders Danielsson **20080719114852] [Made installation of the Emacs mode slightly easier. Nils Anders Danielsson **20080719123400] [fixed documentation for Haddock 0.8 Liyang HU**20080718150153 in preparation for Debian packaging. Haddock and/or ghc -cpp chokes on the following: * Pairs of forward slashes (/) are used to denote emphasis. Single slashes should be escaped with a backslash: \/ * Multi-line string continuations aren't processed properly by -cpp, and this confuses Haddock. Use concat ["first", "second"] (or unlines) instead. * Individual constructor argument types in (non-record) data declarations cannot be annotated. One description per constructor only. ] [Haddock comments cannot be given for instances. Nils Anders Danielsson **20080719200805] [Updated the code for Haddock 2. Nils Anders Danielsson **20080719201430 + Hackage uses Haddock 2. + Note that I had to remove -Werror, since Haddock 2 (which uses the GHC API) for some reason gives the "Unnecessary {-# SOURCE #-} in the import of module ..." warning and I could not find any flag which turns off this warning. ] [Removed duplicate occurrence of ¬. Nils Anders Danielsson **20080721134208] [Reduced the differences between the default bindings under Emacs 22 and 23. Nils Anders Danielsson **20080721155521] [fixed issue 84 (corecursion and absurd clauses) ulfn@cs.chalmers.se**20080725094056] [fixed issue 87 by improving the error message ulfn@cs.chalmers.se**20080725101129] [fixed issue 85 ulfn@cs.chalmers.se**20080725101956] [Module name file name correspondence is now enforce also for the main module ulfn@cs.chalmers.se**20080725110226] [fixed issue 89 with normalisation stopping early for corecursive definitions ulfn@cs.chalmers.se**20080728093430] [extended function inversion to handle nested invertible functions ulfn@cs.chalmers.se**20080728120539 f (g x) = c will now solve for x if f and g are invertible ] [removed unstructured verbosity output ulfn@cs.chalmers.se**20080728141300] [added failing test case for uncurried metavariables ulfn@cs.chalmers.se**20080729092148] [Added the QED symbol (∎). Nils Anders Danielsson **20080725161152] [Noted that a comment seems to be out of date. Nils Anders Danielsson **20080725161307] [Improved some comments. Nils Anders Danielsson **20080728124632] [fixed issue 90 improving Set != Set1 error message ulfn@cs.chalmers.se**20080730082757] [put back -Werror ulfn@cs.chalmers.se**20080730092324 If there's a problem with Haddock, fix Haddock. -Werror is crucial. ] [fixed issue 36 where the same name could be exported twice from a module ulfn@cs.chalmers.se**20080730093432] [fixed some problems in the benchmark suite ulfn@cs.chalmers.se**20080730114419] [fixed a bug when inverting functions with dot patterns ulfn@cs.chalmers.se**20080730114450] [removed __HADDOCK__ ifdefs ulfn@cs.chalmers.se**20080730121228] [Added a newtype for ambiguous QNames in the abstract syntax. Nils Anders Danielsson **20080728152414] [Added allNames. Nils Anders Danielsson **20080728192230] [Made checkModuleName interact better with syntax highlighting. Nils Anders Danielsson **20080729122214] [Simplified the interface to the syntax highlighting code. Nils Anders Danielsson **20080729170232] [Removed some unused and unfinished instances. Nils Anders Danielsson **20080729190630] [Slightly modified the treatment of LINE pragmas. Nils Anders Danielsson **20080729200949] [The QuickCheck test suite now gives a boolean result. Nils Anders Danielsson **20080730021226] [Merged/removed some utilities. Nils Anders Danielsson **20080730021907 + Removed two separate copies of on, for instance. ] [Improved the handling of ranges. Nils Anders Danielsson **20080730025558 + A range is now a list of intervals. Hence operators are easier to handle. ] [Some ad-hoc tweaks to preserve ranges. Nils Anders Danielsson **20080730030240 + Ranges in the internal syntax often used to be incorrect (pointing to the definition site of a constructor instead of the use site, for instance). This patch improves the situation somewhat. However, some of the tweaks are probably unnecessary (or perhaps even incorrect), and more tweaks should probably be added. It would be nice if someone with more knowledge about the Agda internals rectified this situation. ] [Partial fix of the problem with highlighting of ambiguous constructors. Nils Anders Danielsson **20080730143642 + The source locations (definition sites) emitted by the highlighting code for ambiguous constructors was previously likely to be wrong. This patch corrects the situation by highlighting disambiguated code. + One issue remains: Currently constructors are not highlighted at all in with clauses. The reason is that I have not figured out a simple way to access the internal representation of with clauses. + Another potential problem is that some names, obtained from the internal representation of a given module's code, have ranges (use sites) corresponding to locations in other files. This problem is solved by ignoring such names, but the underlying problem (if any) should probably be tackled instead. ] [fixed issue 91 with constructors not being highlighted in with clauses ulfn@cs.chalmers.se**20080731073802 + The name of the with functions are now generated when + scope checking and stored in the abstract syntax. ] [remove the range information from the generated type of a with function ulfn@cs.chalmers.se**20080731085754 + This should avoid bogus error ranges when the type is incorrect. ] [the range for errors in the type of a with function is now the range of the clauses ulfn@cs.chalmers.se**20080731092515] [disabled highlighting of blocked terms ulfn@cs.chalmers.se**20080731095338 + It's more useful to see the cause of the blocking + and in many cases this is obscured by the highlighting + of the blocked term. ] [kill ranges on internally generated terms to avoid highlighting looking at them ulfn@cs.chalmers.se**20080731134601] [killed a few more ranges for generated terms ulfn@cs.chalmers.se**20080801104940] [Fixed issue 93 ("Lisp nesting exceeds `max-lisp-eval-depth'"). Nils Anders Danielsson **20080805160341] [fixed a bug with eta expansion in module application ulfn@cs.chalmers.se**20080807100211 + Module applications are now properly eta expanded + and the error message when a module is applied to + the wrong number of arguments no longer mentions + Prop. ] [Fixed issue 94 (panic in positivity checker) and improved ranges for positivity errors ulfn@cs.chalmers.se**20080807114337] [fixed issue 95 with unpredictible invertibility ulfn@cs.chalmers.se**20080812095518] [Added indent. Nils Anders Danielsson **20080808135540] [Recursion behaviours are now printed if -vterm.behaviours:30 is used. Nils Anders Danielsson **20080808140527] [fixed a non termination issue with the fix to issue 95 ulfn@cs.chalmers.se**20080812100130] [fixed issue 98 (bug in checking patterns of with clauses) ulfn@cs.chalmers.se**20080813103027] [fixed problem with highlighting of constructors in arguments to overloaded constructors ulfn@cs.chalmers.se**20080815095226] [Clarification of README + more of the install-script patrikj@chalmers.se**20080604074348] [Corrected README after the addition of "Agda/" to the source tree patrikj@chalmers.se**20080604074539] [Readme fixes: darcs repo moved to code.haskell.org, some minor errors corrected, the Ubuntu install script updated patrikj@chalmers.se**20080806221609] [fixed Interaction.Imports.matchFileName for Windows. makoto.takeyama@aist.go.jp**20080827085937] [option for sized types ulfn@cs.chalmers.se**20080901110642] [builtins for the Size type ulfn@cs.chalmers.se**20080901110711] [allow --show-implicit in OPTIONS pragma ulfn@cs.chalmers.se**20080901114050] [added place holder for polarity information to definitions ulfn@cs.chalmers.se**20080901114902] [fixed a bug in the file name / module name correspondance check ulfn@cs.chalmers.se**20080901122706] [paved the way for adding subtyping ulfn@cs.chalmers.se**20080901134211] [compute polarity information (using the positivity checker) ulfn@cs.chalmers.se**20080901143141] [fixed error messages to take subtyping into account ulfn@cs.chalmers.se**20080901143912] [special rules for comparing sizes ulfn@cs.chalmers.se**20080902093934] [minor bug in positivity checker ulfn@cs.chalmers.se**20080902094200] [possible impossible and updates to error messages ulfn@cs.chalmers.se**20080902094218] [simplified rules for size comparison ulfn@cs.chalmers.se**20080902095140] [changed some debug printing ulfn@cs.chalmers.se**20080902101206] [failing test case for suspicious termination argument ulfn@cs.chalmers.se**20080902132312] [added linearity constraint in positivity checker ulfn@cs.chalmers.se**20080902141348 For instance, in data _==_ (A : Set) : Set -> Set where refl : A == A _==_ is no longer considered positive in its first argument. ] [compute polarity information for size indices ulfn@cs.chalmers.se**20080902153427] [treat size suc as a constructor in termination checker ulfn@cs.chalmers.se**20080903092612] [collect size constraints ulfn@cs.chalmers.se**20080903100503] [add an indirection for the fontset to use for Agda makoto.takeyama@aist.go.jp**20080904060247] [solving of size constraints ulfn@cs.chalmers.se**20080904145305] [call the size constraint solving after each declaration ulfn@cs.chalmers.se**20080904161436] [removed bug in termination checker causing call to be collected up to four times andreas.abel@ifi.lmu.de**20080904155031] [termination and sized types test cases andreas.abel@ifi.lmu.de**20080904160226] [fixed issue 103 (bug with positivity checking and open public) ulfn@cs.chalmers.se**20080923104423] [error files for make fail ulfn@cs.chalmers.se**20080923104652] [Made the default fontset on other platforms match the Windows one. Nils Anders Danielsson **20080905132110] [Added the bindings len ↦ ≰ and gen ↦ ≱. Nils Anders Danielsson **20080905132208] [Removed unnecessary use of unsafePerformIO. Nils Anders Danielsson **20080915174736] [added a unique number to names of generated with functions ulfn@cs.chalmers.se**20080923133039] [fixed issue 104 (make case not generating with applications when it should) ulfn@cs.chalmers.se**20080923133119]