← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to benchmark/notes

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
benchmark/notes
1
 
 
2
 
20110629: after new level representation and optimised positivity check
3
 
          (used interface file for monad example)
4
 
 
5
 
20110701: actually type checking the monad example
6
 
 
7
 
20110706: (15:00) better precision in ArgsCmp constraints (avoiding rechecking
8
 
          the first arguments)
9
 
 
10
 
20110822: (13:30) switched compareArgs to compareElim (without getting rid of
11
 
          projection arguments). 1 second faster on monad and 1.5 seconds
12
 
          faster on monadpostulate, not sure why.
13
 
 
14
 
20110823: Got rid of projection arguments. Cut the monad examples in half, but
15
 
          no effect on prim which is kind of odd since ... oh we're using a
16
 
          datatype in prim. Changing that to a record and rerunning.
17
 
 
18
 
20110823: (08:00) Sigma record in prim and added all projections instead of
19
 
          just the first three.
20
 
 
21
 
20110825: Allow instantiation of blocked terms, and short-cut instantiation of
22
 
          metas.
23
 
 
24
 
20110830: New computer.
25
 
 
26
 
20110830: (18:00) Added patternmatch test case. Needs abnormal amounts of
27
 
          memory. No idea why.
28
 
 
29
 
20110901: Removed a clause from the patternmatch case. The reason it requires
30
 
          so much memory is coverage checking. It's expected with the current
31
 
          algorithm. It could potentially be improved by separating coverage
32
 
          checking from unreachability checking, but this isn't really a
33
 
          problem in practise. GHC checks both completeness and overlap
34
 
          instantly, so it is possible.
35
 
 
36
 
20110901: (12:30) Set.mapMonotonic instead of Set.map when lowering sets of
37
 
          free variables under a binder.
38
 
 
39
 
20110901: (13:30) New projection benchmarks (record, data and nested) to test
40
 
          eliminator detection for projection-like functions.
41
 
 
42
 
20110902: Implemented projection detection.
43
 
 
44
 
20110906: New state monad implementation (IORef s -> m a)
45
 
 
46
 
20110907: (01:00) Pushing types into constructor applications.
47
 
 
48
 
          (03:00) Treating (\x -> x) as (\(x : _) -> x). Note increase in
49
 
          number of metas.
50
 
 
51
 
          (03:26) Pushing types into lambdas, helps a little, but not as much
52
 
          as we would like: For cwf we had 2794 metas before the (\x -> x)
53
 
          change, 3242 after, and 3038 after this fix.
54
 
 
55
 
          (04:48) Taking better care of types in lambdas. Metas for cwf now
56
 
          down to 2834, so almost what we had before.
57
 
 
58
 
          (05:33) Removed all 'abstract's from the cwf benchmark. Very little
59
 
          difference! 3.1s -> 3.7s and 43MB -> 61MB.
60
 
 
61
 
20110908: Fixed issues 311, 450 and 451.
62
 
 
63
 
20110909: Minor improvement of FreeVars.singleton and added
64
 
          Data.List.Any.Properties as a benchmark.
65
 
 
66
 
20110910: Can't remember.
67
 
 
68
 
20110915: (07.38) New constraint handling machinery.
69
 
          (08.47) No more quadratic nubbing in localNames
70
 
          (09.14) Don't reduce sorts when reducing types
71
 
          (13.11) Got rid of most MonadTCMs
72
 
 
73
 
20110919: Positivity checker needs to look at pattern matching.
74
 
 
75
 
20110922: Just minor stuff.
76
 
 
77
 
20110924: (09.49) New mutual syntax.
78
 
          (10.04) Avoid generating sort metas when checking isType_ of a Fun or a Pi
79
 
          (     ) Same for isType_ of Set or Set a
80
 
 
81
 
20120406: Qualified mixfix operators
82
 
 
83
 
20120702: Pre-sharing
84
 
20120705: Sharing is working but under-utilized
85
 
20121005: (18.37) With sharing
86
 
          (20.31) Without sharing