1 patch for repository http://code.haskell.org/Agda: Wed Nov 17 09:38:22 COT 2010 Andrés Sicard-Ramírez * More versions of QuickCheck are now accepted. New patches: [More versions of QuickCheck are now accepted. Andrés Sicard-Ramírez **20101117143822 Ignore-this: bd729e8db5924b47a7164ed079678cb0 ] hunk ./Agda.cabal 63 build-depends: base == 4.1.*, utf8-string == 0.3.* build-depends: mtl == 2.0.*, - QuickCheck == 2.3.*, + QuickCheck >= 2.3 && < 2.5, haskell-src-exts >= 1.9.6 && < 1.10, containers >= 0.1.0 && < 1, pretty >= 1 && < 2, Context: [Modified a constraint (see issue 360). Nils Anders Danielsson **20101117132440 Ignore-this: 33e9e8e25cb8b96db35501340ceb05e ] [Undid my fix for issue 361 because it breaks Data.Star.Decoration. andreas.abel@ifi.lmu.de**20101116223424 Extracted a successful test case from Data.Star.Decoration. Issue 361 remains open. ] [Removed an outdated file. Nils Anders Danielsson **20101116153505 Ignore-this: 53e8d53a50c05aa1a89aeb2cdfbbf51a ] [Fixed bug: Module names were not encoded correctly by the compiler. Nils Anders Danielsson **20101116153457 Ignore-this: 29204339d830f19be1fb001bd53af58b ] [Updated the error message comparison machinery. Nils Anders Danielsson **20101116151107 Ignore-this: f664b1952dde8a95512522a8d30cfd18 + GHC 7 numbers columns differently. ] [Updated an error message. Nils Anders Danielsson **20101116150825 Ignore-this: b8f111d5d4f977d2bf6c869dd9dc3e83 ] [Fixed successful test case 259c. andreas.abel@ifi.lmu.de**20101112224806] [Fixed issue 361 with unsound eta-contraction of records. andreas.abel@ifi.lmu.de**20101112175756 Put eta-contraction back to instantiateFull (undos my previous patch). Removed eta-contraction of function bodies in Def.hs. Failed test Issue259 is now successful (to no harm, imho). ] [Removed eta-contraction from instantiateFull. andreas.abel@ifi.lmu.de**20101112170915] [Removed eta-contraction in interactive normalization commands. andreas.abel@ifi.lmu.de**20101112170835] [Debug print record eta contractions on -v tc.record.eta:15. andreas.abel@ifi.lmu.de**20101112170751] [Another constraint change (see issue 360). Nils Anders Danielsson **20101111204603 Ignore-this: 7a1b290a0a2afd602cfa2f8a691c4c1c ] [Tightened version constraint to avoid Cabal problem. Nils Anders Danielsson **20101111164056 Ignore-this: 93c24d10df404190d3ca1e97ba71f24f + See issue 360. ] [MAlonzo now generates a special module MAlonzo.RTE ulfn@chalmers.se**20101109133249 Ignore-this: 27fd8a1312674ef0a690bce346963b2c containing the unsafeCoerce function instead of defining locally for each generated module ] [added RULES pragma to get rid of back-and-forth coercions of builtin naturals in Haskell backend ulfn@chalmers.se**20101109125639 Ignore-this: 600443c59d450bb69f3b5476f7541889 ] [Made the code compile with GHC 7. Nils Anders Danielsson **20101108231842 Ignore-this: b17a0d1d9293f26cb4eb6251152e59fe ] [Switched to haskell-src-exts. Nils Anders Danielsson **20101108201656 Ignore-this: fef5571be500f141fdc731f004396f44 ] [Removed warnings due to new semantics of -fwarn-incomplete-patterns. Nils Anders Danielsson **20101106213420 Ignore-this: 4e8845fb31d2d241b787b8f86f17acf6 + In GHC 7 -fwarn-simple-patterns and -fwarn-incomplete-patterns have been merged. + One potential bug was discovered in AbstractToConcrete. I inserted a use of __IMPOSSIBLE__; someone should take a closer look. ] [Switched to mtl 2.0, removed some orphan instances. Nils Anders Danielsson **20101106205212 Ignore-this: b0189e5f4d908ded5fb4bab50835d151 + Note that the Monad instance for Either has been changed: the default definition of fail is now used. ] [Made the code work with a newer version of QuickCheck. Nils Anders Danielsson **20101106194547 Ignore-this: b0cb5196391e40c7304495d049707a6d ] [Updated the tested-with field. Nils Anders Danielsson **20101106195610 Ignore-this: 4d116ee2cb5128ad719c889cf8e1c82e ] [Updated error message. Nils Anders Danielsson **20101105183404 Ignore-this: cf9e0a4da7ae2c52edb6a6c2a9dbbf90 ] [Removed space (previously: "Finished X ."; now: "Finished X."). Nils Anders Danielsson **20101105115916 Ignore-this: 86225f1f363bc3499352acbfac9c08c7 ] [New output "Finished X ." after done with importing module X. andreas.abel@ifi.lmu.de**20101105074312 This is the closing bracket to the opening "Checking X (...)." ] [In test/fail/Makefile code to create .err file for customised/NestedProjectRoots. andreas.abel@ifi.lmu.de**20101105074051] [Documented how --test can be enabled by default for darcs record. Nils Anders Danielsson **20101103200326 Ignore-this: 9b55e41cd08656b20e1c9a2aaad3810d ] [The whitespace test is now included in "make test". Nils Anders Danielsson **20101103195630 Ignore-this: 63297c8d1223f22743792cf6f163d708 ] [The fix-agda-whitespace command now has to be installed manually. Nils Anders Danielsson **20101103194049 Ignore-this: cf477419a11a432b863756ad9519c81d + This can be done by running "make install-fix-agda-whitespace". + Reason for this change: darcs runs tests in a clean repository, and with the previous setup fix-agda-whitespace was recompiled every time the test was run. ] [Incorporated Janis Voigtländers' edits. Nils Anders Danielsson **20101103184919 Ignore-this: 184fc8af3e60a2ad7ed8f9abedc90941 ] [Updated a test case. Nils Anders Danielsson **20101103121058 Ignore-this: da9b4349c6a87920a40d07f9b01a5275 ] [Added local type signatures for GHC-7 Wolfram Kahl **20101102003647 Ignore-this: 518a5d8c7ba9e8ca81a8cf3805708b0b ] [Final version of HCAR entry. Nils Anders Danielsson **20101029155048 Ignore-this: 4a56194dc247c713ca7ce0713575f91b ] [Fixed issue 355 frelindb@chalmers.se**20101101171839 Ignore-this: 97d99d0a92b7b4626d573f382def0669 ] [removed update-cabal dependency for prof and fix-whitespace make targets ulfn@chalmers.se**20101029074749 Ignore-this: aff54f00033f9ca0c66fbb3d6a2d49c4 and made fix-whitespace work without configuring first ] [the compiler now inserts coercions that play well with ghc rewrite rules (I hope) ulfn@chalmers.se**20101029074005 Ignore-this: 16e80e2e3c7eeb1544ab7a5f133c6be0 ] [Highlighting on after go-to-definition to file in different project. Nils Anders Danielsson **20101026220414 Ignore-this: 46fa2f789e14852239f269882847cd49 + Previously, if one jumped to a definition in a file in a different "project" (under a different top-level directory), then one had to load the file in order to get syntax highlighting. Now highlighting is loaded automatically (in the common case: file not modified, file not already loaded by Emacs, etc.), and the proof state is not reset (usually). ] [Fixed bug: agda2-goals-action was sometimes invoked for the wrong buffer. Nils Anders Danielsson **20101025171154 Ignore-this: 707ed4df468d581d892c3f31004bc7af ] [Made it possible to infer ♯_ using the intro command. Nils Anders Danielsson **20101025161056 Ignore-this: 881586b7b939348d9ec10d898d382f4e ] [Included .el files in the strict whitespace regime. Nils Anders Danielsson **20101027143240 Ignore-this: 85f2dadd5e84d53c59392fc9e35d6418 ] [Removed unused rule. Nils Anders Danielsson **20101027134958 Ignore-this: 4b2487e201e89e5cdfad73ebef2a5fbb ] [Fixed issue 352 by writing a program which fixes whitespace issues. Nils Anders Danielsson **20101027133434 Ignore-this: e2ea20262286cc69fa074686686d396b + The Agda build can fail on Windows if CPP-processed files don't end with newline characters. + Whenever a patch is recorded the program checks that there are no whitespace issues. + One can fix these issues by running "make fix-whitespace". This can be done automatically by darcs record if a line record prehook make fix-whitespace is added to _darcs/prefs/defaults. + I took the liberty of imposing the additional condition that there must be no trailing white space, or trailing empty lines. ] [Converted some files from Latin-1 to UTF-8. Nils Anders Danielsson **20101027121247 Ignore-this: 58138f503f4034b22b7ee89762303428 ] [First draft of HCAR entry for November 2010. Nils Anders Danielsson **20101025090454 Ignore-this: 1e6d87afc31ec9388fa28165984315d ] [dropped unnecessary coercions for nat literals ulfn@chalmers.se**20101021093647 Ignore-this: c09fe261b8814b696e560e6147573677 and made Nat-Integer conversions more rewrite-friendly ] [Minor simplifications. Nils Anders Danielsson **20101018142022 Ignore-this: 4724e0736139455f592ab95db6f43592 ] [The first non-empty line can no longer be indented using TAB. Nils Anders Danielsson **20101018141624 Ignore-this: ffd805cfbc591f8c528970a2fbf9788d + (With the default settings.) ] [Fixed bug in eri-calculate-indentation-points. Nils Anders Danielsson **20101018135421 Ignore-this: ed0a4c7c4cf91dc61f26c78ddd478a50 + Bogus results were sometimes returned when the function was invoked on the first line of a buffer. ] [Updated some comments. Nils Anders Danielsson **20101018135016 Ignore-this: ea7309566d7d5cdd582eceee469cb874 ] [Fixed bug in eri-new-indentation-point. Nils Anders Danielsson **20101018133600 Ignore-this: 61f0ada4776d5df08d6a1e22461015b1 + Bogus results were sometimes returned when the function was invoked at or before the first line containing text. ] [Added save-excursion in eri-calculate-indentation-points-on-line. Nils Anders Danielsson **20101018132700 Ignore-this: ba038f38cfae342697462571e145a33 ] [Removed agda2-indentation. Nils Anders Danielsson **20101018125657 Ignore-this: 9346242956ae91af7fdf814bce37497d ] [Fixed compiler bug: no function was generated for INFINITY, only a type. Nils Anders Danielsson **20101020184358 Ignore-this: 81d662d6a8dbc968c8db904ea32754ac ] [Fixed problem with agda2-restart: GHCi has become harder to kill. Nils Anders Danielsson **20101020134359 Ignore-this: 1d3275a1e7046b4dfda2013feeb232e1 ] [Removed use of the TupleSections extension. Nils Anders Danielsson **20101018130001 Ignore-this: ae1b33d582ec9ab26c40a4eb02d62f2e + Perhaps Agda can now be built using GHC 6.10. ] [Typo in successful test case module name. andreas.abel@ifi.lmu.de**20101016155146] [Making eta-expansion even lazier. andreas.abel@ifi.lmu.de**20101015184808 In conversion test, only eta-expand when comparing a record against a neutral or another record, no longer when comparing against a meta variable. ] [No change. Some comments and debug prints for MetaVar code. andreas.abel@ifi.lmu.de**20101015175257] [Fixed issue 331. Meta-variables created by performKill had not been eta-expanded. andreas.abel@ifi.lmu.de**20101015162336 Just added one line to MetaVars/Occurs.hs, the rest is refactoring. ] [Added online to 2-2-10 release notes on projections preserve guardedness. andreas.abel@ifi.lmu.de**20101015153146] [Made eta-expansion of metavars more lazy in MetaVars.hs/etaExpandListeners. Solves issue 348. andreas.abel@ifi.lmu.de**20101015153050] [Projections preserve guardedness in the productivity (=termination) checker. andreas.abel@ifi.lmu.de**20101014075721] [Fixed issue 347 (eta expanding meta var forgets irrelevant record fields). andreas.abel@ifi.lmu.de**20101011172612 While this fix is indispensible for the soundness of Agda, note that some meta-variables which had been soundly resolved before, dont resolve any more. record R : Set where constructor mkR field fromR : A reflR : (r : R) -> r == r reflR r = refl -- unsolved metas here, only (refl {a = r}) works ] [Failing test cases: record constructors do not count as structural increase. andreas.abel@ifi.lmu.de**20101005133033] [Fixed issue 345, internal error in Auto Fredrik Lindblad **20101005083341 Ignore-this: 148bf7d44f7d0bf03118fd16dbedd5a6 ] [Release notes for irrelevant declarations and projections. andreas.abel@ifi.lmu.de**20101004170425] [Fixed issue 344: highlighting of field names. Nils Anders Danielsson **20101004135914 Ignore-this: 6df1203751a6683686c23d9c96e147ba ] [Updated an entry: record patterns did not exist before Agda 2.2.8. Nils Anders Danielsson **20101004135527 Ignore-this: 86bc4abd4bb55310ec8a47fc1f9ff9ef ] [Termination checker: stripping of a record constructor is no longer counted as decrease. andreas.abel@ifi.lmu.de**20101004100900] [Started release notes for 2.2.10. andreas.abel@ifi.lmu.de**20101004085937] [Failing test for termination checking translated record pattern. (see issue 334) andreas.abel@ifi.lmu.de**20101002192955] [Termination checker understands now record projections. andreas.abel@ifi.lmu.de**20101002192314 Added a field funProjection to Function definitions which indicates whether the function is a projection and which argument is the record argument. The termination checker knows that proj r <= r. ] [Compile DontCare as error instead of (). andreas.abel@ifi.lmu.de**20101001133559] [Fixed issue 342 (type checking constructors turned Funs into Pis). andreas.abel@ifi.lmu.de**20101001133519] [move the __IMPOSSIBLE__ triggered by the impossible failing test to a separate file ulfn@chalmers.se**20100930100615 Ignore-this: fe13424136446099202517ba44bbdcad to prevent the line number in the error message from changing ] [missing error message for failing test ulfn@chalmers.se**20100930095858 Ignore-this: 906099a500bbc7b067a6972ee1f75675 ] [added projections for irrelevant record fields (with --irrelevant-projections) ulfn@chalmers.se**20100930095832 Ignore-this: 595a7cc87104ac1360bd2d2e7ab4267b ] [Compiler now ignores irrelevant definitions and irrelevant arguments. andreas.abel@ifi.lmu.de**20100929193203] [Fixed typo. andreas.abel@ifi.lmu.de**20100929181610] [Minor factorization of duplicated code. andreas.abel@ifi.lmu.de**20100929181122] [Spotted opportunity for irrelevance in examples/simple-lib (two dots ;-)). andreas.abel@ifi.lmu.de**20100929150655] [.err file to testcase andreas.abel@ifi.lmu.de**20100929145205] [Testcase for bad irrelevant projections. andreas.abel@ifi.lmu.de**20100929145143] [Preliminary fix of issue 337 (generation of with functions in the presence of irrelevance). andreas.abel@ifi.lmu.de**20100929144945] [Added irrelevant function and axiom declarations .ident : Type andreas.abel@ifi.lmu.de**20100929084645 These can only be used in irrelevant positions. They can use other irrelevant declarations. ] [Test case for absurd matching on irrelevant empty type. andreas.abel@ifi.lmu.de**20100928201747] [Test cases for untyped and typed lambda, demonstrating that \ x is not \ (x : _) andreas.abel@ifi.lmu.de**20100928173706] [Typesig, comment, and some factoring for function TC.Rules.Term.checkArguments'. andreas.abel@ifi.lmu.de**20100928151619] [Bumped version to 2.2.9. Nils Anders Danielsson **20100927203646 Ignore-this: d8e25eefb66fc2fac2cd3cab5b5367b ] [TAG 2.2.8 Nils Anders Danielsson **20100927162925 Ignore-this: 24db4b37e559935c9cd6f81f8a90a6f7 ] Patch bundle hash: 86be359882b5b8160e0387f639170a23ad5e4a1b