[Agda] Re: Avoid GHC 6.10.1 (for now)
Nils Anders Danielsson
nad at Cs.Nott.AC.UK
Wed Nov 12 12:41:41 CET 2008
On 2008-11-12 03:37, Darin Morrison wrote:
>
> It looks like it isn't really an Agda issue but a readline problem:
Readline is only used by the unsupported agda -I. In order to get rid of
this problem I suggest that we choose one of the following two
solutions:
1) Drop readline in favour of the simple putStrLn/getLine method which
is used under Windows.
2) Drop readline in favour of editline. I tried to use agda -I with
editline under Linux, and it worked fine, also for Unicode input. Can
Mac and Windows users try the attached patch? Does it compile and run
flawlessly?
--
/NAD
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
-------------- next part --------------
Wed Nov 12 11:38:35 GMT 2008 Nils Anders Danielsson <nils.anders.danielsson at gmail.com>
* Dropped readline in favour of editline. Enabled editline also under Windows.
New patches:
[Dropped readline in favour of editline. Enabled editline also under Windows.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081112113835] {
hunk ./Agda.cabal 31
binary >= 0.4.4 && < 0.5,
zlib >= 0.4.0.1 && < 1,
filepath >= 1.1 && < 2,
- process >= 1.0 && < 2
+ process >= 1.0 && < 2,
+ editline == 0.2.*
if impl(ghc >= 6.10)
build-depends: ghc-prim >= 0.1 && < 1
hunk ./Agda.cabal 35
- if !os(windows)
- build-depends: readline >= 1.0.1 && < 2
build-tools: happy >= 1.15 && < 2,
alex >= 2.0.1 && < 3
exposed-modules: Agda.Main
hunk ./src/full/Agda/Utils/ReadLine.hs 1
-{-# LANGUAGE CPP #-}
-
{-| A wrapper for readline. Makes it easier to handle absence of readline.
-}
module Agda.Utils.ReadLine where
hunk ./src/full/Agda/Utils/ReadLine.hs 5
-#ifndef mingw32_HOST_OS
-import qualified System.Console.Readline as RL
-#endif
+import qualified System.Console.Editline.Readline as RL
import System.IO
import Agda.Utils.Unicode
hunk ./src/full/Agda/Utils/ReadLine.hs 11
import Agda.Utils.Monad
-readline :: String -> IO (Maybe String)
+readline :: String -> IO (Maybe String)
+readline s = fmap fromUTF8 <$> RL.readline s
+
addHistory :: String -> IO ()
hunk ./src/full/Agda/Utils/ReadLine.hs 15
-#ifdef mingw32_HOST_OS
-readline s = do
- putStr s
- hFlush stdout
- l <- getLine
- return $ Just $ fromUTF8 l
-addHistory s = return ()
-#else
-readline s = fmap fromUTF8 <$> RL.readline s
addHistory s = RL.addHistory $ toUTF8 s
hunk ./src/full/Agda/Utils/ReadLine.hs 16
-#endif
}
Context:
[Updated Ulf's email address.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081111154930]
[binary >= 0.4.4 is now required.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081111154444
+ Some earlier versions lead to a slowdown under GHC 6.10.1.
]
["Removed Agda.Compiler.MAlonzo.Pretty" made the build fail. Fixed this.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081111154333]
[removed dependencies on deleted module Compiler.MAlonzo.Pretty
ulfn at cs.chalmers.se**20081110114614]
[Added _∘_ for stream processors.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081110213331]
[Removed Agda.Compiler.MAlonzo.Pretty.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081110110816
+ This module was copied from the Haskell base library (and slightly
modified), so either it would have to be removed, or our LICENSE
file would have to be updated.
+ The modified module inserted some disambiguating parentheses when
pretty-printing expressions. I took care of this by preprocessing
expressions instead, inserting parentheses everywhere (this can of
course be improved).
]
[Improved a test.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081110102456]
[Fixed bug 92: The compiler chokes on certain module names.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081110095731]
[Switched from defaultMainWithHooks to defaultMain.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081109111929
+ Because defaultUserHooks is deprecated and most users do not need to
run ./configure.
]
[Forced Agda to use a specific version of QuickCheck.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081109105205
+ The development version of QuickCheck includes an Applicative
instance for Gen, which conflicts with an instance in the Agda code
base.
]
[Removed -O. Cabal now turns on optimisations by default.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081105183407]
[Made Agda compile under GHC 6.8.3 again.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081105140133]
[Made Agda work under GHC 6.10.1.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081104210226]
[U+200B is not whitespace (according to Data.Char.isSpace from base 4).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081104210046]
[wrapper and some tests for the implementation of warshall's algorithm
ulfn at cs.chalmers.se**20081104115115]
[Changed "Compute normal form" to "Evaluate term to normal form".
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081031212459]
[Improved formatting of error message.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081029113616]
[fixed issue109 where inverting point-free definition caused a crash
ulfn at cs.chalmers.se**20081029104753]
[added a PrettyTCM instance for lists
ulfn at cs.chalmers.se**20081029104712]
[etacontract when unifying indicies for pattern matching
ulfn at cs.chalmers.se**20081029095240]
[fixed a problem with absurd lambdas and the emacs mode
ulfn at cs.chalmers.se**20081028124536]
[a simple typechecker for the locally nameless prototype
ulfn at cs.chalmers.se**20081028110707]
[added absurd lambdas
ulfn at cs.chalmers.se**20081028110104
If A is an empty (constructorless) type, then
\() : (x : A) -> B and
\{} : {x : A} -> B
The usual lambda sugar applies, but the absurd pattern must
appear last:
\x y z () -- OK
\x () y z -- NOT OK (\x () will do in this case)
]
[Added bindings for tie (⁀) and undertie (‿).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081027074329]
[use the integer generator to generate arbitrary numbers (to get reasonable sizes)
ulfn at cs.chalmers.se**20081024140940]
[fixed silly mistake in previous patch
ulfn at cs.chalmers.se**20081024132430]
[fixed issue 107 (function inversion + overlapping patterns = loop)
ulfn at cs.chalmers.se**20081024131802]
[ghc-6.10 compatibility (+changing OPTIONS pragma to LANGUAGE when possible)
ulfn at cs.chalmers.se**20081023153229]
[added Andreas as author
ulfn at cs.chalmers.se**20081023152410]
[fixed problem with termination checking and nat literals (issue 106)
ulfn at cs.chalmers.se**20081023100722]
[Submitted version of HCAR entry for November 2008.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081022120350]
[Draft of HCAR entry for November 2008.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081009195427]
[fixed bug with splitting when a constructor was imported several times
ulfn at cs.chalmers.se**20081009103706]
[fixed some issues with the quickcheck test suite
ulfn at cs.chalmers.se**20081006145407]
[upgraded to QuickCheck-2.1
ulfn at cs.chalmers.se**20081006124755]
[removed BUILTIN IO (use COMPILED_TYPE instead)
ulfn at cs.chalmers.se**20081006124746]
[removed failing test case for ambiguous import
ulfn at cs.chalmers.se**20081001105933]
[COMPILED_TYPE IO also does BUILTIN IO
ulfn at cs.chalmers.se**20081001105810]
[pick first file when more than one match import
ulfn at cs.chalmers.se**20081001105652]
[Made the customisation buffer easier to understand (hopefully).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080925004354]
[Fixed bug: fontset-agda2 should not be created if agda2-fontset-name is nil.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080925003128]
[fixed liftIO in TCM to only wrap IOExceptions as TCM exceptions
ulfn at cs.chalmers.se**20080924082857]
[fixed issue 104 (make case not generating with applications when it should)
ulfn at cs.chalmers.se**20080923133119]
[added a unique number to names of generated with functions
ulfn at cs.chalmers.se**20080923133039]
[error files for make fail
ulfn at cs.chalmers.se**20080923104652]
[fixed issue 103 (bug with positivity checking and open public)
ulfn at cs.chalmers.se**20080923104423]
[termination and sized types test cases
andreas.abel at ifi.lmu.de**20080904160226]
[removed bug in termination checker causing call to be collected up to four times
andreas.abel at ifi.lmu.de**20080904155031]
[call the size constraint solving after each declaration
ulfn at cs.chalmers.se**20080904161436]
[solving of size constraints
ulfn at cs.chalmers.se**20080904145305]
[collect size constraints
ulfn at cs.chalmers.se**20080903100503]
[treat size suc as a constructor in termination checker
ulfn at cs.chalmers.se**20080903092612]
[compute polarity information for size indices
ulfn at cs.chalmers.se**20080902153427]
[added linearity constraint in positivity checker
ulfn at 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.
]
[failing test case for suspicious termination argument
ulfn at cs.chalmers.se**20080902132312]
[changed some debug printing
ulfn at cs.chalmers.se**20080902101206]
[simplified rules for size comparison
ulfn at cs.chalmers.se**20080902095140]
[possible impossible and updates to error messages
ulfn at cs.chalmers.se**20080902094218]
[minor bug in positivity checker
ulfn at cs.chalmers.se**20080902094200]
[special rules for comparing sizes
ulfn at cs.chalmers.se**20080902093934]
[fixed error messages to take subtyping into account
ulfn at cs.chalmers.se**20080901143912]
[compute polarity information (using the positivity checker)
ulfn at cs.chalmers.se**20080901143141]
[paved the way for adding subtyping
ulfn at cs.chalmers.se**20080901134211]
[fixed a bug in the file name / module name correspondance check
ulfn at cs.chalmers.se**20080901122706]
[added place holder for polarity information to definitions
ulfn at cs.chalmers.se**20080901114902]
[builtins for the Size type
ulfn at cs.chalmers.se**20080901110711]
[option for sized types
ulfn at cs.chalmers.se**20080901110642]
[Removed unnecessary use of unsafePerformIO.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080915174736]
[Added the bindings len ↦ ≰ and gen ↦ ≱.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080905132208]
[Made the default fontset on other platforms match the Windows one.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080905132110]
[add an indirection for the fontset to use for Agda
makoto.takeyama at aist.go.jp**20080904060247]
[allow --show-implicit in OPTIONS pragma
ulfn at cs.chalmers.se**20080901114050]
[fixed Interaction.Imports.matchFileName for Windows.
makoto.takeyama at aist.go.jp**20080827085937]
[Readme fixes: darcs repo moved to code.haskell.org, some minor errors corrected, the Ubuntu install script updated
patrikj at chalmers.se**20080806221609]
[Corrected README after the addition of "Agda/" to the source tree
patrikj at chalmers.se**20080604074539]
[Clarification of README + more of the install-script
patrikj at chalmers.se**20080604074348]
[fixed problem with highlighting of constructors in arguments to overloaded constructors
ulfn at cs.chalmers.se**20080815095226]
[fixed issue 98 (bug in checking patterns of with clauses)
ulfn at cs.chalmers.se**20080813103027]
[fixed a non termination issue with the fix to issue 95
ulfn at cs.chalmers.se**20080812100130]
[fixed issue 95 with unpredictible invertibility
ulfn at cs.chalmers.se**20080812095518]
[Recursion behaviours are now printed if -vterm.behaviours:30 is used.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080808140527]
[Added indent.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080808135540]
[Fixed issue 94 (panic in positivity checker) and improved ranges for positivity errors
ulfn at cs.chalmers.se**20080807114337]
[fixed a bug with eta expansion in module application
ulfn at 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 93 ("Lisp nesting exceeds `max-lisp-eval-depth'").
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080805160341]
[killed a few more ranges for generated terms
ulfn at cs.chalmers.se**20080801104940]
[kill ranges on internally generated terms to avoid highlighting looking at them
ulfn at cs.chalmers.se**20080731134601]
[disabled highlighting of blocked terms
ulfn at 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.
]
[the range for errors in the type of a with function is now the range of the clauses
ulfn at cs.chalmers.se**20080731092515]
[remove the range information from the generated type of a with function
ulfn at cs.chalmers.se**20080731085754
+ This should avoid bogus error ranges when the type is incorrect.
]
[fixed issue 91 with constructors not being highlighted in with clauses
ulfn at cs.chalmers.se**20080731073802
+ The name of the with functions are now generated when
+ scope checking and stored in the abstract syntax.
]
[Partial fix of the problem with highlighting of ambiguous constructors.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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.
]
[removed __HADDOCK__ ifdefs
ulfn at cs.chalmers.se**20080730121228]
[fixed a bug when inverting functions with dot patterns
ulfn at cs.chalmers.se**20080730114450]
[fixed some problems in the benchmark suite
ulfn at cs.chalmers.se**20080730114419]
[fixed issue 36 where the same name could be exported twice from a module
ulfn at cs.chalmers.se**20080730093432]
[put back -Werror
ulfn at cs.chalmers.se**20080730092324
If there's a problem with Haddock, fix Haddock.
-Werror is crucial.
]
[fixed issue 90 improving Set != Set1 error message
ulfn at cs.chalmers.se**20080730082757]
[Some ad-hoc tweaks to preserve ranges.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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.
]
[Improved the handling of ranges.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080730025558
+ A range is now a list of intervals. Hence operators are easier to
handle.
]
[Merged/removed some utilities.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080730021907
+ Removed two separate copies of on, for instance.
]
[The QuickCheck test suite now gives a boolean result.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080730021226]
[Slightly modified the treatment of LINE pragmas.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080729200949]
[Removed some unused and unfinished instances.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080729190630]
[Simplified the interface to the syntax highlighting code.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080729170232]
[removed unstructured verbosity output
ulfn at cs.chalmers.se**20080728141300]
[extended function inversion to handle nested invertible functions
ulfn at cs.chalmers.se**20080728120539
f (g x) = c will now solve for x if f and g are invertible
]
[fixed issue 89 with normalisation stopping early for corecursive definitions
ulfn at cs.chalmers.se**20080728093430]
[added failing test case for uncurried metavariables
ulfn at cs.chalmers.se**20080729092148]
[Made checkModuleName interact better with syntax highlighting.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080729122214]
[Added allNames.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080728192230]
[Added a newtype for ambiguous QNames in the abstract syntax.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080728152414]
[Improved some comments.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080728124632]
[Noted that a comment seems to be out of date.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080725161307]
[Added the QED symbol (∎).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080725161152]
[Module name file name correspondence is now enforce also for the main module
ulfn at cs.chalmers.se**20080725110226]
[fixed issue 85
ulfn at cs.chalmers.se**20080725101956]
[fixed issue 87 by improving the error message
ulfn at cs.chalmers.se**20080725101129]
[fixed issue 84 (corecursion and absurd clauses)
ulfn at cs.chalmers.se**20080725094056]
[Reduced the differences between the default bindings under Emacs 22 and 23.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080721155521]
[Removed duplicate occurrence of ¬.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080721134208]
[patched the Agda1 to Agda2 translator to concrete syntax changes
ulfn at cs.chalmers.se**20080619121049]
[Agda now compiles with binary-0.4.2
ulfn at cs.chalmers.se**20080619121032]
[Updated the code for Haddock 2.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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.
]
[Haddock comments cannot be given for instances.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080719200805]
[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.
]
[Made installation of the Emacs mode slightly easier.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080719123400]
[Replaced text about the TeX input method with text about the Agda one.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080719114852]
[Explained how to rebuild the batch-mode tool when upgrading.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080719110936]
[Stopped referring to the batch-mode tool as an "interpreter".
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080719110756]
[Defined an Agda-specific input method.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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.
]
[Defined some Agda-specific abbrevs.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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.
]
[Syntax table change: Made _ and ! punctuation characters.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080706102611]
[Removed unnecessary code.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080706101550]
[made malonzo the default compiler
ulfn at cs.chalmers.se**20080617190432]
[changed simple-lib to be MAlonzo compatible
ulfn at cs.chalmers.se**20080617173933]
[fixed a bug in MAlonzo with foreign constructors being incorrectly qualified
ulfn at cs.chalmers.se**20080617173823]
[fixed a bug in Haskell code generation for primitive functions
ulfn at cs.chalmers.se**20080617173746]
[Agda has now been tested with GHC 6.8.3.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080618132825]
[use -fno-warn-overlapping-patterns when compiling generated Haskell
ulfn at cs.chalmers.se**20080617161526]
[MAlonzo now checks the types of foreign functions and constructors
ulfn at cs.chalmers.se**20080617160323]
[updated simple-lib to the new COMPILED_DATA pragma
ulfn at cs.chalmers.se**20080617151603]
[changed COMPILED_DATA pragma to include Haskell type name
ulfn at cs.chalmers.se**20080617151450]
[COMPILED_TYPE pragma and translation to Haskell types
ulfn at cs.chalmers.se**20080617135508]
[infrastructure for checking the types of foreign functions
ulfn at cs.chalmers.se**20080617111441]
[renamed SerialiseShare.hs to Serialise.hs
ulfn at cs.chalmers.se**20080617105229]
[removed unused Serialise.hs
ulfn at cs.chalmers.se**20080617103139]
[Fixed comment.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080617143949]
[Updated the MAlonzo README in response to a recent patch.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080616150610]
[MAlonzo now checks that main has type IO a (issue 82)
ulfn at cs.chalmers.se**20080616145536]
[Removed the primitive IO functions, along with the UNIT builtin.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080616145220
+ Use the FFI for IO.
+ Note that this change may break the old Alonzo.
]
[added test case for issue 81
ulfn at cs.chalmers.se**20080616110202]
[fixed bug in emptyness checker (issue 81) and improved error message
ulfn at cs.chalmers.se**20080616105953]
[Made it possible to use forall-style declarations for record parameters.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080612154848]
[Merged two related test cases.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080611144838]
[fixed issue 76 (missing parenthesis around roundfix operators)
ulfn at cs.chalmers.se**20080611133309]
[error message comparison in make fail ignores whitespace
ulfn at cs.chalmers.se**20080611131946]
[fixed issue 63 where the scope checker allowed duplicate constructors
ulfn at cs.chalmers.se**20080611130919]
[fixed issue 80 with constructor types not being properly unfolded
ulfn at cs.chalmers.se**20080611125653]
[always pull patches from standard lib
ulfn at cs.chalmers.se**20080611125629]
[added test case for forall-style datatype parameters
ulfn at cs.chalmers.se**20080611125612]
[Made it possible to use forall-style declarations for module parameters.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080611121448]
[fixed bug with metavariables not being expanded in datatype declarations
ulfn at cs.chalmers.se**20080611100554]
[Made it possible to use forall-style declarations for (co)data parameters.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080610152516]
[added the stream eating example
ulfn at cs.chalmers.se**20080605104633]
[do eta contraction when termination checking
ulfn at cs.chalmers.se**20080604163705]
[README adapted to the top-level hierachical name Agda
andres.sicard at gmail.com**20080604160702]
[MAlonzo FFI support
makoto.takeyama at aist.go.jp**20080604155931]
[disallow shadowing of module names
ulfn at cs.chalmers.se**20080604160433]
[removed termination examples with constructor names not mattering
ulfn at cs.chalmers.se**20080604150504]
[termination-check-ignore-constructor-names
andreas.abel at ifi.lmu.de*-20080604130641]
[added disclaimer to the interactive mode
ulfn at cs.chalmers.se**20080604131348]
[termination-check-ignore-constructor-names
andreas.abel at ifi.lmu.de**20080604130641]
[added-3-termination-examples-to-makefile
andreas.abel at ifi.lmu.de**20080604130006]
[more-termination-examples
andreas.abel at ifi.lmu.de**20080604124753]
[clear undo history when loading to fix memory leak (issue 67)
ulfn at cs.chalmers.se**20080604123721]
[fixed issue 74 with make case in modules with implicit parameters
ulfn at cs.chalmers.se**20080604115141]
[require binary-0.4.1
ulfn at cs.chalmers.se**20080604095605]
[fixed some problems with make case and dot patterns (issue 73)
ulfn at cs.chalmers.se**20080604091843]
[removed support for as-patterns
ulfn at cs.chalmers.se**20080604083555]
[Removed the Agda-aware undo feature from the Emacs mode.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080604124142]
[fixed issue 54 (panic in the coverage checker)
ulfn at cs.chalmers.se**20080603144441]
[normalise dot patterns when using them for termination (fixes issue 53)
ulfn at cs.chalmers.se**20080603142725]
[fixed bug in with functions where dot patterns were needed to evaluate the types
ulfn at cs.chalmers.se**20080603132427]
[Added an example which does not pass the productivity checker.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080603082115]
[fixed bug with productivity checker messing up some termination problems
ulfn at cs.chalmers.se**20080602161850]
[Improved a property.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080602213743]
[Added a lexer and support for parsing qualified names.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080602211233
+ Including qualified operator applications and sections.
]
[Added separate and twoAdjacent.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080602211018]
[productivity checking for corecursive functions
ulfn at cs.chalmers.se**20080602151626]
[some utility functions for mutual blocks
ulfn at cs.chalmers.se**20080602124410]
[made the termination checker ignore coconstructors
ulfn at cs.chalmers.se**20080602081857]
[safe unfolding of corecursive functions
ulfn at cs.chalmers.se**20080602081755]
[fixed silly mistake in lexer
ulfn at cs.chalmers.se**20080602073708]
[codata and corecursion (only syntax)
ulfn at cs.chalmers.se**20080530172437]
[made agda1 to agda2 translator compile
ulfn at cs.chalmers.se**20080530151358]
[Removed associativity from the fixity type.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080601222949]
[Added more tests. Rearranged files.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080601202028]
[Dropped the transitivity emulation.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080531195333]
[Improved the precedence graph interface.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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).
]
[Put all modules under the top-level hierachical name Agda.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080530150335
+ This ensures that we do not pollute the Haskell module name space
too much.
]
[changed a lot of Ints to Integers
ulfn at cs.chalmers.se**20080530124136]
[fixed bug with modules in let
ulfn at cs.chalmers.se**20080530073854]
[fixed printing of impossibles in batch mode
ulfn at cs.chalmers.se**20080530073815]
[Suggested dropping the transitivity emulation.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080529211338]
[Made make test recheck everything by default.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080529210203
+ Change the setting of AGDA_TEST_FLAGS if you don't like this.
]
[fixed bug with overloaded constructors in parameterised modules
ulfn at cs.chalmers.se**20080527120457]
[make library-test checks out the standard library to std-lib/
ulfn at cs.chalmers.se**20080527111226
and just does darcs pull if std-lib/ exists
]
[fixed scoping bug with overloaded constructors (issue 62)
ulfn at cs.chalmers.se**20080527110953]
[Noted a problem with the suggested approach to operator precedences.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080528200029]
[Removed an unnecessary precondition.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080527185639]
[Documented and tested some invariants.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080527175348]
[Removed possibly incomprehensible remark.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150542]
[Fixed issue 75 (sometimes hidden arguments cannot be referenced by name).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150519]
[Noted that agda2-highlight-incomplete-pattern-face is currently unused.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150445
+ Since the backend treats incomplete patterns as full errors instead
of warnings.
]
[Changed some colours in "Conor's" colour scheme.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150409
+ Made termination and completeness checking errors be highlighted
differently from other errors.
]
[Fixed bug: agda2-highlight-face-groups could not be permanently customised.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150348]
[fixed some bugs
ulfn at cs.chalmers.se**20080520062303]
[TAG AFP08-2
ulfn at cs.chalmers.se**20080520061847]
[make case now preserves variable names of the original clause
ulfn at cs.chalmers.se**20080519085742]
[Added the standard library to the test-suite.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**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...
]
[Moved away or fixed many broken example files.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080518144152]
[All non-ASCII whitespace characters are now treated as whitespace.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080518123927
+ Do we also want to treat \f and \v as whitespace?
]
[Fixed bug caused by incompatible settings in .ghci.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080518122945]
[Improved documentation.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517164237]
[Simplified the syntax table code.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517164024]
[Added support for more matching parentheses.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517160238]
[Added an option to use Conor McBride's colour scheme.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517120803
+ I may not have gotten all the colours right, though.
]
[Minor simplification.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517093748]
[Added more status information to the mode line.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517091454
+ Currently just an indication of whether implicit arguments are
displayed.
]
[Moved the text mode/type checked indication forward in the mode line.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517083141]
[Fixed issue 20 (pragmas are too static in the GUI).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080517081540
+ To avoid complicating things too much I decided to reset all
options, including whether or not to display implicit arguments, on
each reload.
]
[Improved formatting of errors without ranges.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080516161852]
[fixed a bug with absurd patterns and make case (issue 73)
ulfn at cs.chalmers.se**20080516144457]
[fixed a bug with make case and with
ulfn at cs.chalmers.se**20080516143208]
[Removed unused macro.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080516151726]
[Made the Emacs UI display internal errors.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080516151415]
[TAG afp08
ulfn at cs.chalmers.se**20080515115143]
Patch bundle hash:
a749065905aa294e0ad70175830c0d7422d6b08b
More information about the Agda
mailing list