Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The great crusade against TCM #3589

Merged
merged 78 commits into from May 7, 2019

Conversation

@jespercockx
Copy link
Member

jespercockx commented Feb 25, 2019

The goal of this PR is to make many functions in the Agda codebase effect-polymorphic by generalizing their types from TCM to an arbitrary monad m satisfying some constraints. In particular, it includes generalized types for the entire pretty-printing pipeline (internal -> abstract and abstract -> concrete), as well as for the conversion checker (i.e. equalTerms, equalTypes, ...) and the internal double-checker (checkInternal). As in the real crusades, I had to pillage many other places throughout the Agda codebase before I got to my final destination.

My main motivation for this refactoring is because I need to call the conversion checker from places where we currently can't, in particular the ReduceM monad (see issues #1433, #2732, #3510, #3525). But there are also other reasons why it is a good idea to write monadic code in this style:

  • It statically rules out whole classes of bugs: the types are explicit in which functions can read and/or modify (specific parts of) the typechecking state, throw exceptions and/or warnings, ...
  • Having a 'pure' implementation of the CheckInternal module allows us to have a separate typechecker for 'core Agda' that is statically guaranteed to not instantiate any metas or create any constraints.
  • The constraints on the monad document which effects are actually used by each function. I actually found several lies in the comments (e.g. "Here we use TCM only for the purpose of generating fresh names" when actually it was used for many more things).
  • Writing functions against an interface instead of in a specific monad such as TCM reduces the coupling of the codebase because not everything has to rely on TypeChecking.Monad.Base.

List of new type classes

  • MonadConstraint: creating, solving and modifying constraints
  • MonadMetaSolver: creating, instantiating, and modifying metavariables
  • MonadAddContext: (locally) adding things to the context with fresh names
  • MonadInteractionPoints: creating new interaction points (for the emacs mode)
  • MonadFresh: generating fresh things (parametrized by the type of the thing)
  • MonadStatistics: write access to the statistics (for profiling)

TODO:

  • Fix a mysterious internal error that pops up during debug printing
  • Benchmarking to make sure this doesn't significantly slow down typechecking
  • More things probably
Copy link
Contributor

andreasabel left a comment

Great job, Jesper!

src/full/Agda/Syntax/Scope/Monad.hs Outdated Show resolved Hide resolved
src/full/Agda/TypeChecking/MetaVars.hs Show resolved Hide resolved
@jespercockx jespercockx force-pushed the jespercockx:MonadConversion branch from 4af6ba7 to 39bd3c7 Feb 26, 2019
@jespercockx

This comment was marked as outdated.

Copy link
Member Author

jespercockx commented Feb 26, 2019

Well that rebase went spectacularly wrong and messed up the whole PR. Not sure what I did wrong...

Edit: it's fixed now.

@jespercockx jespercockx force-pushed the jespercockx:MonadConversion branch 2 times, most recently from 142d01b to 86120bd Feb 26, 2019
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 27, 2019

Here are the results from running make library-test on Agda both before and after this PR. There is a moderate slowdown in overall typechecking (about 9%). The difference is spread kind of evenly between typing, serialization, and parsing, so I'm not sure what to make of it. Any Haskell experts can help with finding out how to avoid this slowdown?

Vanilla Agda @ 12941e5

Total                        366,311ms            
Miscellaneous                  3,466ms            
Typing                        46,635ms (171,618ms)
Typing.CheckLHS               24,390ms  (42,088ms)
Typing.CheckLHS.UnifyIndices  17,698ms            
Typing.CheckRHS               37,720ms            
Typing.TypeSig                25,515ms            
Typing.OccursCheck            13,882ms            
Typing.With                    5,776ms            
Serialization                 84,296ms (116,172ms)
Serialization.BinaryEncode    25,990ms            
Serialization.Compress         2,349ms            
Serialization.BuildInterface   2,243ms            
Serialization.Sort             1,294ms            
Parsing                        1,359ms  (17,831ms)
Parsing.OperatorsExpr         13,761ms            
Parsing.OperatorsPattern       2,710ms            
Scoping                       13,103ms  (16,210ms)
Scoping.InverseScopeLookup     3,106ms            
Termination                    7,654ms  (11,518ms)
Termination.Compare            1,937ms            
Termination.RecCheck           1,414ms            
Termination.Graph                511ms            
Highlighting                  10,994ms            
Positivity                     6,833ms            
Coverage                       4,960ms            
Injectivity                    2,916ms            
DeadCode                       2,760ms            
Import                           548ms            
Deserialization                  324ms            
ProjectionLikeness               143ms            
ModuleName                        10ms            

 371,939,415,384 bytes allocated in the heap
  44,886,106,256 bytes copied during GC
   1,167,892,464 bytes maximum residency (68 sample(s))
      18,609,776 bytes maximum slop
            1564 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     190263 colls,     0 par   56.842s  56.859s     0.0003s    0.1564s
  Gen  1        68 colls,     0 par   95.823s  96.050s     1.4125s    3.9330s

  INIT    time    0.000s  (  0.001s elapsed)
  MUT     time  213.649s  (213.830s elapsed)
  GC      time  152.665s  (152.910s elapsed)
  EXIT    time    0.453s  (  0.453s elapsed)
  Total   time  366.768s  (367.194s elapsed)

  %GC     time      41.6%  (41.6% elapsed)

  Alloc rate    1,740,893,595 bytes per MUT second

  Productivity  58.4% of total user, 58.4% of total elapsed


real	6m7,253s
user	6m2,661s
sys	0m4,159s

Modified Agda @ 86120bd

Total                        397,934ms            
Miscellaneous                  3,189ms            
Typing                        46,711ms (185,510ms)
Typing.CheckRHS               56,975ms            
Typing.TypeSig                32,683ms            
Typing.CheckLHS               15,630ms  (29,258ms)
Typing.CheckLHS.UnifyIndices  13,627ms            
Typing.With                   10,002ms            
Typing.OccursCheck             9,878ms            
Serialization                 83,236ms (127,857ms)
Serialization.BinaryEncode    25,525ms            
Serialization.Sort            11,604ms            
Serialization.BuildInterface   5,589ms            
Serialization.Compress         1,901ms            
Parsing                        1,468ms  (20,474ms)
Parsing.OperatorsExpr         15,830ms            
Parsing.OperatorsPattern       3,175ms            
Scoping                       12,927ms  (15,985ms)
Scoping.InverseScopeLookup     3,057ms            
Highlighting                  12,133ms            
Termination                    7,316ms  (11,320ms)
Termination.Compare            2,190ms            
Termination.RecCheck           1,369ms            
Termination.Graph                444ms            
Positivity                     9,422ms            
DeadCode                       4,563ms            
Coverage                       4,232ms            
Injectivity                    1,891ms            
Import                           861ms            
Deserialization                  317ms            
ProjectionLikeness               159ms            
ModuleName                        13ms            

 364,690,160,784 bytes allocated in the heap
  45,661,676,640 bytes copied during GC
   1,139,596,288 bytes maximum residency (67 sample(s))
      13,153,800 bytes maximum slop
            1588 MB total memory in use (23 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     209504 colls,     0 par   61.744s  61.746s     0.0003s    0.1701s
  Gen  1        67 colls,     0 par   105.829s  105.834s     1.5796s    3.6685s

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time  230.362s  (230.449s elapsed)
  GC      time  167.573s  (167.580s elapsed)
  EXIT    time    0.393s  (  0.393s elapsed)
  Total   time  398.329s  (398.422s elapsed)

  %GC     time      42.1%  (42.1% elapsed)

  Alloc rate    1,583,117,764 bytes per MUT second

  Productivity  57.9% of total user, 57.9% of total elapsed


real	6m38,475s
user	6m35,613s
sys	0m2,768s
@UlfNorell

This comment has been minimized.

Copy link
Member

UlfNorell commented Feb 27, 2019

My guess is that the problem is carrying along monad dictionaries everywhere, where before you where running in TCM which is just a thin layer on top of IO.

Try adding a SPECIALIZE pragma to every single function you overloaded (although I don't think I've ever managed to get any performance out of one of those).

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 27, 2019

So I am experimenting a bit and recompiled Agda with the ghc options -fspecialise-aggressively and -fexpose-all-unfoldings (see the Haskell wiki) and this results in a ~10% speedup compared to vanilla Agda. So it seems there is definitely something to be gained from specializing functions.

Now I don't know if turning on these flags by default is a good idea or if there are some negatives (e.g. slower compilation speed, larger binaries, ...). At least one person on reddit who recommends against them. But at least it seems better than manually adding all the {-# SPECIALIZE #-} pragmas to hundreds of functions.

Total                        328,386ms            
Miscellaneous                  2,967ms            
Typing                        37,137ms (144,361ms)
Typing.CheckRHS               45,014ms            
Typing.CheckLHS               12,343ms  (25,510ms)
Typing.CheckLHS.UnifyIndices  13,166ms            
Typing.TypeSig                21,542ms            
Typing.With                    8,096ms            
Typing.OccursCheck             7,060ms            
Serialization                 82,350ms (108,008ms)
Serialization.BinaryEncode    16,343ms            
Serialization.Sort             5,109ms            
Serialization.BuildInterface   2,305ms            
Serialization.Compress         1,899ms            
Parsing                        1,720ms  (23,007ms)
Parsing.OperatorsExpr         18,196ms            
Parsing.OperatorsPattern       3,091ms            
Highlighting                  12,455ms            
Termination                    8,188ms  (11,312ms)
Termination.Compare            1,687ms            
Termination.RecCheck           1,001ms            
Termination.Graph                435ms            
Scoping                        7,490ms   (9,912ms)
Scoping.InverseScopeLookup     2,422ms            
Positivity                     5,852ms            
Coverage                       3,418ms            
Injectivity                    3,258ms            
DeadCode                       2,355ms            
Import                         1,002ms            
Deserialization                  342ms            
ProjectionLikeness               115ms            
ModuleName                        13ms            

 296,945,020,200 bytes allocated in the heap
  41,047,316,304 bytes copied during GC
   1,114,645,320 bytes maximum residency (58 sample(s))
      15,183,864 bytes maximum slop
            1564 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     169202 colls,     0 par   56.060s  56.078s     0.0003s    0.2002s
  Gen  1        58 colls,     0 par   86.639s  86.661s     1.4942s    3.7668s

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time  185.688s  (186.043s elapsed)
  GC      time  142.699s  (142.740s elapsed)
  EXIT    time    0.415s  (  0.415s elapsed)
  Total   time  328.804s  (329.198s elapsed)

  %GC     time      43.4%  (43.4% elapsed)

  Alloc rate    1,599,157,292 bytes per MUT second

  Productivity  56.6% of total user, 56.6% of total elapsed


real	5m29,272s
user	5m25,953s
sys	0m2,923s
@WolframKahl

This comment has been minimized.

Copy link
Member

WolframKahl commented Feb 27, 2019

I recommend to re-run these timings with:

+RTS -H4G -M4G -A128M -RTS

This should drastically reduce the percentage of time spent on garbage collection.

(I only call Agda with such settings, with sizes depending on machine and application.)

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 27, 2019

Sure, I can do that. However, if these settings are better than the default ones then I wonder why they are not used by default when running make library-test. Maybe we should update the Makefile instead?

@WolframKahl

This comment has been minimized.

Copy link
Member

WolframKahl commented Feb 28, 2019

(If somebody tries this on a machine with only 2GB of RAM, they will want to use something in the rough direction of

+RTS -H0.6G -M1.2G -A64M -RTS

instead...)

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 28, 2019

Here are the timings with better heap settings as suggested by @WolframKahl. We get a speedup of almost 20% now compared to unmodified Agda! I will also run the test on unmodified Agda with the ghc flags, but I need to recompile first.

Unmodified Agda, better heap settings

Total                        292,340ms            
Miscellaneous                  2,345ms            
Typing                        31,037ms (157,453ms)
Typing.CheckLHS               21,089ms  (41,336ms)
Typing.CheckLHS.UnifyIndices  20,247ms            
Typing.CheckRHS               41,040ms            
Typing.TypeSig                28,414ms            
Typing.OccursCheck             8,543ms            
Typing.With                    7,081ms            
Serialization                 35,192ms  (53,938ms)
Serialization.BinaryEncode    12,933ms            
Serialization.BuildInterface   2,122ms            
Serialization.Compress         2,003ms            
Serialization.Sort             1,686ms            
Parsing                        1,473ms  (18,907ms)
Parsing.OperatorsExpr         14,072ms            
Parsing.OperatorsPattern       3,362ms            
Termination                   10,696ms  (15,450ms)
Termination.Compare            2,636ms            
Termination.RecCheck           1,523ms            
Termination.Graph                594ms            
Scoping                        9,604ms  (13,152ms)
Scoping.InverseScopeLookup     3,548ms            
Highlighting                  10,735ms            
Positivity                     7,818ms            
Coverage                       5,467ms            
DeadCode                       3,116ms            
Injectivity                    2,835ms            
Import                           605ms            
Deserialization                  364ms            
ProjectionLikeness               134ms            
ModuleName                        12ms            

 372,075,275,960 bytes allocated in the heap
  10,048,580,296 bytes copied during GC
   1,029,621,096 bytes maximum residency (10 sample(s))
       6,458,536 bytes maximum slop
            4329 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       104 colls,     0 par   12.596s  12.604s     0.1212s    0.2901s
  Gen  1        10 colls,     0 par    5.529s   5.534s     0.5534s    1.9817s

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time  274.216s  (274.669s elapsed)
  GC      time   18.125s  ( 18.138s elapsed)
  EXIT    time    0.071s  (  0.071s elapsed)
  Total   time  292.416s  (292.879s elapsed)

  %GC     time       6.2%  (6.2% elapsed)

  Alloc rate    1,356,869,802 bytes per MUT second

  Productivity  93.8% of total user, 93.8% of total elapsed


real	4m53,028s
user	4m49,012s
sys	0m3,550s

Patched Agda with -fexpose-all-unfoldings & -fspecialise-aggressively, better heap settings

Total                        236,322ms            
Miscellaneous                  2,698ms            
Typing                        28,787ms (117,998ms)
Typing.CheckRHS               31,951ms            
Typing.CheckLHS               14,744ms  (26,785ms)
Typing.CheckLHS.UnifyIndices  12,041ms            
Typing.TypeSig                19,266ms            
Typing.OccursCheck             6,735ms            
Typing.With                    4,473ms            
Serialization                 32,089ms  (50,273ms)
Serialization.BinaryEncode    12,797ms            
Serialization.Compress         2,021ms            
Serialization.BuildInterface   1,739ms            
Serialization.Sort             1,624ms            
Parsing                        1,597ms  (19,264ms)
Parsing.OperatorsExpr         14,345ms            
Parsing.OperatorsPattern       3,321ms            
Scoping                        9,262ms  (11,769ms)
Scoping.InverseScopeLookup     2,506ms            
Highlighting                  10,918ms            
Termination                    6,004ms   (8,960ms)
Termination.Compare            1,566ms            
Termination.RecCheck             984ms            
Termination.Graph                405ms            
Positivity                     5,526ms            
Coverage                       3,455ms            
DeadCode                       2,205ms            
Injectivity                    2,110ms            
Import                           623ms            
Deserialization                  393ms            
ProjectionLikeness               110ms            
ModuleName                        13ms            

 296,982,072,448 bytes allocated in the heap
   8,523,243,688 bytes copied during GC
     872,961,472 bytes maximum residency (9 sample(s))
       5,618,216 bytes maximum slop
            4375 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0        81 colls,     0 par   11.896s  11.906s     0.1470s    0.5880s
  Gen  1         9 colls,     0 par    4.785s   4.799s     0.5333s    1.8008s

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time  219.642s  (220.221s elapsed)
  GC      time   16.681s  ( 16.705s elapsed)
  EXIT    time    0.080s  (  0.080s elapsed)
  Total   time  236.406s  (237.007s elapsed)

  %GC     time       7.1%  (7.0% elapsed)

  Alloc rate    1,352,117,091 bytes per MUT second

  Productivity  92.9% of total user, 93.0% of total elapsed


real	3m57,177s
user	3m52,876s
sys	0m3,698s
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 28, 2019

I want to note that the optimized settings suggested by @WolframKahl really do matter a lot (in the order of 30% speedup on the standard library)! Since I suspect there are not many people running Agda on 2GB of memory but there are many people that have no idea how to tweak these settings yet would benefit greatly from it, I suggest we change the default to something closer to what Wolfram suggests.

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 28, 2019

Here are the results for Agda before this PR but with the two flags set. Surprisingly, we see only some speedup but not to the same degree I observe for Agda after the PR. Maybe having more general types actually helps ghc with aggressive specialization enabled? I've rerun the tests a few times and I get a variation of <10s between runs, so there is actually some observable difference.

Total                        259,878ms            
Miscellaneous                  2,183ms            
Typing                        27,837ms (139,272ms)
Typing.CheckRHS               36,582ms            
Typing.CheckLHS               18,437ms  (36,332ms)
Typing.CheckLHS.UnifyIndices  17,895ms            
Typing.TypeSig                25,323ms            
Typing.OccursCheck             7,560ms            
Typing.With                    5,634ms            
Serialization                 31,680ms  (49,346ms)
Serialization.BinaryEncode    12,047ms            
Serialization.BuildInterface   2,081ms            
Serialization.Compress         1,958ms            
Serialization.Sort             1,578ms            
Parsing                        1,350ms  (16,961ms)
Parsing.OperatorsExpr         12,434ms            
Parsing.OperatorsPattern       3,176ms            
Scoping                        8,966ms  (12,230ms)
Scoping.InverseScopeLookup     3,263ms            
Termination                    8,092ms  (12,008ms)
Termination.Compare            2,018ms            
Termination.RecCheck           1,446ms            
Termination.Graph                451ms            
Highlighting                   9,792ms            
Positivity                     6,798ms            
Coverage                       4,908ms            
DeadCode                       2,854ms            
Injectivity                    2,528ms            
Import                           524ms            
Deserialization                  328ms            
ProjectionLikeness               126ms            
ModuleName                        11ms            

 372,073,355,104 bytes allocated in the heap
  10,051,369,912 bytes copied during GC
   1,029,632,832 bytes maximum residency (10 sample(s))
       6,400,456 bytes maximum slop
            4329 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       104 colls,     0 par   11.698s  11.700s     0.1125s    0.2705s
  Gen  1        10 colls,     0 par    4.755s   4.755s     0.4755s    1.2909s

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time  243.426s  (243.509s elapsed)
  GC      time   16.453s  ( 16.454s elapsed)
  EXIT    time    0.070s  (  0.070s elapsed)
  Total   time  259.951s  (260.034s elapsed)

  %GC     time       6.3%  (6.3% elapsed)

  Alloc rate    1,528,483,712 bytes per MUT second

  Productivity  93.7% of total user, 93.7% of total elapsed


real	4m20,183s
user	4m16,822s
sys	0m3,276s
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 28, 2019

Here's the effect on compilation speed:

  • Running make clean && time make install-bin with no extra options:
real	11m36,700s
user	11m22,402s
sys	0m13,785s
  • Running make clean && time make install-bin with the two ghc flags -fspecialise-aggressively and -fexpose-all-unfoldings
real	16m17,882s
user	15m56,353s
sys	0m18,595s

So there is a real effect on compilation speeds. The question is if this a price we are willing to pay.

@UlfNorell

This comment has been minimized.

Copy link
Member

UlfNorell commented Feb 28, 2019

I would say yes. You could always disable them (and optimisation in general) locally when doing things that benefit from a quicker turn-around.

@asr

This comment has been minimized.

Copy link
Member

asr commented Feb 28, 2019

@jespercockx, just out curiosity, what GHC version are you using on your tests?

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 28, 2019

8.0.2, which is the default version in current LTS ubuntu repositories

@nad

This comment has been minimized.

Copy link
Contributor

nad commented Feb 28, 2019

I suggest that you rerun the tests using the latest released version of GHC (8.6.3). I think compilation times and the effects of optimisations can vary quite a bit from version to version.

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Feb 28, 2019

I'd rather not mess around with different versions of GHC on my pc and I don't want to move to a newer version as long as we still support the old one. Maybe someone else who already has the newest GHC could rerun the tests?

@nad

This comment has been minimized.

Copy link
Contributor

nad commented Mar 1, 2019

I have tried make clean && time make install-bin twice now, using GHC 8.6.3, but both builds failed (with different error messages):

[314 of 356] Compiling Agda.TypeChecking.Coverage ( src/full/Agda/TypeChecking/Coverage.hs, dist-2.6.0/build/Agda/TypeChecking/Coverage.o )

<no location info>: error:
    expectJust cpeBody:collect_args
CallStack (from HasCallStack):
  error, called at compiler/utils/Maybes.hs:55:27 in ghc:Maybes
  expectJust, called at compiler/coreSyn/CorePrep.hs:930:32 in ghc:CorePrep
[350 of 356] Compiling Agda.Interaction.InteractionTop ( src/full/Agda/Interaction/InteractionTop.hs, dist-2.6.0/build/Agda/Interaction/InteractionTop.o )

<no location info>: error:
    ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.3 for i386-unknown-linux):
        tyThingTyCon
  Identifier ‘$tcCPasswd2’
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/main/HscTypes.hs:2165:28 in ghc:HscTypes

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

This is using commit 39b4729. I have not turned on -fspecialise-aggressively or -fexpose-all-unfoldings. The nondeterministic error messages might be explained by the fact that I give the option -j3 to GHC.

Has anyone else encountered problems of this kind? Travis built this commit successfully using GHC 8.6.3.

@asr

This comment has been minimized.

Copy link
Member

asr commented Mar 1, 2019

Using GHC 8.6.3, I couldn't reproduce the problem running

$ make clean && make install-bin CABAL_OPTS='--ghc-option=-j3'
@nad

This comment has been minimized.

Copy link
Contributor

nad commented Mar 1, 2019

My next compilation was successful…

@jespercockx jespercockx force-pushed the jespercockx:MonadConversion branch from dcda8ff to fdbd035 Mar 16, 2019
@jespercockx jespercockx force-pushed the jespercockx:MonadConversion branch 3 times, most recently from 64a985d to 23a4e05 Apr 18, 2019
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented Apr 18, 2019

I brought this PR up-to-date with the latest master, I'm hoping I can merge it soon to avoid having to continue doing this. There are still two problems in test/interaction that need to be solved but I'm stuck on, however:

  • The test case for #1829 runs out of memory, I need to increase the heap from 4MB to ~50MB to make the error go away. @Saizan this could have something to do with caching, do you know what you did to fix the original issue (I only see you added many bangs)?
  • The test case for #2076 runs into an internal error at src/full/Agda/Syntax/Scope/Base.hs:997. @UlfNorell I remember we looked at this on the flight back from Tokyo but I don't remember if we found a solution :(
@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 3, 2019

Maybe try some combination of: --interleaved-output and --cabal-verbose to line 298-ish in .travis.yml?

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 3, 2019

@jespercockx jespercockx force-pushed the jespercockx:MonadConversion branch from 73ec2f9 to 8f5b270 May 3, 2019
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 3, 2019

I tried your suggestion, but it doesn't seem to work b/c Travis only prints all the output after the command completes. However, I found that travis_wait takes an optional extra argument for the timeout (default is 20 minutes). I now increased it to 30 minutes to see if that helps.

@asr

This comment has been minimized.

Copy link
Member

asr commented May 4, 2019

It doesn't seem a timeout error. We run two tests with stack. In the second test, we test the Agda flags including the use of the cpphs preprocessor. In this test, Travis is showing the following error:

/home/travis/build/agda/agda/src/full/Agda/TypeChecking/Primitive.hs:1882:4: error:
    parse error (possibly incorrect indentation or mismatched brackets)
     |
1882 |    isOne = fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIsOne
     |    ^

The error doesn't show up with Cabal because we don't test the cpphs preprocessor with Cabal.

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 4, 2019

Well, at least there's no more timeout now that I increased it to 30 minutes. The parse error here seems super weird to me as this is not a part of the code I touched in this PR. Can someone else explain what's going on?

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 4, 2019

BTW, the other builds using stack give different but similar errors:

On 8.6:

/home/travis/build/agda/agda/src/full/Agda/TypeChecking/Primitive.hs:1882:4: error:
    parse error (possibly incorrect indentation or mismatched brackets)
     |
1882 |    isOne = fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIsOne
     |    ^

On 8.4 and 8.2:

/home/travis/build/agda/agda/src/full/Agda/TypeChecking/Primitive.hs:1880:47: error:
        parse error on input ‘\’
         |
    1880 |    toFinitePi _               = __IMPOSSIBLE__\
         |                                               ^

On 8.0:

 /home/travis/build/agda/agda/src/full/Agda/TypeChecking/Primitive.hs:1880:47: error:
        parse error on input ‘\’
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 4, 2019

Trying again after fixing a weird typo...

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 4, 2019

Travis is still not happy, this time there's a problem in the compiler test:

======================================================================
========================== Compiler tests ============================
======================================================================
all
  LaTeXAndHTML
piler
    MAlonzo
      simple
        Arith:                 pareNat:            pileAsPattern:      pileCatchAll:       pileNumbers:        piledRecord:        pilingCoinduction:  pilingQNamePats:    Sized:  DISABLED (0.00s)
        ErasureSubtyping:      ashing:      DISABLED (0.00s)
        Issue2664:             Seq:               eOrder:            DISABLED (0.00s)
        Sort:                  bda:   plicits:     orphicIO: ents:       DISABLED (0.00s)
        VecReverseIrr:                 AllStdLib:                     ExportTestAgda:              simple
        Arith:                 pareNat:            pileAsPattern:      FAIL (0.89s)
                               Result did not match golden value.
                               Diff between actual and golden value:
========================================
agda-tests: Call to `git diff` failed: (ExitFailure 1,"diff --git a/tmp/CompileAsPattern4333-0.golden b/tmp/CompileAsPattern4333-1.actual\nindex 105a09d..8736cec 100644\n--- a/tmp/CompileAsPattern4333-0.golden\n+++ b/tmp/CompileAsPattern4333-1.actual\n@@ -16,8 +16,7 @@ out >               (Agda.Builtin.List.List._\8759_ f (CompileAsPattern._.merge _\n out > CompileAsPattern.mapM! =\n out >   \955 _ a b \8594\n out >     case b of\n-out >       Agda.Builtin.List.List.[] \8594\n-out >         Common.IO.return () _ Agda.Builtin.Unit.\8868.tt\n+out >       Agda.Builtin.List.List.[] \8594 Common.IO.return () _ _\n out >       Agda.Builtin.List.List._\8759_ c d \8594\n out >         Common.IO._>>=_\n out >           () () _ _ (a c) (\955 _ \8594 CompileAsPattern.mapM! _ a d)\n","")
CallStack (from HasCallStack):
  error, called at ./Test/Tasty/Silver/Interactive.hs:187:16 in tasty-silver-3.1.12-BQTaQu15xJWFFSz4RfixLJ:Test.Tasty.Silver.Interactive
make: *** [compiler-test] Error 1
The command "if [[ $TEST = "MAIN" ]]; then make AGDA_TESTS_OPTIONS="-j${PARALLEL_TESTS} --hide-successes" BUILD_DIR=$BUILD_DIR compiler-test; fi" exited with 2.
62.29s$ if [[ $TEST = "MAIN" ]]; then make AGDA_TESTS_OPTIONS="-j${PARALLEL_TESTS} --hide-successes" BUILD_DIR=$BUILD_DIR lib-succeed; fi

This is especially weird since this happens in the cabal tests which previously passed fine. sigh

@asr

This comment has been minimized.

Copy link
Member

asr commented May 4, 2019

This is especially weird since this happens in the cabal tests which previously passed fine.

You are testing your PR on a newer master. The above error is also present in the current master.

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 4, 2019

Yep, that build error is already in master and is breaking the other PRs as well.
If it helps, the error's golden v. expected diff output, prettied with gsed 's/\\n/\n/g' looks like:

agda-tests: Call to `git diff` failed: (ExitFailure 1,"diff --git a/tmp/CompileAsPattern4333-0.golden b/tmp/CompileAsPattern4333-1.actual
index 105a09d..8736cec 100644
--- a/tmp/CompileAsPattern4333-0.golden
+++ b/tmp/CompileAsPattern4333-1.actual
@@ -16,8 +16,7 @@ out >               (Agda.Builtin.List.List._\8759_ f (CompileAsPattern._.merge _
 out > CompileAsPattern.mapM! =
 out >   \955 _ a b \8594
 out >     case b of
-out >       Agda.Builtin.List.List.[] \8594
-out >         Common.IO.return () _ Agda.Builtin.Unit.\8868.tt
+out >       Agda.Builtin.List.List.[] \8594 Common.IO.return () _ _
 out >       Agda.Builtin.List.List._\8759_ c d \8594
 out >         Common.IO._>>=_
 out >           () () _ _ (a c) (\955 _ \8594 CompileAsPattern.mapM! _ a d)
","")

Possibly Definitely related to 53de225

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 4, 2019

@jespercockx Just so it doesn't stay a mystery, regarding that typo: __IMPOSSIBLE__ is no longer a macro, so it's likely that before, the C preprocessor was eating the backslash (as a newline continuation) after macro expansion, and no longer does. The cabal v. stack difference is possibly due to one using gcc and the other using cpphs like @asr suggested.

@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 6, 2019

Thanks @erydo for the explanation. Since the error doesn't have anything to do with this PR and all problems here seem to be fixed, should I go ahead and merge this PR? Or should I wait until the build on master is fixed and we get a definite green mark from Travis on this PR?

@andreasabel

This comment has been minimized.

Copy link
Contributor

andreasabel commented May 6, 2019

@erydo : I commented on the broken travis here: #3732 (comment) ; let us continue the discussion there.

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 6, 2019

@jespercockx — My advice would be to not push or merge changes (except fixes) to master until it's building cleanly. Otherwise it becomes harder to troubleshoot the causes of build failures.

Though, I do want to see this PR merged in quickly!

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 7, 2019

Now that master seems to be building again, I've triggered a rebuild on Travis. Fingers crossed!

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 7, 2019

@agda/developers — CI passed! Any objection to merging this in now?

@@ -1,4 +1,5 @@
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE CPP #-}

This comment has been minimized.

Copy link
@erydo

erydo May 7, 2019

Contributor

This should not add the CPP pragma here. But should probably be fixed in subsequent PR.

@erydo

This comment has been minimized.

Copy link
Contributor

erydo commented May 7, 2019

Given how long this PR has been in progress, and that no one had before asked for this to be delayed, I'm going to take a leap of faith and merge it in. Please yell at me if I was not supposed to do that.

@erydo erydo merged commit adcd57d into agda:master May 7, 2019
1 check passed
1 check passed
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@jespercockx

This comment has been minimized.

Copy link
Member Author

jespercockx commented May 8, 2019

I'm very happy this finally got merged :)

@nad

This comment has been minimized.

Copy link
Contributor

nad commented May 9, 2019

Compilation times on my seven year old laptop, using GHC 8.6.5 with -j3, for adcd57d:

  • Without the optimisations:
    real    15m1,526s
    user    23m32,134s
    sys     5m38,682s
    
  • With the optimisations:
    real    22m55,709s
    user    35m4,065s
    sys     8m47,846s
    

For make library-test (with the default RTS settings, i.e. -H1G -M1.5G) I get the following results:

  • Without optimisations:
    Total                        267,646ms
    Miscellaneous                  4,656ms
    Typing                        28,461ms (136,235ms)
    Typing.CheckRHS               43,088ms
    Typing.TypeSig                25,408ms
    Typing.CheckLHS               13,575ms  (24,605ms)
    Typing.CheckLHS.UnifyIndices  11,030ms
    Typing.OccursCheck             8,254ms
    Typing.With                    6,416ms
    Serialization                 47,493ms  (70,416ms)
    Serialization.BinaryEncode    16,895ms
    Serialization.Compress         2,687ms
    Serialization.BuildInterface   2,643ms
    Serialization.Sort               696ms
    Parsing                        1,383ms  (15,222ms)
    Parsing.OperatorsExpr         11,150ms
    Parsing.OperatorsPattern       2,688ms
    Highlighting                  11,367ms
    Scoping                        6,960ms   (9,650ms)
    Scoping.InverseScopeLookup     2,689ms
    Positivity                     5,990ms
    Termination                    1,767ms   (4,124ms)
    Termination.Compare            1,293ms
    Termination.RecCheck             790ms
    Termination.Graph                273ms
    Coverage                       3,336ms
    DeadCode                       2,389ms
    Import                         2,353ms
    Injectivity                    1,477ms
    Deserialization                  284ms
    ProjectionLikeness               128ms
    ModuleName                        12ms
    
       2,327,593,132 bytes allocated in the heap
      13,978,823,916 bytes copied during GC
         553,705,972 bytes maximum residency (29 sample(s))
           2,412,044 bytes maximum slop
                 528 MB total memory in use (0 MB lost due to fragmentation)
    
                                         Tot time (elapsed)  Avg pause  Max pause
      Gen  0      1852 colls,     0 par   31.784s  31.937s     0.0172s    0.2318s
      Gen  1        29 colls,     0 par   18.950s  19.074s     0.6577s    4.6357s
    
      INIT    time    0.000s  (  0.000s elapsed)
      MUT     time  214.392s  (218.419s elapsed)
      GC      time   50.734s  ( 51.011s elapsed)
      EXIT    time    0.000s  (  0.000s elapsed)
      Total   time  265.126s  (269.430s elapsed)
    
      %GC     time       0.0%  (0.0% elapsed)
    
      Alloc rate    10,856,728 bytes per MUT second
    
      Productivity  80.9% of total user, 81.1% of total elapsed
    
    
    real    4m29,486s
    user    4m25,128s
    sys     0m3,021s
    
  • With optimisations:
    Total                        223,952ms
    Miscellaneous                  4,788ms
    Typing                        22,858ms (103,447ms)
    Typing.CheckRHS               28,374ms
    Typing.CheckLHS               11,069ms  (20,531ms)
    Typing.CheckLHS.UnifyIndices   9,461ms
    Typing.TypeSig                19,491ms
    Typing.OccursCheck             6,750ms
    Typing.With                    5,441ms
    Serialization                 46,682ms  (66,003ms)
    Serialization.BinaryEncode    12,855ms
    Serialization.Compress         3,142ms
    Serialization.BuildInterface   2,663ms            
    Serialization.Sort               660ms            
    Parsing                        1,249ms  (13,882ms)
    Parsing.OperatorsExpr          9,980ms            
    Parsing.OperatorsPattern       2,652ms            
    Highlighting                  10,886ms            
    Scoping                        5,428ms   (8,488ms)
    Scoping.InverseScopeLookup     3,060ms            
    Positivity                     4,995ms            
    Termination                    1,439ms   (3,091ms)
    Termination.Compare            1,013ms            
    Termination.RecCheck             489ms            
    Termination.Graph                149ms            
    Coverage                       2,916ms            
    DeadCode                       2,536ms            
    Import                         1,352ms            
    Injectivity                    1,168ms            
    Deserialization                  280ms            
    ProjectionLikeness               101ms            
    ModuleName                        11ms            
    
       3,805,222,776 bytes allocated in the heap
      13,568,998,588 bytes copied during GC
         528,303,532 bytes maximum residency (28 sample(s))
           2,169,428 bytes maximum slop
                 503 MB total memory in use (1 MB lost due to fragmentation)
    
                                         Tot time (elapsed)  Avg pause  Max pause
      Gen  0      1793 colls,     0 par   30.749s  30.906s     0.0172s    0.2605s
      Gen  1        28 colls,     0 par   13.804s  13.922s     0.4972s    1.6573s
    
      INIT    time    0.000s  (  0.000s elapsed)
      MUT     time  177.283s  (180.569s elapsed)
      GC      time   44.553s  ( 44.828s elapsed)
      EXIT    time    0.000s  (  0.000s elapsed)
      Total   time  221.836s  (225.397s elapsed)
    
      %GC     time       0.0%  (0.0% elapsed)
    
      Alloc rate    21,464,157 bytes per MUT second
    
      Productivity  79.9% of total user, 80.1% of total elapsed
    
    
    real    3m45,448s
    user    3m41,837s
    sys     0m2,794s
    

My build times are considerably longer than @jespercockx's, but the library test completes more quickly. I think @jespercockx has newer, more performant hardware, but I'm using a newer version of GHC and (unlike @jespercockx) a 32-bit kernel. (And we haven't tested exactly the same version of Agda, and perhaps not exactly the same version of the standard library.) An apples-to-apples comparison where only one variable at a time is tweaked might be interesting.

@jespercockx jespercockx deleted the jespercockx:MonadConversion branch May 21, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
8 participants
You can’t perform that action at this time.