Agda: Why does Agda use less memory?

[nad]

Some of my code type-checks faster, using quite a bit less memory than before. Has anyone else noticed this? I'd be interested in knowing the cause of this improvement.

With Agda 2.6.1-ed526b5 compiled with GHC 8.6.5:

             750 MB total memory in use (0 MB lost due to fragmentation)
  Total   time  415.856s  (422.531s elapsed)

With Agda 2.6.0.1 compiled with GHC 8.4.4:

            2215 MB total memory in use (0 MB lost due to fragmentation)
  Total   time  444.285s  (450.781s elapsed)

[jespercockx]

I did some work on improving the performance of the occurs check (see https://github.com/agda/agda/issues/4120). The issue is about Prop, but one change I made could also impact general performance (https://github.com/agda/agda/commit/87d5957eb22f2dc1e692b68b7fdd0e4fd32825be)

[andreasabel]

I'd be interested in knowing the cause of this improvement.

@nad: You could do a bisection with a hard memory limit for checking your development.

[nad]

Yes, perhaps I'll do this later.