[Agda] Improving reload performance in emacs mode

Mon Nov 24 16:14:43 CET 2008

Hi all,

Agda's interactive emacs mode is really nice to work with, but reloading
the current file (C-c C-x C-l) can be quite slow. On my machine (an old
laptop), reloading part of a multi-module program that imports several
standard library modules can take half a minute or more. Profiling the
standalone typechecker shows that most of the time is spent decoding the
interface files that are read from disk. This is done by decoding functions
in module Agda.Typechecking.Serialise; they are apparently carefully
designed to maximise sharing in the typechecker's internal structures, and
are probably not easy to speed up.

However, it seems a shame to repeat this work on every reload, even if the
interfaces haven't changed. I've patched Agda to maintain a cache of
previously decoded interfaces that is preserved across reloads (details
below for those interested). This does not do anything for the initial
loading of a file, but it speeds up subsequent reloads significantly.  The
implementation can certainly be improved, but the patch does not seem to
break anything, and hopefully it shows that caching interfaces is a fairly
easy way to improve the reloading performance. It would be nice if
something like this could be implemented in the official repository,
especially for those of us with slow hardware!
Thanks,

Kasper

Patch details:

Actually, Agda already maintains a cache of decoded interfaces, in the
"stVisitedModules" component of the typechecking state. This is used to
avoid reading and decoding modules more than once during a single run of
the typechecker, but the cached interfaces are discarded when reloading. In
addition to caching, the stVisitedModules component is also used to keep
track of which interfaces have been merged into the typechecker's proof
state. Therefore, simply preserving it across reloads would not work.
Because I wanted to be sure not to change the behaviour of the typechecker,
I duplicated part of this functionality into a new state component,
"stDecodedModules". A better way to implement this would probably be to
separate the interface caching from the tracking of visited modules.
Perhaps someone who is more familiar with the internals of the typechecker
can have a look at this?

The attached darcs patch bundle consists of two parts:
- The first patch adds stDecodedModules to the typechecking state, provides
  actions to manipulate it, and ensures that it is preserved across calls
  to cmd_load and cmd_reset (in Agda.Interactive.GhciTop). It also adds the
  logic to actually store and load interfaces in the "getInterface"
  function (in Agda.Interaction.Imports). Cached interfaces are only reused
  if the corresponding interface file on disk exists and is not newer.
- The second patch threads the cached interfaces through the "createInterface"
  function, where a separate run of the typechecker is performed.
Also attached is the module Benchmark.hs, which performs "cmd_load"
repeatedly on a specified file.

On a fast machine (not my laptop), the patches produce these results:
- The first patch reduces the reload time of Everything.agda from the
  standard library from 9 seconds to less than one second (measured with
  the benchmarking module). In the emacs mode, the speedup is less
  impressive, but the reload time is still reduced by about two thirds.
- The second patch, surprisingly, doesn't seem to have any effect. I would
  have expected this change to be necessary if the source file has changed,
  but perhaps it can be omitted?

There is currently no command to clear the cache, but I haven't found this
to be a problem (if necessary, type "ioTCM resetState" in the *ghci* buffer).
-------------- next part --------------
Mon Nov 24 13:09:26 CET 2008  Kasper Brink <kjbrink at students.cs.uu.nl>
  * Improved reload performance by caching interfaces.
  + added a cache for decoded interfaces to the typechecking state, which
    is preserved across reloads.
  + changed "getInterface" to store and reuse previously decoded interfaces.

Mon Nov 24 13:38:52 CET 2008  Kasper Brink <kjbrink at students.cs.uu.nl>
  * Threaded the cached interfaces through "createInterface".
  + createInterface performs a separate run of the typechecker; make the
    cached interfaces available there as well.

New patches:

[Improved reload performance by caching interfaces.
Kasper Brink <kjbrink at students.cs.uu.nl>**20081124120926
 + added a cache for decoded interfaces to the typechecking state, which
   is preserved across reloads.
 + changed "getInterface" to store and reuse previously decoded interfaces.
] {
hunk ./src/full/Agda/Interaction/GhciTop.hs 187
-	    resetState
+	    preserveDecodedModules resetState
hunk ./src/full/Agda/Interaction/GhciTop.hs 263
-cmd_reset = ioTCM $ do putUndoStack []; resetState
+cmd_reset = ioTCM $ do putUndoStack []; preserveDecodedModules resetState
hunk ./src/full/Agda/Interaction/Imports.hs 122
-    ic <- if uptodate
-	then skip      ifile file
+    (i,t) <- if uptodate
+	then skip x ifile file
hunk ./src/full/Agda/Interaction/Imports.hs 129
-    unless visited $ mergeInterface (fst ic)
+    unless visited $ mergeInterface i
hunk ./src/full/Agda/Interaction/Imports.hs 131
-    return ic
+    storeDecodedModule x i t
+    return (i,t)
hunk ./src/full/Agda/Interaction/Imports.hs 135
-	skip ifile file = do
+	skip x ifile file = do
hunk ./src/full/Agda/Interaction/Imports.hs 137
-	    reportSLn "import.iface" 5 $ "  reading interface file " ++ ifile
-
-	    -- Read interface file
-	    mi <- liftIO $ readInterface ifile
+	    -- Examine the mtime of the interface file. If it is newer than the
+	    -- stored version (in stDecodedModules), or if there is no stored version,
+	    -- read and decode it. Otherwise use the stored version.
+	    t  <- liftIO $ getModificationTime ifile
+	    mm <- getDecodedModule x
+	    mi <- case mm of
+		      Just (im, tm) ->
+			 if tm < t
+			 then do dropDecodedModule x
+				 reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifile
+				 liftIO $ readInterface ifile
+			 else do reportSLn "import.iface" 5 $ "  using stored version of " ++ ifile
+				 return (Just im)
+		      Nothing ->
+			 do reportSLn "import.iface" 5 $ "  no stored version, reading " ++ ifile
+			    liftIO $ readInterface ifile
hunk ./src/full/Agda/Interaction/Imports.hs 161
-		    -- Check time stamp of imported modules
-		    t  <- liftIO $ getModificationTime ifile
-
hunk ./src/full/Agda/TypeChecking/Monad/Base.hs 51
+	 , stDecodedModules    :: DecodedModules
hunk ./src/full/Agda/TypeChecking/Monad/Base.hs 82
+	 , stDecodedModules    = Map.empty
hunk ./src/full/Agda/TypeChecking/Monad/Base.hs 127
+type DecodedModules = Map ModuleName (Interface, ClockTime)
hunk ./src/full/Agda/TypeChecking/Monad/Imports.hs 51
+getDecodedModules :: TCM DecodedModules
+getDecodedModules = gets stDecodedModules
+
+setDecodedModules :: DecodedModules -> TCM ()
+setDecodedModules ms = modify $ \s -> s { stDecodedModules = ms }
+
+preserveDecodedModules :: TCM a -> TCM a
+preserveDecodedModules tcm = do ms <- getDecodedModules
+                                a  <- tcm
+                                setDecodedModules ms
+                                return a
+
+getDecodedModule :: ModuleName -> TCM (Maybe (Interface, ClockTime))
+getDecodedModule x = gets $ Map.lookup x . stDecodedModules
+
+storeDecodedModule :: ModuleName -> Interface -> ClockTime -> TCM ()
+storeDecodedModule x i t = modify $ \s -> s { stDecodedModules = Map.insert x (i,t) $ stDecodedModules s }
+
+dropDecodedModule :: ModuleName -> TCM ()
+dropDecodedModule x = modify $ \s -> s { stDecodedModules = Map.delete x $ stDecodedModules s }
+
}

[Threaded the cached interfaces through "createInterface".
Kasper Brink <kjbrink at students.cs.uu.nl>**20081124123852
 + createInterface performs a separate run of the typechecker; make the
   cached interfaces available there as well.
] {
hunk ./src/full/Agda/Interaction/Imports.hs 180
+	    ds	  <- getDecodedModules
hunk ./src/full/Agda/Interaction/Imports.hs 183
-	    r  <- liftIO $ createInterface opts trace ms vs x file
+	    r  <- liftIO $ createInterface opts trace ms vs ds x file
hunk ./src/full/Agda/Interaction/Imports.hs 188
-		Right (vs, i, isig)  -> do
+		Right (vs, ds, i, isig)  -> do
hunk ./src/full/Agda/Interaction/Imports.hs 197
+		    setDecodedModules ds
hunk ./src/full/Agda/Interaction/Imports.hs 236
-		   ModuleName -> FilePath ->
-		   IO (Either TCErr (VisitedModules, Interface, Signature))
-createInterface opts trace path visited mname file = runTCM $ withImportPath path $ do
+		   DecodedModules -> ModuleName -> FilePath ->
+		   IO (Either TCErr (VisitedModules, DecodedModules, Interface, Signature))
+createInterface opts trace path visited decoded mname file = runTCM $ withImportPath path $ do
hunk ./src/full/Agda/Interaction/Imports.hs 240
+    setDecodedModules decoded
hunk ./src/full/Agda/Interaction/Imports.hs 284
-    return (vs, i, isig)
+    ds   <- getDecodedModules
+    return (vs, ds, i, isig)
}

Context:

[Added mapUndoT.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081122102936] 
[Removed confusing comment.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081111181551] 
[Made the GHC call more robust and enabled GHC optimisations by default.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081118145932
 + Optimisations can be turned off by using --ghc-flag=-O0.
] 
[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] 
[Added _?_ for stream processors.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081110213331] 
[removed dependencies on deleted module Compiler.MAlonzo.Pretty
ulfn at cs.chalmers.se**20081110114614] 
[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] 
[Added bindings for tie (?) and undertie (?).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081027074329] 
[Submitted version of HCAR entry for November 2008.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20081022120350] 
[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)
] 
[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] 
[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.
] 
[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] 
[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] 
[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] 
[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] 
[added failing test case for uncurried metavariables
ulfn at cs.chalmers.se**20080729092148] 
[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] 
[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] 
[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] 
[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] 
[Agda has now been tested with GHC 6.8.3.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080618132825] 
[Fixed comment.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080617143949] 
[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] 
[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] 
[Updated the MAlonzo README in response to a recent patch.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080616150610] 
[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.
] 
[MAlonzo now checks that main has type IO a (issue 82)
ulfn at cs.chalmers.se**20080616145536] 
[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] 
[Made it possible to use forall-style declarations for (co)data parameters.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080610152516] 
[Removed the Agda-aware undo feature from the Emacs mode.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080604124142] 
[fixed bug with metavariables not being expanded in datatype declarations
ulfn at cs.chalmers.se**20080611100554] 
[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] 
[termination-check-ignore-constructor-names
andreas.abel at ifi.lmu.de**20080604130641] 
[added disclaimer to the interactive mode
ulfn at cs.chalmers.se**20080604131348] 
[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] 
[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] 
[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] 
[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).
] 
[fixed bug with productivity checker messing up some termination problems
ulfn at cs.chalmers.se**20080602161850] 
[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] 
[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] 
[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.
] 
[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] 
[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] 
[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] 
[Fixed issue 75 (sometimes hidden arguments cannot be referenced by name).
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150519] 
[Removed possibly incomprehensible remark.
Nils Anders Danielsson <nils.anders.danielsson at gmail.com>**20080523150542] 
[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] 
[TAG AFP08-2
ulfn at cs.chalmers.se**20080520061847] 
[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...
] 
[fixed some bugs
ulfn at cs.chalmers.se**20080520062303] 
[make case now preserves variable names of the original clause
ulfn at cs.chalmers.se**20080519085742] 
[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] 
[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] 
[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] 
[TAG afp08
ulfn at cs.chalmers.se**20080515115143] 
Patch bundle hash:
b3f23f2498418b30f8632b93025c08ad5d02f718
-------------- next part --------------
-- Benchmark.hs -- repeated execution of Agda.Interaction.GhciTop.cmd_load
--
-- Usage:  benchmark num_iterations /full/path/to/source.agda [includedir ...]
--
-- Note:
--   * the default include path for agda libraries can be hardcoded below.
--
--   * it may be necessary to get rid of old .agdai files (issue #111?)

{- compilation flags:
ghc --make Benchmark.hs -main-is Benchmark -o benchmark -fforce-recomp -prof -auto-all
-}

module Benchmark where

import Agda.Interaction.GhciTop
import System
import System.Environment
import System.Posix.Files (touchFile)

-- Default include path for libraries:
defaultincludes :: [ FilePath ]
defaultincludes = [ "."
               -- , "/path/to/agda/lib"
                  ]

--------------------------------------------------------------------------------

main :: IO ()
main = do (n, file, includes) <- getArguments 
          sequence_ . replicate n $ reloadFile file includes

-- In typical usage, the current file will have been modified when reloading:
reloadFile :: FilePath -> [FilePath] -> IO ()
reloadFile file includes = do touchFile file
                              cmd_load file includes

getArguments :: IO (Int, FilePath, [FilePath])
getArguments = do
   args <- getArgs
   case args of
        (num : file : []) -> return (read num, file, defaultincludes)
        (num : file : is) -> return (read num, file, is)
        _                 -> do putStrLn usage
                                exitFailure 

usage :: String
usage = "usage:  benchmark num_iterations /full/path/to/source.agda [includedir ...]"